Two loop detection mechanisms: a comparison
Howe, J. M. (1997). Two loop detection mechanisms: a comparison. In: LNCS. International Conference on Analytic Tableaux and Related Methods (TABLEAUX'97), 13 - 16 May 1997, Pont-a-Mousson, France.
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 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.
| Publication Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | The original publication is available at www.springerlink.com |
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| Departments: | School of Science & Technology > Computer Science |
Metadata
MetadataActions (login required)
Admin Login