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