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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
E. Giunchiglia, A. Tacchella, ✻SAT: a System for the Development of Modal Decision Procedures, in: Automated Deduction—CADE-17, Springer, LNAI 1831, 2000.
V. Haarslev, R. Möller, RACE System Description, in: Proc. of the International Workshop on Description Logics (DL’ 99), Linköping, pp. 130–132, 1999
I. Horrocks, Optimising Tableaux Decision Procedures for Description Logics. Ph.D. thesis, Univ. of Manchester, U.K. 1997
J. Happe, A Subsumption-Aided Caching Technique, to appear.
F. Massacci, Simplification with Renaming: A General Proof Technique for Tableau and Sequent Based Provers, Tech. Report 424, Computer Laboratory, Univ. of Cambridge, UK, 1997.
F. Massacci, Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison, in: Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000), pp. 52–56, Springer, LNAI 1847, 2000.
P. F. Patel-Schneider, DLP System Description. In E. Franconi, G. de Giacomo, R.M. MacGregor, W. Nutt, C.A. Welty and F. Sebastiani (eds.) Collected Papers from the International Description Logics Workshop (DL’ 98), pp. 87–89, 1998.
I. Horrocks, P. F. Patel-Schneider, Optimizing Description Logic Subsumption. Journal of Logic and Computation, 9:3, pp. 267–293, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Happe, J. (2001). The modprof Theorem Prover. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_39
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_39
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive