Abstract
In order to compare two loop detection mechanisms we describe two calculi for theorem proving in intuitionistic propositional logic. We call them both MJ Hist, and distinguish between them by description as ‘Swiss’ or ‘Scottish’. These calculi combine in different ways the ideas on focused proof search of Herbelin and Dyckhoff & Pinto with the work of Heuerding et al on loop detection. The Scottish calculus detects loops earlier than the Swiss calculus but at the expense of modest extra storage in the history. A comparison of the two approaches is then given, both on a theoretic and on an implementational level.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Dyckhoff, R.: Contraction-free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic 57(3) (1992) 795–807
Dyckhoff, R.: MacLogic implementation. Available from URL http://www-theory.dcs.stand. ac.uk/∼rd/logic/soft.html
Dyckhoff, R., Pinto, L.: A Permutation-free Sequent Calculus for Intuitionistic Logic. University of St Andrews Research Report CS/96/9 (1996)
Dyckhoff, R., Pinto, L.: Implementation of a Loop-free Method for Construction of Countermodels for Intuitionistic Prepositional Logic. University of St Andrews Research Report CS/96/8 (1996)
Gabbay, D.: Algorithmic Proof With Diminishing Resources, Part 1. Proceedings of the 1990 workshop Computer Science Logic, eds. Börger, E., Kleine Büning, H., Richter, M. M., Schönfeld, W.; Springer LNCS 533 (1991) 156–173
Girard, J.-Y.: A New Constructive Logic: Classical Logic. Mathematical Structures in Computer Science 1 (1991) 255–296
Herbelin, H.: A λ-calculus Structure Isomorphic to Gentzen-style Sequent Calculus Structure. Proceeding of the 1994 workshop Computer Science Logic, eds. Pacholski, L., Tiuryn, J.; Springer LNCS 933 (1995) 61–75
Heuerding, A., Jäger, G., Schwendimann, S., Seyfried, M.: Propositional Logics on the Computer. Proceedings of the 1995 international workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX '95), eds. Baumgartner, P., Hähnle, R., Posegga, J.; Springer LNAI 918 (1995) 310–323
Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient Loop-Check for Backward Proof Search in Some Non-classical Propositional Logics. Proceedings of the 1996 international workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX '96), eds. Miglioli, P., Moscato, U., Mundici, D., Ornaghi, M.; Springer LNAI 1071 (1996) 210–225
Howe, J.M.: Theorem Proving and Partial Proof Search for Intuitionistic Propositional Logic Using a Permutation-free Calculus with Loop Checking. University of St Andrews Research Report CS/96/12 http://www-theory.cs.st-and.ac.uk/∼jacob/papers/tpil.html (1996)
Sahlin, D., Franzén, T., Haridi, S.: An Intuitionistic Predicate Logic Theorem Prover. Journal of Logic and Computation 2(5) (1992) 619–656
Shankar, N.: Proof Search in the Intuitionistic Sequent Calculus. Proceedings of the 1992 international conference on Automated Deduction (CADE-13), ed., Kupar, D.; Springer LNAI 607 (1992) 522–536
Stoughton, A.: porgi:a Proof-Or-Refutation Generator for Intuitionistic prepositional logic. http://www.cis.ksu.edu/∼allen/home.html
Tammet, T.: A Resolution Theorem Prover for Intuitionistic Logic. Available from the URL http://www.cs.chalmers.se/tammet/ (1996). This is a longer version of the paper in Proceedings of the 1996 international conference on Automated Deduction (CADE-13), eds. McRobbie, M. A., Slaney, J. K.; Springer LNAI 1104 (1996) 2–16
SICStus Prolog User's Manual. Swedish Institute of Computer Science (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Howe, J.M. (1997). Two loop detection mechanisms: A comparison. In: Galmiche, D. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1997. Lecture Notes in Computer Science, vol 1227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0027414
Download citation
DOI: https://doi.org/10.1007/BFb0027414
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-62920-7
Online ISBN: 978-3-540-69046-7
eBook Packages: Springer Book Archive