Generated with

gapt/gapt/gapt.proofs/gapt.proofs.lk/gapt.proofs.lk.transformations/ReductiveCutNormalization

ReductiveCutNormalization

gapt.proofs.lk.transformations.ReductiveCutNormalization

class ReductiveCutNormalization(cleanStructuralRules: Boolean, unfoldInduction: Boolean)(implicit val ctx: Context)

This class implements a version of Gentzen's cut-reduction procedure for our sequent calculus LK.

Attributes

Source: cutNormalization.scala
Graph
Supertypes: class Object

trait Matchable

class Any

Members list

Type members

Classlikes

Attributes

Source: cutNormalization.scala
Supertypes: trait CutReduction

trait Reduction

class Object

trait Matchable

class Any
Self type: emptyCutReduction.type

Value members

Concrete methods

Applies Gentzen's reductive cut-elimination to a proof.

Applies Gentzen's reductive cut-elimination to a proof.

Value parameters

proof: The proof that is subject to cut-elimination.

Attributes

Returns: If the input proof is an LK proof, then a cut-free proof is returned, otherwise the resulting proof may not be cut-free.
Source: cutNormalization.scala

Concrete fields

Attributes

Source: cutNormalization.scala

Implicits

Implicits

Attributes

Source: cutNormalization.scala

In this article

Generated with