LinearExampleProof

gapt.examples.sequence.LinearExampleProof

Constructs cut-free 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.

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods

def apply(n: Int): LKProof

Value parameters

n

An integer >= 0.

Attributes

Returns

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

Inherited methods

def name: String

Attributes

Inherited from:
ProofSequence