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

About

MOLTAP is a Modal Logic Tableau Prover, an automated theorem prover for modal logic (in particular for epistemic logic). This program was developed for the Multi Agent Systems course. MOLTAP was inspired by OOPS, a similar proof system from a previous year.

Quick links

• Go to the prover
• Users guide
• Download the prover
• Theory behind the prover
• Implementation of the prover

Goals

The goals for the MOLTAP project are

• Create a convenient system for proving formulas in epistemic and other modal logics. In particular, this means
  • The syntax should be user friendly, and correspond directly to the formal notation.
  • Include notation for writing more complicated formulas, such as the let syntax.
• The system should generate counter models for false formulas and proofs for true formulas. This will help convince the user of the tool's correctness by allowing manual verification. In addition, proofs and counter examples could be used for educational purposes independent of the program.
• Include a correctness proof for the system. The formal description should correspond closely to the actual implementation.
• Support additional modal operators beyond □/◇, with the focus on epistemic logic. In this regard the common knowledge operator is the most important, because common knowledge greatly simplifies the modeling of real world situations.

There exist several other modal tableau provers, most of these have a different focus.

Known problems

At the present time there are still some problems with MOLTAP:

1. K and □ are used interchangeably throughout this paper. I should be more consistent.
2. The common knowledge operator can lead to infinite loops.
3. Common knowledge is not implemented correctly (there is no rule for K^*φ⁺).
4. The 4 and 5 rules for group knowledge are currently incorrect, for example the prover will claim that K_{1,2} x → K_{1,2} K_{1,2} x is true, which should not be the case. The expanded form (K₁ x ∧ K₂ x) → K₁ (K₁ x ∧ K₂ x) ∧ K₂ (K₁ x ∧ K₂ x) is indeed not valid.
5. The program still contains much experimental and debug code, a lot of which is not used. As a result building the source code will give many warning messages.