package reduction
- Alphabetic
- Public
- Protected
Type Members
- case class CombinedReduction[-P1, P2, +P3, +S1, S2, -S3](red1: Reduction[P1, P2, S1, S2], red2: Reduction[P2, P3, S2, S3]) extends Reduction[P1, P3, S1, S3] with Product with Serializable
Sequential composition of reductions.
Sequential composition of reductions.
This class is not intended to be used directly, but via the Reduction#|> operator.
- case class HOFunctionReduction(extraAxioms: Boolean = true) extends OneWayReduction_[HOLSequent] with Product with Serializable
Replaces the use of higher-order functions by fresh function symbols, together with axioms that axiomatize them.
- case class HOFunctionReductionCNFRes(extraAxioms: Boolean = true) extends Reduction_[Set[HOLSequent], ResolutionProof] with Product with Serializable
Replaces the use of higher-order functions by fresh function symbols, together with axioms that axiomatize them.
- case class HOFunctionReductionET(extraAxioms: Boolean = true) extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable
Replaces the use of higher-order functions by fresh function symbols, together with axioms that axiomatize them.
- case class HOFunctionReductionRes(extraAxioms: Boolean = true) extends Reduction_[HOLSequent, ResolutionProof] with Product with Serializable
Replaces the use of higher-order functions by fresh function symbols, together with axioms that axiomatize them.
- case class LambdaEliminationReduction(extraAxioms: Boolean = true) extends OneWayReduction_[HOLSequent] with Product with Serializable
Replaces lambda abstractions by fresh function symbols, together with axioms that axiomatize them.
- case class LambdaEliminationReductionCNFRes(extraAxioms: Boolean = true) extends Reduction_[Set[HOLSequent], ResolutionProof] with Product with Serializable
Replaces lambda abstractions by fresh function symbols, together with axioms that axiomatize them.
- case class LambdaEliminationReductionET(extraAxioms: Boolean = true) extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable
Replaces lambda abstractions by fresh function symbols, together with axioms that axiomatize them.
- case class LambdaEliminationReductionRes(extraAxioms: Boolean = true) extends Reduction_[HOLSequent, ResolutionProof] with Product with Serializable
Replaces lambda abstractions by fresh function symbols, together with axioms that axiomatize them.
- trait OneWayReduction_[P] extends Reduction[P, P, Nothing, Any]
A reduction without back-translation.
- case class PredicateTranslation(context: Context) extends Product with Serializable
Sets up the predicate reduction for first-order multi-sorted languages.
Sets up the predicate reduction for first-order multi-sorted languages.
- context
The context for which the predicate translation is to be constructed.
- trait Reduction[-P1, +P2, +S1, -S2] extends AnyRef
Represents a reduction of a problem together with a back-translation of the solutions.
Represents a reduction of a problem together with a back-translation of the solutions.
A problem P1 is reduced to a problem P2, a solution S2 to the problem P2 can then be translated back to a solution S1 of the problem P1.
- trait Reduction_[P, S] extends Reduction[P, P, S, S]
A reduction that does not change the type of the problem.
Value Members
- case object CNFReductionExpRes extends Reduction[HOLSequent, Set[HOLClause], ExpansionProof, ResolutionProof] with Product with Serializable
Reduces finding an expansion proof for a sequent to finding a resolution proof of a clause set.
- case object CNFReductionLKRes extends Reduction[HOLSequent, Set[HOLClause], LKProof, ResolutionProof] with Product with Serializable
Reduces finding an LK proof for a sequent to finding a resolution proof of a clause set.
- case object CNFReductionResRes extends Reduction[HOLSequent, Set[HOLClause], ResolutionProof, ResolutionProof] with Product with Serializable
Reduces finding a resolution proof for a sequent to finding a resolution proof of a clause set.
- case object CNFReductionSequentsResRes extends Reduction[Set[HOLSequent], Set[HOLClause], ResolutionProof, ResolutionProof] with Product with Serializable
Reduces finding a resolution proof for a sequent set to finding a resolution proof of a clause set.
- case object ErasureReductionCNF extends Reduction_[Set[HOLClause], ResolutionProof] with Product with Serializable
Reduces finding a resolution proof of a many-sorted clause set to the first-order case.
Reduces finding a resolution proof of a many-sorted clause set to the first-order case.
Sorts are simply ignored and we make a best effort to convert the resolution refutation back.
- case object ErasureReductionET extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable
Reduces finding an expansion proof of a many-sorted sequent to the first-order case.
Reduces finding an expansion proof of a many-sorted sequent to the first-order case.
Sorts are simply ignored and we make a best effort to convert the expansion tree.
- case object GroundingReductionET extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable
Simplifies the problem by grounding free variables.
- case object PredicateReductionCNF extends Reduction_[Set[HOLClause], ResolutionProof] with Product with Serializable
Simplifies the problem of finding a resolution refutation of a many-sorted clause set by adding predicates for each of the sorts.
Simplifies the problem of finding a resolution refutation of a many-sorted clause set by adding predicates for each of the sorts. The resulting problem is still many-sorted.
- case object PredicateReductionET extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable
Simplifies the problem of finding an expansion proof of a many-sorted sequent by adding predicates for each of the sorts.
Simplifies the problem of finding an expansion proof of a many-sorted sequent by adding predicates for each of the sorts. The resulting problem is still many-sorted.
- case object TagReductionCNF extends Reduction_[Set[HOLClause], ResolutionProof] with Product with Serializable
- case object TagReductionET extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable
- object guessContext
This is the API documentation for GAPT.
The main package is gapt.