Cutres is a system which takes as input an LK-proof with arbitrary cuts and skolemized end-sequent and gives as output an LK-proof 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 II. Any resolution refutation #psi# of C then serves as a skeleton for an LK-proof #SIGMA# of the original end-sequent, containing only atomic cuts; #SIGMA# can be constructed from #psi# and II by projections. Note, that a proof with atomic cuts provides the same information as a cut-free proof.
展开▼
