Packages

package hol

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Package Members

  1. package dls

Type Members

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

  2. case class fastStructuralCNF(propositional: Boolean = true, bidirectionalDefs: Boolean = false) extends Product with Serializable

Value Members

  1. object AndOr
  2. 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.

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

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

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

  6. object SkolemFunctions extends Serializable
  7. 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.

  8. object moveQuantifiers
  9. object removeRedundantQuantifiers
  10. object simplifyPropositional

    Simplify a Formula using the equations for bottom and top as well as idempotence of conjunction and disjunction.

  11. object skolemize
  12. 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.

  13. object toNNF

    Transforms a formula to negation normal form (transforming also implications into disjunctions)

Ungrouped