Abstract
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. © Springer-Verlag Berlin Heidelberg 2001.
Cite
CITATION STYLE
Happe, J. (2001). The ModProf theorem prover. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2083 LNAI, pp. 459–463). Springer Verlag. https://doi.org/10.1007/3-540-45744-5_39
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
