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).