Howe, J.M. (1997) Two Loop Detection Mechanisms: A Comparison. In: TABLEAUX'97, May 13-16, 1997, Pont A Mousson, France, .
| Other (zip) | ||
|
Download (32Kb)
|
![[img]](http://kar.kent.ac.uk/style/images/fileicons/other.png) |
|
|
Download (95Kb)
|
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_pdf.png)
|
|
| Postscript | ||
|
Download (98Kb)
|
![[img]](http://kar.kent.ac.uk/style/images/fileicons/application_postscript.png)
|
|
| Official URL http://dx.doi.org/10.1007/BFb0027400 |
||
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<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 & 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: | Conference or workshop item (Paper) |
|---|---|
| Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
| Divisions: | Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group |
| Depositing User: | Mark Wheadon |
| Date Deposited: | 25 Aug 2009 17:28 |
| Last Modified: | 06 Sep 2011 03:56 |
| Resource URI: | http://kar.kent.ac.uk/id/eprint/21499 (The current URI for this page, for reference purposes) |
- Depositors only (login required):
