package hol
- Alphabetic
- Public
- Protected
Type Members
- case class SkolemFunctions(skolemDefs: Map[Const, Expr]) extends Product with Serializable
List of definitions of Skolem symbols.
List of definitions of Skolem symbols.
A Skolem definition is similar but slightly different from the epsilon operator:
Syntactically it is a map s_i → λx_1 .. λx_n Qy φ(x_1, .., x_n, y), where Q is a quantifier. Then s_i(x_1, .., x_n) is the Skolem term used for the formula Qy φ(x_1, .., x_n, y), where Qy is strong.
This Skolem term corresponds to the epsilon term εy φ(x_1, .., x_n, y) or εy ¬φ(x_1, .., x_n), depending on whether Q is ∃ or ∀. The reason we don't use epsilon terms directly is that this makes it impossible to deskolemize a formula based on just the Skolem definitions: for example both ∃x ∀y φ and ∃x ¬∃y¬ φ would define their Skolem functions using the same epsilon terms.
- case class fastStructuralCNF(propositional: Boolean = true, bidirectionalDefs: Boolean = false) extends Product with Serializable
Value Members
- object AndOr
- object CNFn
Computes a negative CNF of a formula, i.e.
Computes a negative CNF of a formula, i.e. one that is logically equivalent to the negation of the input formula.
The computation is done by expanding the input formula using distributivity.
- object CNFp
Computes a positive CNF of a formula, i.e.
Computes a positive CNF of a formula, i.e. one that is logically equivalent to the input formula.
The computation is done by expanding the input formula using distributivity.
- object DNFn
Computes a negative DNF of a formula, i.e.
Computes a negative DNF of a formula, i.e. one that is logically equivalent to the negation of the input formula.
The computation is done by expanding the input formula using distributivity.
- object DNFp
Computes a positive DNF of a formula, i.e.
Computes a positive DNF of a formula, i.e. one that is logically equivalent to the input formula.
The computation is done by expanding the input formula using distributivity.
- object SkolemFunctions extends Serializable
- object isOrevkovClass1
Checks whether a sequent is in (a minor extension of) Orevkov's class 1.
Checks whether a sequent is in (a minor extension of) Orevkov's class 1.
This is a Glivenko class, i.e., whenever this function returns true for a first-order formula, then that formula is provable in intuitionistic logic iff it is provable in classical logic.
- object moveQuantifiers
- object removeRedundantQuantifiers
- object simplifyPropositional
Simplify a Formula using the equations for bottom and top as well as idempotence of conjunction and disjunction.
- object skolemize
- object solveFormulaEquation
Takes a formula equation F[X₁,...,Xₙ] and if successful returns a substitution of the second order variables X_1,...,X_n such that applying the substitution to F is a valid first-order formula.
Takes a formula equation F[X₁,...,Xₙ] and if successful returns a substitution of the second order variables X_1,...,X_n such that applying the substitution to F is a valid first-order formula. See dls for a detailed description when this succeeds and when it fails. In addition, this method uses Escargot to check if the found first-order formula is valid and returns a Failure, if it is not.
- object toNNF
Transforms a formula to negation normal form (transforming also implications into disjunctions)
This is the API documentation for GAPT.
The main package is gapt.