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

leftRankReduction

gapt.proofs.lk.reductions.leftRankReduction
object leftRankReduction 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 the rank of the cut by permuting it upwards on the left-hand side.

Reduces the rank of the cut by permuting it upwards on the left-hand side.

Value parameters

cut

The proof to which the left rank reduction is applied

Attributes

Returns

A reduced proof or None if the left rank reduction could not be applied.

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