arXiv subjects

Michael Peter Lettmann

Publications and source records attributed to Michael Peter Lettmann.

3 recordsLinked to original sources

arXiv2018

The problem of Pi_2-cut-introduction

We describe an algorithmic method of proof compression based on the introduction of Pi_2-cuts into a cut-free LK-proof. The current approach is based on an inversion of Gentzen s cut-elimination method and extends former methods for introducing Pi_1-cuts. The Herbrand instances of a cut-free proof pi of a sequent S are described by a grammar G which encodes substitutions defined in the elimination of quantified cuts. We present an algorithm which, given a grammar G, constructs a Pi_2-cut formula A and a proof phi of S with one cut on A. It is shown that, by this algorithm, we can achieve an exponential proof compression.

cs.LO↗

arXiv2018

A Tableaux Calculus for Reducing Proof Size

A tableau calculus is proposed, based on a compressed representation of clauses, where literals sharing a similar shape may be merged. The inferences applied on these literals are fused when possible, which reduces the size of the proof. It is shown that the obtained proof procedure is sound, refutationally complete and allows to reduce the size of the tableau by an exponential factor. The approach is compatible with all usual refinements of tableaux.

cs.LO↗

arXiv2017

Integrating a Global Induction Mechanism into a Sequent Calculus

Most interesting proofs in mathematics contain an inductive argument which requires an extension of the LK-calculus to formalize. The most commonly used calculi for induction contain a separate rule or axiom which reduces the valid proof theoretic properties of the calculus. To the best of our knowledge, there are no such calculi which allow cut-elimination to a normal form with the subformula property, i.e. every formula occurring in the proof is a subformula of the end sequent. Proof schemata are a variant of LK-proofs able to simulate induction by linking proofs together. There exists a schematic normal form which has comparable proof theoretic behaviour to normal forms with the subformula property. However, a calculus for the construction of proof schemata does not exist. In this paper, we introduce a calculus for proof schemata and prove soundness and completeness with respect to a fragment of the inductive arguments formalizable in Peano arithmetic.

math.LO↗