package fol

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

Type Members

  1. trait FOLAtom extends Expr with FOLPartialAtom with Atom with FOLFormula
  2. trait FOLAtomConst extends Const with HOLAtomConst with FOLPartialAtom
  3. trait FOLConst extends Const with FOLTerm with FOLFunctionConst
  4. trait FOLExpression extends Expr
  5. trait FOLFormula extends Expr with FOLPartialFormula with Formula with FOLExpression
  6. trait FOLFunctionConst extends Const with FOLPartialTerm
  7. trait FOLPartialAtom extends Expr with HOLPartialAtom
  8. trait FOLPartialTerm extends Expr
  9. case class FOLPosition(list: List[Int]) extends Product with Serializable

    Positions are given as lists of Integers.

    Positions are given as lists of Integers. The empty list denotes the current expression itself. A list starting with k denotes a subexpression in the kth argument of the current expression.

    list

    The list describing the position.

  10. trait FOLQuantifier extends Const with LogicalConstant
  11. trait FOLTerm extends Expr with FOLPartialTerm with FOLExpression
  12. trait FOLVar extends Var with FOLTerm
  13. class Hol2FolDefinitions extends AnyRef

    Definitions of the form cₜ(x₁,...,xₙ) := t(x₁,...,xₙ), where c is a constant and t is a term having as only free variables x₁,...,xₙ.

Value Members

  1. object BinaryConnective
  2. object FOLAtom
  3. object FOLAtomConst extends FOLHead
  4. object FOLConst
  5. object FOLFunction
  6. object FOLFunctionArgs

    Unsafely extracts the function arguments from a term.

    Unsafely extracts the function arguments from a term. Fails if the term is not a function.

  7. object FOLFunctionConst extends FOLHead
  8. object FOLFunctionName

    Unsafely extracts the function name from a term.

    Unsafely extracts the function name from a term. Fails if the term is not a function.

  9. object FOLHeadType
  10. object FOLPosition extends Serializable
  11. object FOLVar
  12. object Numeral
  13. object QuantifierStructure
  14. object Utils
  15. object changeTypeIn

    Introducing abstractions and converting to fol changes more complex types to fol compatible ones.

    Introducing abstractions and converting to fol changes more complex types to fol compatible ones. With changeTypeIn you can change them back.

  16. object flatSubterms

    Flat subterms are obtained by decomposing a sequence of applications in one step i.e.

    Flat subterms are obtained by decomposing a sequence of applications in one step i.e. the flat subterms of f x₁ ... xₙ are the term itself and the variables x₁,...,xₙ.

  17. object folTermSize
  18. object getArityOfConstants
  19. object invertBijectiveMap
  20. object isFOLFunction
  21. object isFOLPrenexPi1
  22. object isFOLPrenexSigma1
  23. object isPrenexPi1
  24. object isPrenexSigma1
  25. object naive
  26. object natMaker
  27. object reduceHolToFol

    Creates a FOL formula from a HOL formula, but applies transformations which do _not_ preserve validity! Transformations applied:

    Creates a FOL formula from a HOL formula, but applies transformations which do _not_ preserve validity! Transformations applied:

    • Replace all subterms (\x.t[v]) by a function q_n(v). The scope parameter is needed to pass existing term-constant mappings.
    • Change the type of constants and variables s.t. they are first order (i.e. Const("c", To->Ti) is mapped to FOLConst("c",Ti)
    • Logical operators inside the term structure are replaced by first order terms
    Note

    Make sure you need all of these tricks. To only replace abstraction subterms, use replaceAbstractions.

  28. object replaceAbstractions

    Replace lambda-abstractions by constants.

    Replace lambda-abstractions by constants.

    Each abstraction in an gapt.proofs.HOLSequent is replaced by a separate constant symbol; the used constants are returned in a Map.

  29. object thresholds
  30. object undoHol2Fol

    This is implements some heuristics to convert a fol formula obtained by gapt.expr.formula.fol.replaceAbstractions and gapt.expr.formula.fol.reduceHolToFol back to its original signature.

    This is implements some heuristics to convert a fol formula obtained by gapt.expr.formula.fol.replaceAbstractions and gapt.expr.formula.fol.reduceHolToFol back to its original signature. Sometimes, types have to be guessed and the code is poorly tested, so it is unclear how general it is. It works (and is necessary) during the acnf creation of the n-tape proof.

    To extract a signature, use the undoHol2Fol.getSignature, to to the back translation use undoHol2Fol.backtranslate.

  31. object undoReplaceAbstractions

    Replaces the constants introduced by replaceAbstractions with the original lambda-abstractions.

    Replaces the constants introduced by replaceAbstractions with the original lambda-abstractions.

    Two lambda abstractions that are matching may have the same abstracting constant. However no effort is made to detect matching lambda abstractions in order to minimize the number of definitions.

Ungrouped