Theorem Prover for S5 + PAL

Welcome! We're Hein de Haan and Martijn Wagenaar, two students of Artificial Intelligence (MSc.) at the University of Groningen. As a project for the course Multi-Agent Systems, we decided to build a system that can prove logical formulas in the epistemic logic S5, extended with Public Announcements. The user of our system can input a set of premisses and a conclusion. If that conclusion does indeed follow from the premisses (given the rules and axioms of S5 with Public Announcements), the system will find a proof in the form of a tableau.

S5 is an extension of the axiom system K, which itself consists of propositional logic combined with epistemic formulas. In what follows, we will shortly talk about propositional logic, mainly to introduce the corresponding symbols our system uses. We will then continue to explain some things about K, again also to show how to write epistemic formulas in our system. Finally, we will do the same for S5 with Public Announcements.

Propositional Logic

Many literature is available on this topic, so we will not explain propositional logic. We will of course explain how to use it in our system. Let φ and ψ be formulas in propostional logic and p be a single proposition. The system accepts the propositional formulas listed below:

• Proposition: p. True if and only if p is true.
• Negation: !(φ). True if and only if φ is not true.
• Conjunction: φ&ψ. True if and only if both φ and ψ are true.
• Disjunction: φ|ψ. True if and only if φ is true or ψ is true or both φ and ψ are true.
• Implication: φ->ψ. True if and only if φ is false or ψ is true.
• Bi-implication: φ<->ψ. True if and only if φ and ψ have the same truth value. I.e, φ and ψ are both true, or φ and ψ are both false.

Of course, brackets ("(" and ")") have to be used if there is any chance of ambiguity.

To summarize:

Syntax rule: φ ::= p | !(φ) | φ&ψ | φ|ψ | φ->ψ | φ<->ψ

where p is a single proposition

Epistemic Logic: K and S5

In multi-agent systems it is often important to describe the knowledge of the agents. Some agents could know that a certain proposition p is valid, while other agents consider both p and not p possible. When there is a formal way of describing this kind of knowledge, it can be used for, for instance, communication between agents and action selection.

To describe multi-agent systems in terms of knowledge and belief, epistemic logic is of use. Epistemic logic uses Kripke's possible worlds semantics and includes accessibility relations which are agent specific. In epistemic logic, K_i(p) means that agent i knows that p is true. In other words: in all worlds accessible for agent i, p is valid. M_i(p) means that agent i considers p to be possible. Using Kripke's possible worlds semantics: there is at least one world accessible for agent i in which p is valid.

The basis of our program uses an axiom system which is an extension of K_(m), where m is the number of agents within the system. Therefore, we will describe the axiom system K_(m) in more detail. K_(m) contains the following axioms:

• (A1) All (instances of) tautologies from propositional logic
• (A2) (K_iφ ∧ K_i(φ → ψ)) → K_iψ

K(m) contains two derivation rules:

• (R1) From φ and φ → ψ follows ψ (Modus Ponens)
• (R2) From φ follows K_iφ (Necessitation)

An extension of K_(m) which is useful for describing knowledge within a system, is S5_(m). S5_(m) is sound and complete for the class of all models that are reflexive, transitive and euclidean. These properties are reflected in the additional axioms for S5_(m): axiom system S5_(m) consists of K_(m) plus three axioms:

• (A3) K_iφ → φ
• (A4) K_iφ → K_iK_iφ
• (A5) ¬K_iφ → K_i¬K_iφ

Our program uses S5(m) with an extension for Public Announcement Logic and accepts epistemic operators in the following way:

Syntax: Ki(φ)

where i is the number of an agent and φ the formula which the agent knows

Syntax: Mi(φ)

where i is the number of an agent and φ the formula which the agent considers possible

Public Announcements

Public announcements are supported in the program. For public announcements, we use the operator [φ] ψ. This means that after a truthful announcement of φ by an external agent (which is not part of the system), ψ is valid. It has been shown that expressions containing the operator for public announcements can be rewritten to epistemic formulas. Our system uses the following translation from PAL (Public Announcement Logic) to EL (Epistemic Logic):

[φ]p	⇒	φ → p
[φ](ψ ∧ χ)	⇒	[φ]ψ ∧ [φ]χ
[φ]¬ ψ	⇒	φ → ¬[φ]ψ
[φ]Kαψ	⇒	φ → Kα[φ]ψ

By applying these rules, it is possible to convert any PAL formula into an equivalent EL formula. Our program accepts the PAL operator as follows:

Syntax: [φ](ψ)

where φ is the announcement and ψ the formula that holds after announcing φ

Tableaux rules

To show whether a formula holds in S5+PAL, tableaux are constructed. The rules which are applied in order to construct the tableaux, are listed below. We only list the rules that are more than mere rewrite rules (such as !(φ|ψ) ⇒ !φ&!ψ).

φ|ψ	⇒	φ | ψ
φ&ψ	⇒	φ ψ
Mi(φ)	⇒	φ, j (where j is new)
Ki(φ)	⇒	φ
!(!(φ))	⇒	φ
[φ](p)	⇒	φ->p
[φ](ψ&χ)	⇒	[φ](ψ)&[φ](χ)
[φ](!ψ)	⇒	φ->
[φ](Ki(ψ))	⇒	φ->Ki[φ](ψ)

Only a disjunction directly triggers a split of the current branch. Whenever a formula on the left is paired with a specific world (for example: φ&ψ, 3), the tableaux rule is applied but only for that world (the example would result in two new lines, namely: φ, 3 and ψ, 3). There is one exception to this: due to the properties of S5, when Ki(φ), then φ in general, and not only in a specific world. So when the system encounters the line Ki(φ), 3, the added formula will be φ instead of φ, 3.

Outcome

A tableau either takes as a starting point:

1. certain premisses and the negation of a conclusion
2. the negation of a set formulas (when a conclusion is not included)

A branch closes when

• it contains a contradiction in general (so not for specific worlds): φ and !(φ)
• it contains a contradiction for a specific world i: φ, i and !(φ), i
• it contains a mixed contradiction (one for a specific world i, one in general): φ, i and !(φ) (note that the placement of the negation is not of importance; the formula in world i could as well be negated)

When all branches of a tableau close, it has been shown that the given formula is a logical truth.

The current version of the software can be downloaded here (right mouse button -> save link as to save it to your computer).

To run the program, the programming language Python is required, which can be downloaded from here.

After installing Python, open a terminal and navigate to the folder where the downloaded file was saved to. Then, type python tp_s5pal.py to run the program.

Our system is very easy to use. Once you have opened the program, it asks you to input your first premisse. If you do not have premisses, just press enter immediately. After the first premisse, you can add more premisses if you want. Once you have pressed enter without giving a premisse, you are asked to give a conclusion which the system will try to prove. Just as with the premisses, you do not have to give a conclusion. After this, the program askes whether you want to see the tableau or not. In either case, the program will tell you whether or not the conclusion follows from the premisses. One final note: you always have to use brackets in case of a negation. !P, where P is a proposition, will not be parsed correctly. Use !(P) instead.