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 based on the
paper Combining
monotone and normal modal logic in nested sequents -- with
countermodels. Given a formula as an input the prover produces
either a nested sequent derivation or a countermodel in the
neighbourhood framework. Since the logic is a combination of
monotone modal logic M and normal modal logic K, the prover can be
used to obtain derivations or countermodels for these logics as well.

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, optionally select
additional axioms, 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 and
manually split the derivation in the tex file.

The implemented base logic is bimodal monotone modal logic,
originally introduced by M.A. Brown in the
article On the
Logic of Ability. The logic is a combination of monotone
non-normal modal logic M for the operator ea and
normal modal logic K for the operator aa. The full
set of Hilbert-style axioms and rules is given by:

p -> q / ea p -> ea q (monotonicity rule for ea)

p -> q / aa p -> aa q (monotonicity rule for aa)

p / aa p (necessitation rule for aa)

aa p and aa q -> aa(p and q) (aggregation axiom for aa)

ea(p -> q) and aa p -> ea q (first interaction axiom)

aa p -> ea p or aa q (second interaction axiom)

Since bimodal monotone modal logic conservatively extends both
monotone modal logic M and normal modal logic K, you can use the
prover for these logics as well by restricting the input formula
to the language with only the modal operator ea
or aa respectively. For derivable formulae this
results in derivations in essentially the full nested version of
the linear nested sequent calculus for monotone modal logic M from
the
article Modularisation
of Sequent Calculi for Normal and Non-normal Modalities and
the two-sided nested sequent calculus for normal modal logic K
introduced independently by K. Brünnler
in Deep
Sequent Systems for Modal Logic and by F. Poggiolesi
in The
Method of Tree-hypersequents for Modal Propositional Logic,
respectively.

The implemented extensions so far include any combination of the
following axioms:

neg ea false, or equivalently neg (ea a ->
aa neg a). Semantically defined by the condition that
no set of neighbourhoods contains the empty set.

aa a -> ea a. Semantically defined by the
condition that no set of neighbourhoods is empty.

neg (aa a and aa neg a) (seriality axiom
for aa). Semantically defined by the condition
that every set of neighbourhoods contains a non-empty
neighbourhood.

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

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