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.