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


The goals for the MOLTAP project are

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 (K1 x K2 x) K1 (K1 x K2 x) K2 (K1 x K2 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.