SquareEdgesExampleProof

gapt.examples.sequence.SquareEdgesExampleProof

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

Attributes

Returns: A proof of 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))

In this article

Generated with