gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.lk/gapt.proofs.lk.reductions/LeftRankInductionReduction

LeftRankInductionReduction

gapt.proofs.lk.reductions.LeftRankInductionReduction
object LeftRankInductionReduction extends CutReduction

Attributes

Source
rankReduction.scala
Graph
Supertypes
trait CutReduction
trait Reduction
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods

def apply(cut: CutRule): Option[LKProof]

Reduces a cut by moving the cut towards the proof's leaves.

Reduces a cut by moving the cut towards the proof's leaves.

Value parameters

ctx

The proof's context.

cut

The cut to be reduced.

Attributes

Returns

A reduced proof if the given cut is reducible w.r.t to some induction inference, otherwise None.

Source
rankReduction.scala
override def reduce(proof: CutRule): Option[LKProof]

Attributes

Definition Classes
Source
rankReduction.scala

Inherited methods

def andThen(reduction: CutReduction): CutReduction

Attributes

Inherited from:
CutReduction
Source
CutReduction.scala
def andThen(reduction: Reduction): Reduction

Attributes

Inherited from:
Reduction
Source
Reduction.scala
def isRedex(proof: LKProof): Boolean

Attributes

Inherited from:
Reduction
Source
Reduction.scala
def orElse(reduction: CutReduction): CutReduction

Attributes

Inherited from:
CutReduction
Source
CutReduction.scala
def orElse(reduction: Reduction): Reduction

Attributes

Inherited from:
Reduction
Source
Reduction.scala
def redexes(proof: LKProof): Seq[LKProof]

Attributes

Inherited from:
Reduction
Source
Reduction.scala
def reduce(proof: LKProof): Option[LKProof]

Attributes

Inherited from:
CutReduction
Source
CutReduction.scala
Generated with