Value Members

1.  object FactorialFunctionEqualityExampleProof extends ProofSequence

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

2.  object FactorialFunctionEqualityExampleProof2 extends ProofSequence
3.  object LinearCutExampleProof extends ProofSequence

   Constructs short FOL LK proofs of the sequents

   Constructs short 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.

4.  object LinearEqExampleProof extends TacticsProof with ProofSequence with ExplicitEqualityTactics

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

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

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

   where n is an Integer parameter >= 0.

5.  object LinearExampleProof extends ProofSequence

   Constructs cut-free FOL LK proofs of the sequents

   Constructs cut-free FOL LK proofs of the sequents

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

   where n is an Integer parameter >= 0.

6.  object LinearRightCutExampleProof extends ProofSequence
7.  object SquareDiagonalExampleProof extends ProofSequence

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

   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ⁿ(0),sⁿ(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.

8.  object SquareEdges2DimExampleProof extends ProofSequence

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

   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ⁿ(a),s_yⁿ(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.

9.  object SquareEdgesExampleProof extends ProofSequence

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

   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ⁿ(0),sⁿ(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

10.  object SumExampleProof extends ProofSequence

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

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

    P(sⁿ(0),0), ∀x,y. P(s(x),y) → P(x,s(y)) :- P(0,sⁿ(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.

11.  object SumOfOnesExampleProof extends ProofSequence

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

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

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

    where n is an Integer parameter >= 0.

12.  object SumOfOnesF2ExampleProof extends TacticsProof with ProofSequence with ExplicitEqualityTactics
13.  object SumOfOnesFExampleProof extends TacticsProof with ProofSequence with ExplicitEqualityTactics
14.  object UniformAssociativity3ExampleProof extends ProofSequence