A redundancy analysis of sequent proofs

Lutovac, T and Harland, J 2005, 'A redundancy analysis of sequent proofs', in TABLEAUX 2005: Automated Reasoning with Analytic Tableaux and Related Methods, Koblenz, Germany, 14-17 September 2005.


Document type: Conference Paper
Collection: Conference Papers

Title A redundancy analysis of sequent proofs
Author(s) Lutovac, T
Harland, J
Year 2005
Conference name International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
Conference location Koblenz, Germany
Conference dates 14-17 September 2005
Proceedings title TABLEAUX 2005: Automated Reasoning with Analytic Tableaux and Related Methods
Publisher Springer
Place of publication Berlin
Abstract Proof search often involves a choice between alternatives which may result in redundant information once the search is complete. This behavior can manifest itself in proof search for sequent systems by the presence of redundant formulae or subformulae in a sequent for which a proof has been found. In this paper we investigate the detection and elimination of redundant parts of a provable sequent by using labels and Boolean constraints to keep track of usage information. We illustrate our ideas in propositional linear logic, but we believe the general approach is applicable to a variety of sequent systems, including other resource-sensitive logics.
Subjects Artificial Intelligence and Image Processing not elsewhere classified
DOI - identifier 10.1007/11554554_15
Copyright notice © Springer-Verlag Berlin Heidelberg 2005
Versions
Version Filter Type
Altmetric details:
Access Statistics: 176 Abstract Views  -  Detailed Statistics
Created: Wed, 22 Jul 2009, 15:47:23 EST by Catalyst Administrator
© 2014 RMIT Research Repository • Powered by Fez SoftwareContact us