Abstract
The careful introduction of cut inferences can be used to structure and possibly compress formal sequent calculus proofs. This paper 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 compression is shown to be exponential in the length of proofs. © 2010 Springer-Verlag.
Cite
CITATION STYLE
Woltzenlogel Paleo, B. (2010). Atomic cut introduction by resolution: Proof structuring and compression. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6355 LNAI, pp. 463–480). https://doi.org/10.1007/978-3-642-17511-4_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
