SquareDiagonalExampleProof

gapt.examples.sequence.SquareDiagonalExampleProof

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.

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))
Source: SquareDiagonalExampleProof.scala

In this article

Generated with