package expansion
- Alphabetic
- By Inheritance
- expansion
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Type Members
- sealed abstract class ETt extends AnyRef
Expansion tree term.
Expansion tree term.
This is a compressed representation of expansion trees that does not store formulas or polarity information.
In contrast to expansion trees, expansion tree terms do not have shallow and deep formulas. Rather, there is a (partial) function from term and shallow formula (and polarity) to deep formula.
For example, instead of
ETAtom(hof"P(a)", Polarity.Positive), we just storeETtAtom.As a side effect, the deep methods checks whether an expansion tree term is correct for a given shallow formula (it throws an exception if the term is not correct).
- case class ETtBinary(child1: ETt, child2: ETt) extends ETt with Product with Serializable
Expansion tree term for binary connectives, i.e., ∧, ∨, and →.
- case class ETtDef(shallow: Formula, child: ETt) extends ETt with Product with Serializable
Expansion tree term for definitions.
Expansion tree term for definitions.
- shallow
The shallow formula for
child
- case class ETtMerge(child1: ETt, child2: ETt) extends ETt with Product with Serializable
Expansion tree term for a merge.
- class ETtPrettyPrinter extends BabelExporter
- case class ETtSkolem(skTerm: Expr, child: ETt) extends ETt with Product with Serializable
Expansion tree term for strong quantifiers with Skolem terms.
- case class ETtStrong(eigenVar: Var, child: ETt) extends ETt with Product with Serializable
Expansion tree term for strong quantifiers with eigenvariables.
- case class ETtUnary(child: ETt) extends ETt with Product with Serializable
Expansion tree term for unary connectives, i.e., ¬.
- case class ETtWeak(instances: Map[Expr, ETt]) extends ETt with Product with Serializable
Expansion tree term for weak quantifiers instances.
- case class ExpansionProof(expansionSequent: Sequent[ExpansionTree]) extends Product with Serializable
Expansion proof.
Expansion proof.
An expansion proof consists of a sequent of expansion trees without duplicate eigenvariable where the dependency relation of the eigenvariables is acyclic.
- class ExpansionProofToLK extends SolveUtils
- class ExpansionProofToMG3i extends SolveUtils
- class ExpansionProofToMG3iViaSAT extends AnyRef
- type ExpansionSequent = Sequent[ExpansionTree]
- case class ExpansionTree(term: ETt, polarity: Polarity, shallow: Formula) extends DagProof[ExpansionTree] with Product with Serializable
Expansion tree.
Expansion tree.
A tree collecting instances of a formula. See, e.g., M. Baaz, S. Hetzl, D. Weller: On the complexity of proof deskolemization, Journal of Symbolic Logic, 77(2), 2012 for a formulation close to the one implemented here.
ExpansionTree wraps an expansion tree term together with the intended shallow formula and polarity. The term may not be necessarily correct for this shallow formula (i.e., calling deep may produce an exception). Calling ExpansionTree.check validates the correctness of the expansion tree (also with respect to the given gapt.proofs.context.Context).
The constructors ETAtom, ETAnd, etc. ensure that the produced expansion trees are correct.
- class ExpansionTreePrettyPrinter extends ETtPrettyPrinter
- class InstanceTermEncoding extends AnyRef
Encodes instances of an end-sequent as terms.
Encodes instances of an end-sequent as terms.
Only instances of weak quantifiers are recorded, instances of strong quantifiers or free variables are ignored.
The end-sequent will be internally transformed into one which is in variable normal form.
In the case of cut-introduction, the end-sequent has no free variables and no strong quantifiers and we're encoding a Herbrand sequent as a set of terms. A term r_i(t_1,...,t_n) encodes an instance of the formula "forall x_1 ... x_n, phi(x_1,...,x_n)" using the instances (t_1,...,t_n).
In the case of inductive proofs, the end-sequent contains strong quantifiers variable (alpha). Here, we consider proofs of instance sequents, which are obtained by e.g. substituting a numeral for alpha. Hence the formulas occurring in the end-sequents of instance proofs are substitution instances of endSequent; the encoded terms still only capture the instances used in the instance proofs--i.e. not alpha.
- implicit final class RichExpansionSequent extends AnyVal
Extension class that allows calling shallow and deep on sequents.
Value Members
- val ExpansionSequent: Sequent.type
- object BinaryExpansionTree
- object ETAnd extends ETBinaryCompanion
Expansion tree for ∧.
- object ETAtom
Expansion tree for an atom.
- object ETBottom extends ETNullaryCompanion
Expansion tree for ⊥.
- object ETCut
- object ETDefinition
Expansion tree for a definition node in an expansion tree.
Expansion tree for a definition node in an expansion tree.
It has the form
φ +def Ewhereφis the shallow formula of the definition node. The formulaφshould be definitionally equal to the shallow formula ofE(i.e., equal after unfolding all definitions). - object ETImp extends ETBinaryCompanion
Expansion tree for →.
- object ETInduction
- object ETMerge
Expansion tree merge node, representing a contraction inference.
- object ETMerges
- object ETNeg
Expansion tree for ¬.
- object ETOr extends ETBinaryCompanion
Expansion tree for ∨.
- object ETSkolemQuantifier
Expansion tree for a strong quantifier, containing a Skolem term.
Expansion tree for a strong quantifier, containing a Skolem term.
As an example let us consider an expansion proof of ∀z P(c,z) :- ∃x ∀y P(x,y). For Skolemization we introduce the Skolem function
s_1(for the single strong quantifier), this function has the Skolem definitionλx ∀y P(x,y)(see gapt.logic.hol.SkolemFunctions for details). The natural expansion proof has the deep formulaP(c,s_1(c)) :- P(c,s_1(c)), so we need a Skolem node with the shallow formula∀y P(c,y), and deep formulaP(c,s_1(c)). This Skolem node is constructed asETSkolemQuantifier(∀y P(c,y), s_1(c), λx ∀y P(x,y), ETAtom(P(c,s_1(c)), InSuc)). - object ETStrongQuantifier
Expansion tree for a strong quantifier, containing the eigenvariable.
Expansion tree for a strong quantifier, containing the eigenvariable.
It has the form Qx.A +α E, where α is a variable (called the eigenvariable) and E is an expansion tree of A[x\α].
- object ETStrongQuantifierBlock
Represents nested strong quantifier nodes in an expansion tree, collecting the eigenvariables for a block of strong quantifiers.
- object ETTop extends ETNullaryCompanion
Expansion tree for ⊤.
- object ETWeakQuantifier
Expansion tree collecting the instances for a weak quantifier.
Expansion tree collecting the instances for a weak quantifier.
It has the form Qx.A +t1 E1 + … +tn En, where t1,…,tn are lambda terms of the same type as x and Ei is an expansion tree of A[x\ti].
Its deep formula is E1.deep ∨ … ∨ En.deep (in the case of an existential) or E1.deep ∧ … ∧ En.deep (in the case of a universal).
- object ETWeakQuantifierBlock
Represents nested weak quantifier nodes in an expansion tree, collecting the instances for a block of weak quantifiers.
- object ETWeakening
Expansion tree representing a weakening inference.
- object ETt
- case object ETtAtom extends ETt with Product with Serializable
Expansion tree term for an atom.
- object ETtMerge extends Serializable
- case object ETtNullary extends ETt with Product with Serializable
Expansion tree term for nullary connectives, i.e., ⊤ and ⊥.
- object ETtWeak extends Serializable
- case object ETtWeakening extends ETt with Product with Serializable
Expansion tree term for a weakening.
- object ExpansionProof extends Serializable
- object ExpansionProofToLK extends ExpansionProofToLK
- object ExpansionProofToMG3i
- object ExpansionProofToMG3iViaSAT
- object ExpansionTree extends Serializable
- object InstanceTermEncoding
- object PropositionalExpansionProofToLK extends ExpansionProofToLK
- object addSymmetry
Given an expansion sequent S which is a tautology modulo symmetry of equality, returns an expansion sequent S' which is S extended by the symmetry instances needed to make it a tautology.
- object atomicExpansionET
- object cleanStructureET
Cleans up an expansion tree by introducing weakenings as late as possible.
- object commuteReplacementCtxWithDefEq
- object deskolemizeET
Deskolemization of expansion trees.
Deskolemization of expansion trees.
We first gather the skolem terms in a given ExpansionProof from the ETSkolemQuantifiers. Then replace each ETSkolemQuantifier by ETStrongQuantifier, and each skolem term within, by a fresh eigenvariable.
- object eigenVariablesET
Returns the eigenvariables in an expansion tree or expansion sequent.
- object eliminateCutsET
- object eliminateDefsET
- object eliminateMerges
Reduces merge nodes in an expansion proof.
- object extractInstances
Extracts the instances used in a prenex FOL Pi_1 expansion tree / Sigma_1 expansion sequent.
Extracts the instances used in a prenex FOL Pi_1 expansion tree / Sigma_1 expansion sequent.
Each expansion tree is transformed into a list of instances of its shallow formula.
In contrast to ExpansionProof.deep, this function doesn't produce conjunctions of instances, but instead increases the number of formulas in the antecedent/succedent.
- object findMerges
Extracts all merge ETs from an expansion proof.
- object formulaToExpansionTree
- object freeVariablesET
- object generalizeET
- object groundTerms
- object insertDefinition
Inserts a definition into an expansion tree by either creating an ETDefinition node at the appropriate place or else just replacing terms.
- object instReplCtx
Instantiates the quantifier inside a replacement context.
Instantiates the quantifier inside a replacement context.
Given λx ∀y P(x,y) and f(c), it will return λx P(x,f(c)).
- object isPropositionalET
- object minimalExpansionSequent
Given an expansion sequent S, this algorithm computes a single expansion sequents below S that is valid and minimal.
Given an expansion sequent S, this algorithm computes a single expansion sequents below S that is valid and minimal. This algorithm is considerably faster than the one implemented in minimalExpansionSequents.
- object minimalExpansionSequents
Given an expansion sequent S, this algorithm computes the list of expansion sequents below S that are valid and minimal.
- object moveDefsUpward
- object moveSkolemNodesToCuts
- object nonProofTheoreticSkolemTerms
- object numberOfInstancesET
- object prenexifyET
- object pushWeakeningsUp
- object removeSkolemCongruences
- object replaceAtHOLPosition
- object replaceWithContext
Replaces terms in an expansion tree according to a replacement context.
- object tautAtomicExpansionET
- object unifyInstancesET
Decreases the number of instances in an expansion proof by unifying the instance terms.
This is the API documentation for GAPT.
The main package is gapt.