System Description: CutRes 0.1: Cut Elimination by Resolution

CutRes is a system which takes as input an LK-proof with arbitrary cuts and skolemized end-sequent and gives as output an LKproof with atomic cuts only. The elimination of cuts is performed in the following way: An unsatisfiable set of clauses C is assigned to a given LK-proof Π. Any resolution refutation ψ of C then serves as a skeleton for an LK-proof Σ of the original end-sequent, containing only atomic cuts; Σ can be constructed from ψ and Π by projections. Note, that a proof with atomic cuts provides the same information as a cut-free proof.

• Type: Conference
• Year: 1999
• Where: CADE
• Authors: Matthias Baaz, Alexander Leitsch, Georg Moser
• Keywords: Arbitrary Cuts, Atomic Cuts, CADE 1999, Logical Reasoning, Resolution Refutation