Generated with

gapt-examples/gapt.examples/gapt.examples.sequence/LinearCutExampleProof

LinearCutExampleProof

gapt.examples.sequence.LinearCutExampleProof

object LinearCutExampleProof extends ProofSequence

Constructs short FOL LK proofs of the sequents

P(0), ∀x. P(x) → P(s(x)) :- P(s^2 ^n^ ^(0))

where n is an Integer parameter >= 0.

Attributes

Graph
Supertypes: trait ProofSequence

class Object

trait Matchable

class Any
Self type: LinearCutExampleProof.type

Members list

Value members

Concrete methods

Value parameters

left: Which way to associate the cuts.
n: An integer >= 0.

Attributes

Returns: A proof of P(0), ∀x. P(x) → P(s(x)) :- P(s^2 ^m^ ^(0))

Inherited methods

Attributes

Inherited from:: ProofSequence

In this article

Generated with