gapt.examples.sequence

Auxiliary structure to deal with axioms of the schema: Forall variables cond1 -> cond2 -> ... -> condn -> consequence |- ...

Proof of f(n) = g(n, 1), where f is the head recursive and g the tail recursive formulation of the factorial function

Constructs short FOL LK proofs of the sequents

P(0), ∀x. P(x) → P(s(x)) :- P(s^2 ^n^ ^(0))

where n is an Integer parameter >= 0.

Functions to construct cut-free FOL LK proofs of the sequents

Refl, Trans, \ALL x. f(x) = x :- f^n^(a) = a

where n is an Integer parameter >= 0.

Constructs cut-free FOL LK proofs of the sequents

P(0), ∀x. P(x) → P(s(x)) :- P(s^n^(0))

where n is an Integer parameter >= 0.

Functions to construct cut-free FOL LK proofs of the sequents

P(0,0), ∀x,y. P(x,y) → P(s(x),y), ∀x,y. P(x,y) → P(x,s(y)) :- P(s^n^(0),s^n^(0))

where n is an Integer parameter >= 0.

The proofs constructed here go along the diagonal of P, i.e. one x-step, then one y-step, etc.

Functions to construct cut-free FOL LK proofs of the sequents

P(a,b), ∀x,y. P(x,y) → P(s,,x,,(x),y), ∀x,y. P(x,y) → P(x,s,,y,,(y)) :- P(s,,x,,^n^(a),s,,y,,^n^(b))

where n is an Integer parameter >= 0.

The proofs constructed here go along the edges of P, i.e. first all X-steps are performed, then all Y-steps are performed, but unlike SquareEdgesExampleProof, different functions are used for the X- and the Y-directions.

Functions to construct cut-free FOL LK proofs of the sequents

P(0,0), ∀x,y. P(x,y) → P(s(x),y), ∀x,y. P(x,y) → P(x,s(y)) :- P(s^n^(0),s^n^(0))

where n is an Integer parameter >= 0.

The proofs constructed here go along the edges of P, i.e. first all X-steps are performed, then all Y-steps are performed

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.

Functions to construct cut-free FOL LK proofs of the sequents

Refl, Trans, CongSuc, ABase, ASuc :- sum( n ) = s^n^(0)

where n is an Integer parameter >= 0.