Packages

p

gapt.proofs

reduction

package reduction

Content Hierarchy
Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Type Members

  1. 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.

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. 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.

  7. 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.

  8. 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.

  9. 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.

  10. trait OneWayReduction_[P] extends Reduction[P, P, Nothing, Any]

    A reduction without back-translation.

  11. 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.

  12. 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.

  13. trait Reduction_[P, S] extends Reduction[P, P, S, S]

    A reduction that does not change the type of the problem.

Value Members

  1. 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.

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. 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.

  7. case object GroundingReductionET extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable

    Simplifies the problem by grounding free variables.

  8. 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.

  9. 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.

  10. case object TagReductionCNF extends Reduction_[Set[HOLClause], ResolutionProof] with Product with Serializable
  11. case object TagReductionET extends Reduction_[HOLSequent, ExpansionProof] with Product with Serializable
  12. object guessContext

Ungrouped