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

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

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

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

?(1,p), p ^
  

?(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.

---

© 2018 TU Wien, Theory and Logic Group - Björn Lellmann