SquareEdges2DimExampleProof
gapt.examples.sequence.SquareEdges2DimExampleProof
object SquareEdges2DimExampleProof extends ProofSequence
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.
Attributes
- Graph
-
- Supertypes
- Self type
Members list
In this article