gapt
2.18.0-SNAPSHOT
API
Generated with
gapt/gapt/gapt.proofs/gapt.proofs.lk/gapt.proofs.lk.transformations

gapt.proofs.lk.transformations

package gapt.proofs.lk.transformations

Members list

Type members

Classlikes

class IterativeParallelStrategy(reduction: Reduction) extends ReductionStrategy

Applies the given reduction exhaustively to lowermost redexes.

Applies the given reduction exhaustively to lowermost redexes.

Value parameters

reduction

The reduction to be used by this reduction strategy.

Attributes

Source
reductionStrategies.scala
Supertypes
class Object
trait Matchable
class Any
class IterativeSelectiveStrategy(selector: Selector) extends ReductionStrategy

Attributes

Source
reductionStrategies.scala
Supertypes
class Object
trait Matchable
class Any
object LKToExpansionProof

Attributes

Source
LKToExpansionProof.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object LKToND

Attributes

Source
LKToND.scala
Supertypes
class Object
trait Matchable
class Any
Self type
LKToND.type
class LKToNDTranslationException(name: String, message: String) extends Exception

Attributes

Source
LKToND.scala
Supertypes
class Exception
class Throwable
trait Serializable
class Object
trait Matchable
class Any
Show all
class LeftRankInductionUnfoldingReduction(implicit ctx: Context) extends CutReduction

Attributes

Source
cutNormalization.scala
Supertypes
trait CutReduction
trait Reduction
class Object
trait Matchable
class Any
class LowerMostRedexReducer(reduction: Reduction) extends RedexReducer

Applies a given reduction to the lowermost redexes.

Applies a given reduction to the lowermost redexes.

Value parameters

reduction

The reduction to be applied to the lowermost redexes.

Attributes

Source
reductionStrategies.scala
Supertypes
trait RedexReducer
class Object
trait Matchable
class Any
object MG3iToLJ

Attributes

Source
MG3iToLJ.scala
Supertypes
class Object
trait Matchable
class Any
Self type
MG3iToLJ.type
class ParallelAtDepthStrategy(reduction: Reduction, depth: Int) extends ReductionStrategy

Attributes

Source
reductionStrategies.scala
Supertypes
class Object
trait Matchable
class Any
trait RedexReducer

Describes objects that can apply a reduction to redexes.

Describes objects that can apply a reduction to redexes.

Attributes

Source
reductionStrategies.scala
Supertypes
class Object
trait Matchable
class Any
Known subtypes
trait ReductionStrategy

Attributes

Source
reductionStrategies.scala
Supertypes
class Object
trait Matchable
class Any
Known subtypes
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.

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

Attributes

Source
cutNormalization.scala
Supertypes
class Object
trait Matchable
class Any
trait Selector

Attributes

Source
reductionStrategies.scala
Supertypes
class Object
trait Matchable
class Any
Known subtypes
object StuckCutReduction

Attributes

Source
cutNormalization.scala
Supertypes
class Object
trait Matchable
class Any
Self type
class UnfoldInductions(implicit ctx: Context)

Attributes

Source
cutNormalization.scala
Supertypes
class Object
trait Matchable
class Any
class UppermostFirstStrategy(reduction: Reduction) extends ReductionStrategy

Applies the given reduction exhaustively to uppermost redexes.

Applies the given reduction exhaustively to uppermost redexes.

Value parameters

reduction

The reduction to be used by this reduction strategy.

Attributes

Source
reductionStrategies.scala
Supertypes
class Object
trait Matchable
class Any
object acnf

Attributes

Source
acnf.scala
Supertypes
class Object
trait Matchable
class Any
Self type
acnf.type
object acnfTop

Attributes

Source
acnf.scala
Supertypes
class Object
trait Matchable
class Any
Self type
acnfTop.type
object cleanCuts

Algorithm that removes some unnecessary cuts. At the moment it only removes cuts where one of the premises is a logical axiom.

Algorithm that removes some unnecessary cuts. At the moment it only removes cuts where one of the premises is a logical axiom.

Attributes

Source
cleanCuts.scala
Supertypes
class Object
trait Matchable
class Any
Self type
cleanCuts.type
object cleanStructuralRules

Attributes

Source
cleanStructuralRules.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object cutNormal

Attributes

Source
cutNormalization.scala
Supertypes
class Object
trait Matchable
class Any
Self type
cutNormal.type
object eliminateDefinitions

Eliminates definitions from a lambda expression, HOL formula, or LK proof.

Eliminates definitions from a lambda expression, HOL formula, or LK proof.

Attributes

Companion
class
Source
eliminateDefinitions.scala
Supertypes
class Object
trait Matchable
class Any
Self type
class eliminateDefinitions extends Expr => Expr

Implements definition elimination.

Implements definition elimination.

Attributes

Companion
object
Source
eliminateDefinitions.scala
Supertypes
trait Expr => Expr
class Object
trait Matchable
class Any
object equalityLeftReduction

Attributes

Source
pushEqualityInferencesToLeaves.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object equalityRightReduction

Attributes

Source
pushEqualityInferencesToLeaves.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object folSkolemize

Attributes

Source
folSkolemize.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object inductionNormalForm

Attributes

Source
inductionNormalForm.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object introOrCut

Attributes

Source
acnf.scala
Supertypes
class Object
trait Matchable
class Any
Self type
introOrCut.type
object isAcnf

Attributes

Source
acnf.scala
Supertypes
class Object
trait Matchable
class Any
Self type
isAcnf.type
object isAcnfTop

Attributes

Source
acnf.scala
Supertypes
class Object
trait Matchable
class Any
Self type
isAcnfTop.type
object isAtomicCut

Attributes

Source
acnf.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object makeInductionExplicit

Attributes

Source
makeInductionExplicit.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object makeTheoryAxiomsExplicit

Given a list of formulas Π, this transforms a proof π of Σ :- Δ into a proof π' of Π, Σ :- Δ.

Given a list of formulas Π, this transforms a proof π of Σ :- Δ into a proof π' of Π, Σ :- Δ.

It replaces theory axioms on sequents S that are subsumed by Π with propositional proofs of Π, S.

Attributes

Source
makeTheoryAxiomsExplicit.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object moveStrongQuantifierRulesDown

Modifies an LK proof to introduce strong quantifiers as soon as possible.

Modifies an LK proof to introduce strong quantifiers as soon as possible.

Attributes

Source
moveStrongQuantifierRulesDown.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object pushAllWeakeningsToLeaves

Attributes

Source
PushWeakeningsToLeaves.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object pushEqualityInferencesToLeaves

Attributes

Source
pushEqualityInferencesToLeaves.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object pushEqualityInferencesToLeaves2 extends LKVisitor[Unit]

Attributes

Source
pushEqualityInferencesToLeaves2.scala
Supertypes
trait LKVisitor[Unit]
class Object
trait Matchable
class Any
Self type
object pushSingleWeakeningToLeaves

Attributes

Source
PushWeakeningsToLeaves.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object skolemizeLK

Attributes

Source
skolemizeLK.scala
Supertypes
class Object
trait Matchable
class Any
Self type
object unfoldInduction

Attributes

Companion
class
Source
unfoldInduction.scala
Supertypes
class Object
trait Matchable
class Any
Self type
class unfoldInduction(induction: InductionRule)

Attributes

Companion
object
Source
unfoldInduction.scala
Supertypes
class Object
trait Matchable
class Any
object weakeningOnlySubTree

Attributes

Source
PushWeakeningsToLeaves.scala
Supertypes
class Object
trait Matchable
class Any
Self type
Generated with