SumExampleProof
gapt.examples.sequence.SumExampleProof
object SumExampleProof extends ProofSequence
Functions to construct the straightforward cut-free FOL LK proofs of the sequents
P(s^n^(0),0), ∀x,y. P(s(x),y) → P(x,s(y)) :- P(0,s^n^(0))
where n is an Integer parameter >= 0.
This sequent is shown to have no cut-free proof which can be compressed by a single cut with a single quantifier in S. Eberhard, S. Hetzl: On the compressibility of finite languages and formal proofs, submitted, 2015.
Attributes
- Graph
-
- Supertypes
- Self type
-
SumExampleProof.type
Members list
In this article