Atomic Cut Introduction by Resolution: Proof Structuring and Compression

Bruno Woltzenlogel Paleo (1)

1 VERIDIS - VERIfication pour les systèmes DIStribués

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.

Mots clés: Sequent Calculus; Proof Theory; Cut-Introduction

Domaines: Logique [math.LO]

Bruno Woltzenlogel Paleo. Atomic Cut Introduction by Resolution: Proof Structuring and Compression. Logic for Programming, Artificial Intelligence, and Reasoning, Apr 2010, Dakar, Senegal. pp.463-480, ⟨10.1007/978-3-642-17511-4_26⟩. ⟨hal-00545473⟩