Two loop detection mechanisms: A comparison | SpringerLink
Skip to main content
Springer Nature Link
Log in

Two loop detection mechanisms: A comparison

  • Contributed Papers
  • Conference paper
  • First Online:
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 1997)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1227))

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.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Dyckhoff, R.: Contraction-free Sequent Calculi for Intuitionistic Logic. Journal of Symbolic Logic 57(3) (1992) 795–807

    Google Scholar 

  2. Dyckhoff, R.: MacLogic implementation. Available from URL http://www-theory.dcs.stand. ac.uk/∼rd/logic/soft.html

    Google Scholar 

  3. Dyckhoff, R., Pinto, L.: A Permutation-free Sequent Calculus for Intuitionistic Logic. University of St Andrews Research Report CS/96/9 (1996)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. 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

    Google Scholar 

  6. Girard, J.-Y.: A New Constructive Logic: Classical Logic. Mathematical Structures in Computer Science 1 (1991) 255–296

    Google Scholar 

  7. 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

    Google Scholar 

  8. 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

    Google Scholar 

  9. 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

    Google Scholar 

  10. 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)

    Google Scholar 

  11. Sahlin, D., Franzén, T., Haridi, S.: An Intuitionistic Predicate Logic Theorem Prover. Journal of Logic and Computation 2(5) (1992) 619–656

    Google Scholar 

  12. 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

    Google Scholar 

  13. Stoughton, A.: porgi:a Proof-Or-Refutation Generator for Intuitionistic prepositional logic. http://www.cis.ksu.edu/∼allen/home.html

    Google Scholar 

  14. 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

    Google Scholar 

  15. SICStus Prolog User's Manual. Swedish Institute of Computer Science (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Division, University of St Andrews, KY16 9SS, Scotland

    Jacob M. Howe

Authors
  1. Jacob M. Howe
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Didier Galmiche

Rights and permissions

Reprints 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

Publish with us

Policies and ethics

Search

Navigation