Propositional formulas

There are three ways to write logical connectors

  1. Using ASCII syntax, for example p & q.
  2. Using Unicode symbols, for example p q.
  3. Using natural language, for example p and q.
Input syntax Description
p, q, cat, bigVar123 Propositional variables consists of alphanumeric symbols, starting with a lower case letter.
(φ)Parentheses can be used for grouping.
, true, falseThe 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

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

Input syntax Description
K_1 φ, K1 φ []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 K1 φ & K2 φ.
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 φ, M1 φ <>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.
# commentComments begin with a # sign and run until the end of the line.

The possible axioms stand for:

Precedence and associativity

  1. not and modal operators bind the strongest.
  2. Followed by and,
  3. then or
  4. and finally implication and equivalence. Implication associates to the right.
  5. 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).