package fol
- Alphabetic
- Public
- Protected
Type Members
- trait FOLAtom extends Expr with FOLPartialAtom with Atom with FOLFormula
- trait FOLAtomConst extends Const with HOLAtomConst with FOLPartialAtom
- trait FOLConst extends Const with FOLTerm with FOLFunctionConst
- trait FOLExpression extends Expr
- trait FOLFormula extends Expr with FOLPartialFormula with Formula with FOLExpression
- trait FOLFunctionConst extends Const with FOLPartialTerm
- trait FOLPartialAtom extends Expr with HOLPartialAtom
- trait FOLPartialTerm extends Expr
- 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.
- trait FOLQuantifier extends Const with LogicalConstant
- trait FOLTerm extends Expr with FOLPartialTerm with FOLExpression
- trait FOLVar extends Var with FOLTerm
- 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
- object BinaryConnective
- object FOLAtom
- object FOLAtomConst extends FOLHead
- object FOLConst
- object FOLFunction
- 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.
- object FOLFunctionConst extends FOLHead
- 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.
- object FOLHeadType
- object FOLPosition extends Serializable
- object FOLVar
- object Numeral
- object QuantifierStructure
- object Utils
- 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.
- 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ₙ.
- object folTermSize
- object getArityOfConstants
- object invertBijectiveMap
- object isFOLFunction
- object isFOLPrenexPi1
- object isFOLPrenexSigma1
- object isPrenexPi1
- object isPrenexSigma1
- object naive
- object natMaker
- 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.
- 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.
- object thresholds
- 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 useundoHol2Fol.backtranslate
. - 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.
This is the API documentation for GAPT.
The main package is gapt.