LNSprover

Modular theorem proving with linear nested sequents

LNSprover is a prototype implementation of modular theorem provers for a number of normal and non-normal modal logics based on the linear nested sequent framework written in SWI Prolog. To run the prover, make sure you have SWI Prolog installed, then download and unpack this file and follow the instructions in the readme. The prover is based on the theoretical results contained in the article

• Proof Search in Nested Sequent Calculi, with Elaine Pimentel.
  In: M. Davis, A. Fehnker, A. McIver, A. Voronkov (Eds.): LPAR-20. LNCS, vol. 9450, pp.558-574. Springer Berlin Heidelberg (2015).
  Preliminary version.

This paper also contains an embedding of the linear nested sequent calculi into linear logic which is exploited in the prover POULE.

The code is also available on github.

Björn Lellmann, August 2016