MOLTAP

• Overview
• The prover
• Examples
• Users guide
• Syntax reference
• Download

Theory

• Introduction
• Propositional tableaux
• Modal tableaux
• KD, S4, S5, etc.
• Soundness
• Completeness
• Knowledge in groups
• Common knowledge

Implementation

• The basics
• Representing tableaux
• Working with models

Conclusion

• Conclusions
• Related work
• References

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
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 φ, 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.
# 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

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).