Propositional Modal Logic KD45

Also known as Weak S5 (WS5) because it lacks reflexivity, this logic is often used as the basis of logics of agents where []p means "the agent knows p" or "the agent believes p".

When you enter a formula A, then "closed" means that A is a theorem because the tableau for ~ A
is closed, and "open" means that A is not a theorem because the tableau for ~ A is open.

Prover for modal logic KD45.
Based on:
Efficient Loop-Check for KD45 Logic
A Birstunas
Lithuanian Mathematics Journal 46(1):44-53 2006.

Author: Rajeev Gore 01 November 2007 (Copyright).

Logic KD45 is built from basic normal modal logic K by adding
the following extra axioms:
D = []p -> <>p which forces R to be serial or total
4 = []p -> [][]p which forces R to be transitive
5 = <>p -> []<>p which forces R to be euclidean.

It is often used as a logic for agents where:
[]p means "the agent believes p"
or
[]p means "the agent knows p".

Histories:
DIAS: accummulates diamond formulae so we can identify new ones
BOXS: accummulates box formulae so we can identify new ones

Inv 1: For every node N, both DIAS and BOXS are subsets of N.
Proof: no rule deletes diamond formulae or box formulae from nodes.

Inv 2: The sets DIAS and BOXS grow monotonically down a branch.
Proof: rules only add formulae to these histories.

Termination: Eventually, no new boxes or diamonds appear so
the side condition to the KD45Birstinas rule will evaluate to
false and this rule is not applicable.

Functions:

somethingnew(l, s)

returns true if list l contains an element
which is not in set s. The pre-defined function
is_in(xl, ys) checks whether the singleton list xl is in
the set ys. For each member h of x, we construct the
singleton list [h] and use is_in([h], s) to check whether
h is in the set s. We return true as soon as we find an
h that is not in s.

newdiamondorboxfound(diaa, diax, bxy, dias, boxs)

returns true if diaa or diax contain an element which is
not in dias or bxy contains an element which is not in boxs.

KD45Birstunas Rule:

This rule is taken directly from the paper mentioned above except
that the principal formula <>A is enclosed in parentheses i.e.
( <> A ) rather than braces i.e. { <> A }. The parentheses are understood
by the TWB to mean "the principal formula may be missing". But if
<> A is missing then <> X must be empty too so this rule creates a
successor even when there are no diamonds as required by Birstunas.

Results
Query

ATOM := a | b | c | ...
formula :=
ATOM | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| [] formula
| <> formula
| ~ formula

Info
kd45Birstunas.ml : Download