## Propositional formulas

There are three ways to write logical connectors

- Using ASCII syntax, for example p & q.
- Using Unicode symbols, for example p ∧ q.
- Using natural language, for example p and q.

Input syntax | Description | ||
---|---|---|---|

ASCII | Unicode | Text | |

p, q, cat, bigVar123 | Propositional variables consists of alphanumeric symbols, starting with a lower case letter. | ||

(φ) | Parentheses can be used for grouping. | ||

⊤, ⊥ | true, false | The true/false proposition. | |

~φ | ¬φ | not φ | Logical negation, ¬φ is true if and only if φ is false. |

φ & ψ | φ ∧ ψ | φ and ψ | Logical conjunction |

φ | ψ | φ ∨ ψ | φ or ψ | Logical disjunction |

φ -> ψ | φ → ψ | φ implies ψ | Logical implication |

φ <- ψ | φ ← ψ | Implication written the other way around. | |

φ <-> ψ, φ = ψ | φ ↔ ψ | Logical equivalence | |

φ <-/-> ψ, φ /= ψ | φ ↮ ψ, φ ≠ ψ | Logical inequivalence |

## Modal formulas

Modal formulas are formulas about agents. Agent names can be arbitrary strings of alphanumeric symbols. Examples of valid agent names are

- 1, 2
- Alice, Bob
- my_Computer
- α, β

MOLTAP supports both the epistemic style (K/M) and modal style (□/◇) of writing operators.

Input syntax | Description | |
---|---|---|

Epistemic | Modal | |

K_1 φ, K_{1} φ | []_{1} φ, □_{1} φ | Agent 1 knows that φ, φ is necessary for agent 1. |

K_{{1,2}} φ | []{1,2} φ | Agents 1 and 2 both knows that φ. This is the same as K_{1} φ & K_{2} φ. |

K φ | [] φ | Every agent knows φ. |

K* φ, K^{*}_{1,2} φ | []* φ | It is common knowledge that φ. Every agent (in a set) knows that φ, and they know that everyone knows, and they know that everyone knows that everyone knows, etc. |

M_1 φ, M_{1} φ | <>_{1} φ, ◇_{1} φ | Agent 1 holds φ for possible, φ is possible for agent 1. |

## Advanced features

Input syntax | Description |
---|---|

let x = φ; ψ | Create a local declaration. Inside ψ all occurrences of x will be replaced by φ. Declarations are only allowed at the top level. |

system S; ψ | Change the axiom system. By default system S5 (=KT45) is used. The name S is either a combination of KDT45 or S4 or S5. |

# comment | Comments begin with a # sign and run until the end of the line. |

The possible axioms stand for:

- K = the basic axiom system, this is always used.
- D = seriality, each world has a successor, ◇
_{i}⊤. - T = all relations are reflexive, □
_{i}φ → φ. - 4 = all relations are transitive, □
_{i}φ → □_{i}□_{i}φ. - 5 = all relations are euclidean, ◇
_{i}φ → □_{i}◇_{i}φ.

## Precedence and associativity

- not and modal operators bind the strongest.
- Followed by and,
- then or
- and finally implication and equivalence. Implication associates to the right.
- Programming features like let bind even weaker.

So for example K1 p ∧ ~q ∨ r → s → t is parsed as (((K_1 p) ∧ (¬q)) ∨ r) → (s → t).