The MODPROF theorem prover. This paper introduces MODPROF, a new theorem prover and model finder for propositional and modal logic K. MODPROF is based on labelled modal tableaux. Its novel feature is a sophisticated simplification algorithm using structural subsumption to detect redundancies. Further distinctive features are the use of syntactic branching, and an enhanced loop-checking algorithm using a cache of satisfiable worlds created in the course of the proof. Experimental results on problems of the TANCS 2000 Theorem Prover comparison are presented.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element