phi ::= a,b,c,... | false | true | neg phi | phi and phi | phi or phi | phi -> phi | ea phi | aa phi

Common axioms and interesting examples

Monotonicity for ea:

ea (a and b) -> ea a and ea b

Necessitation for ea:

ea true

Aggregation for ea:

ea a and ea b -> ea (a and b)

Interaction between the operators:

aa (a -> b) and ea a -> ea b

Axiom D for ea:

neg (ea a and ea neg a)

Axiom D for ea and aa:

neg (ea a and aa neg a)

Axiom T for ea:

ea a -> a

Large model:

ea (ea c and d -> aa a or ea b or f) and ea(ea m -> k
or ea l or ea n) and aa( ea x and aa y -> ea( ea z and ea w)) -> aa
(g or aa h) or ea ea ea ea i or ea(aa o -> ea p)

K

?(5, p + q) , ?(4, r + t), !(1, p ^ * t ^)
?(1, q) && ?(1, p) && !(1, p ^ * q ^)
?(1, p * q ^) && ?(1, p ^) && !(1, q)

K + 4

?(1, p), !(1, !(1, p ^))
?(3, p + q), !(2, !(1, p ^ ))
?(5, p) , ?(4, q), !(2, !(1, p ^ * q ^))
?(3, p ^) , !(2, !(1, p))

K + D

?(1,p) , ?(1, p ^)
?(2,?(1, p)) , ?(2, !(1, p ^))
?(1, ?(1, p)) && ?(1, ?(1, p ^))

K + T

?(1,p), p ^

K + D + 4

?(2, p) && ?(2, ?(1, p ^))
?(3, ?(2, p)) && ?(2, ?(1, p ^))

Description

nnProver is a Prolog implementation of a nested sequent prover
for bimodal monotone modal logic. Given a formula as an input it
produces either a nested sequent derivation or a countermodel in the
neighbourhood framework.

Formulae are built from the grammar

Phi ::= atom | false | true | neg Phi | Phi and Phi | Phi or Phi
| Phi -> Phi | ea Phi | aa Phi

where atom is any Prolog atom, e.g., p,q,r,...,a1,a2,a3,...
The usual conventions about binding strength of the connectives apply, i.e.,
the unary connectives neg, ea, aa bind stronger than and
binds stronger than or binds stronger than ->.

To run the prover, input your formula, select the logic, and hit 'Prove'. The derivation or a countermodel is displayed automatically. You might need to zoom in a bit for large derivations.
NOTE: In some cases the derivations or models might become too large for TeX to handle (if they are more than about 19 feet). In these cases no pdf output is produced. However, you may still download the source code, run the prover locally, and manually split the derivation in the tex file.

For further information, contact Björn Lellmann. We thank Carlos Olarte for his help in implementing this site.