hal-00545473, version 1
Atomic Cut Introduction by Resolution: Proof Structuring and Compression
Logic for Programming, Artificial Intelligence, and Reasoning 6355 (2010) 463-480
Abstract: The careful introduction of cut inferences can be used to structure and possibly compress formal sequent calculus proofs. This pa- per presents CIRes, an algorithm for the introduction of atomic cuts based on various modifications and improvements of the CERes method, which was originally devised for efficient cut-elimination. It is also demonstrated that CIRes is capable of compressing proofs, and the amount of compres- sion is shown to be exponential in the length of proofs.
- 1:
- Université de Lorraine – CNRS : UMR7503 – INRIA
- Domain : Mathematics/Logic
- Keywords : Sequent Calculus – Proof Theory – Cut-Introduction
- Comment : The original publication is available at www.springerlink.com
- hal-00545473, version 1
- http://hal.archives-ouvertes.fr/hal-00545473
- oai:hal.archives-ouvertes.fr:hal-00545473
- From:
- Submitted on: Saturday, 11 December 2010 12:55:31
- Updated on: Monday, 13 December 2010 10:12:16
Associated documents
Export