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

Common axioms

Linearity:

(a -> b) or (b -> a)

Bounded depth 2:

q or (q -> p or (p -> false))

Alternatively:

((p -> (((q -> r) -> q) -> q)) -> p) -> p

Smetanich logic:

((q -> false) -> p) -> (((p -> q) -> p) -> p)

Classical logic:

p or (p -> false)

Bounded branching 2:

(p and q -> r) or (p and r -> q) or (q and r -> 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

iiProve is a Prolog implementation of a generic theorem prover for propositional intermediate logics in the framework of injective nested sequents. Due to the close similarity between injective nested sequents and tree-like models for intermediate logics, a failed proof search for a formula produces a countermodel.

Supported logics:

Intuitionistic logic INT: No restrictions on the frames

Gödel-Dummett logic GD: Linear Kripke-frames

Smetanich logic Sm: Linear Kripke-frames with depth at most two

Greatest Semi-constructible logic GSc: Kripke-frames with depth at most two and at most two final elements

Bounded depth logics BD(N): Kripke-frames with depth at most N

N-valued Gödel logics: Linear Kripke-frames with at most N worlds

Classical logic: Kripke-frames with at most one world

Formulae are built from the grammar

Phi ::= atom | false | true | Phi and Phi | Phi or Phi | Phi -> Phi

where atom is any Prolog atom, e.g., p,q,r,...,a1,a2,a3,...
Negation is treated as defined by not(A) <-> (A -> false).
The usual conventions about binding strength of the connectives apply, i.e.,
'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 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.

The source code in SWI-Prolog can be obtained here. To run the prover, follow the instructions in the Readme. In order to typeset the output you will also need LaTeX

The prover is based on a general method for the construction of calculi for intermediate logics in the framework of nested sequents. Unlike the standard approach, nested sequents are understood in a very semantical way, and are embedded into Kripke models in the corresponding frame class. Except for the implication left rule and the Lift and Lower rules, the rules do not copy the principal formula into the premisses, because the rules for conjunction and disjunction can be shown to be invertible, while for implication right it can be shown that derivations can be restricted so that this rule creates only one new component per implication and branch in the nested sequent. Internally, the rules still create an "invisible" copy of the principal formulae to prevent loops.

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