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
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Goré, Rajeev (ed.); Leitsch, Alexander (ed.); Nipkow, Tobias (ed.): Automated reasoning. 1st international joint conference, IJCAR 2001, Siena, Italy, June 18-22, 2001. Proceedings (2001)
- Happe, Jens: The MODPROF theorem prover (2001)