Skip to main content
Kent Academic Repository

Two Loop Detection Mechanisms: A Comparison

Howe, Jacob M. (1997) Two Loop Detection Mechanisms: A Comparison. In: Galmiche, D., ed. Automated Reasoning with Analytic Tableaux and Related Methods International Conference. Lecture Notes in Artificial Intelligence . Springer, Berlin, Germany, pp. 188-200. ISBN 978-3-540-62920-7. E-ISBN 978-3-540-69046-7. (doi:10.1007/BFb0027414) (KAR id:21499)


In order to compare two loop detection mechanisms we describe two calculi for theorem proving in intuitionistic propositional logic. We call them both MJ<sup>Hist</sup>, 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 &amp; Pinto with the work of Heuerding emphet 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.

Item Type: Book section
DOI/Identification number: 10.1007/BFb0027414
Uncontrolled keywords: Theorem Prove, Intuitionistic Logic, Propositional Variable, Sequent Calculus, Proof Tree
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 25 Aug 2009 17:28 UTC
Last Modified: 16 Nov 2021 09:59 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.