Packages

p

gapt.proofs

resolution

package resolution

Source
package.scala
Linear Supertypes
AnyRef, Any
Content Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. resolution
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. case class AllL(subProof: ResolutionProof, idx: SequentIndex, skolemTerm: Expr) extends SkolemQuantResolutionRule with Product with Serializable
  2. case class AllR(subProof: ResolutionProof, idx: SequentIndex, variable: Var) extends WeakQuantResolutionRule with Product with Serializable
  3. case class AndL(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  4. case class AndR1(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  5. case class AndR2(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  6. case class AvatarComponent(component: AvatarDefinition) extends InitialClause with Product with Serializable

    Introduces a clause component.

    Introduces a clause component.

    ------
C <- a
  7. case class AvatarContradiction(subProof: ResolutionProof) extends LocalResolutionRule with Product with Serializable

    Moves an assertion back to the sequent.

    Moves an assertion back to the sequent.

      S <- A
------------
 S ++ ¬A <-
  8. trait AvatarDefinition extends AnyRef

    Clause component together with its associated propositional atom.

  9. abstract class AvatarGeneralNonGroundComp extends AvatarDefinition
  10. case class AvatarGroundComp(atom: Atom, polarity: Polarity) extends AvatarDefinition with Product with Serializable
  11. case class AvatarNegNonGroundComp(atom: Atom, definition: Formula, vars: Seq[Var], idx: SequentIndex) extends AvatarGeneralNonGroundComp with Product with Serializable
  12. case class AvatarNonGroundComp(atom: Atom, definition: Formula, vars: Seq[Var]) extends AvatarGeneralNonGroundComp with Product with Serializable
  13. case class AvatarSplit(subProof: ResolutionProof, indices: Set[SequentIndex], component: AvatarDefinition) extends LocalResolutionRule with Product with Serializable

    Removes a clause component.

    Removes a clause component.

    S ++ C <- A
----------------
   S   <- A ∧ ¬a
  14. case class BottomR(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  15. class Clausifier extends AnyRef
  16. case class DefIntro(subProof: ResolutionProof, idx: SequentIndex, definition: Definition, args: Seq[Expr]) extends PropositionalResolutionRule with Product with Serializable

    Definition introduction.

    Definition introduction.

    Γ :- Δ, φ(x)
--------
Γ :- Δ, D(x)

    This inference should only be used on descendants of Input inferences.

  17. case class Defn(defConst: HOLAtomConst, definition: Expr) extends InitialClause with Product with Serializable

    Definition.

    Definition.

    ---------------------
:- ∀x (D(x) <-> φ(x))
  18. case class ExL(subProof: ResolutionProof, idx: SequentIndex, variable: Var) extends WeakQuantResolutionRule with Product with Serializable
  19. case class ExR(subProof: ResolutionProof, idx: SequentIndex, skolemTerm: Expr) extends SkolemQuantResolutionRule with Product with Serializable
  20. case class Factor(subProof: ResolutionProof, idx1: SequentIndex, idx2: SequentIndex) extends LocalResolutionRule with Product with Serializable

    Factoring.

    Factoring.

    l, l, Γ :- Δ
-----------
l, Γ :- Δ
  21. case class Flip(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  22. case class ImpL1(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  23. case class ImpL2(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  24. case class ImpR(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  25. abstract class InitialClause extends LocalResolutionRule
  26. case class Input(sequent: HOLSequent) extends InitialClause with Product with Serializable

    Input sequent.

    Input sequent.

    -------
sequent
  27. abstract class LocalResolutionRule extends ResolutionProof with ContextRule[Formula, ResolutionProof]
  28. case class NegL(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  29. case class NegR(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  30. case class OrL1(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  31. case class OrL2(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  32. case class OrR(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  33. case class Paramod(subProof1: ResolutionProof, eqIdx: SequentIndex, leftToRight: Boolean, subProof2: ResolutionProof, auxIdx: SequentIndex, context: Expr) extends LocalResolutionRule with Product with Serializable

    Paramodulation.

    Paramodulation.

    Γ :- Δ, t=s     Π :- Λ, l[t]
----------------------------
     Γ, Π :- Δ, Λ, l[s]
  34. abstract class PropositionalResolutionRule extends LocalResolutionRule
  35. case class Refl(term: Expr) extends InitialClause with Product with Serializable

    Reflexivity.

    Reflexivity.

    --------------
:- term = term
  36. case class Resolution(subProof1: ResolutionProof, idx1: SequentIndex, subProof2: ResolutionProof, idx2: SequentIndex) extends LocalResolutionRule with Product with Serializable

    Resolution.

    Resolution.

    Γ :- Δ, a    a, Π :- Λ
----------------------
      Γ, Π :- Δ, Λ
  37. class Resolution2RalWithAbstractions extends ResolutionToRal

    A converter from resolution proofs to Ral proofs, which reintroduces the lambda abstractions which we removed for the fol export.

  38. trait ResolutionProof extends SequentProof[Formula, ResolutionProof] with DagProof[ResolutionProof]

    Proof using resolution.

    Proof using resolution.

    Our resolution calculus integrates higher-order reasoning, structural clausification, and Avatar-style splitting as in [Vor14].

    The judgments of this calculus are A-sequents. An A-sequent is a pair of a sequent of HOL formulas, and a conjunction of propositional literals---the assertion (that's where the "A" comes from).

    Γ :- Δ <- A

    We store the sequent as a HOLSequent in ResolutionProof#conclusion, and the negation of the assertion as a HOLClause in ResolutionProof#assertions (as the negation of a conjunction of literals is a clause). The judgment is interpreted as one of the following equivalent formulas:

    assertions.toNegConjunction --> conclusion.toDisjunction
(conclusion ++ assertions).toDisjunction   // equivalent to the first one

    Inferences such as Resolution or Paramod do not operate on the assertions. Unless specified otherwise, assertions are inherited by default:

    Γ :- Δ, a <- A       a, Π :- Λ <- B
--------------------------------
      Γ, Π :- Δ, Λ <- A ∧ B

    There is no factoring on assertions, duplicate assertions are automatically removed.

    Reading from top to bottom, a resolution proof is usually structured as follows:

    Substitutions are not absorbed into resolution, factoring, and paramodulation; they are explicitly represented using Subst.

    [Vor14] Andrei Voronkov, AVATAR: The Architecture for First-Order Theorem Provers. CAV 2014: pp. 696-710

  39. class ResolutionProofVisitor extends AnyRef
  40. abstract class ResolutionToRal extends AnyRef
  41. abstract class SkolemQuantResolutionRule extends PropositionalResolutionRule
  42. trait SkolemQuantResolutionRuleCompanion extends AnyRef
  43. case class Subst(subProof: ResolutionProof, substitution: Substitution) extends ResolutionProof with Product with Serializable

    Substitution.

    Substitution.

           Γ :- Δ
----------------------
substitution(Γ :- Δ)
  44. case class Taut(formula: Formula) extends InitialClause with Product with Serializable

    Tautology.

    Tautology.

    -------------------
formula :- formula
  45. case class TopL(subProof: ResolutionProof, idx: SequentIndex) extends PropositionalResolutionRule with Product with Serializable
  46. abstract class WeakQuantResolutionRule extends PropositionalResolutionRule

Value Members

  1. object AllL extends SkolemQuantResolutionRuleCompanion with Serializable
  2. object AllR extends Serializable
  3. object AvatarNonGroundComp extends Serializable
  4. object AvatarSplit extends Serializable
  5. object ExR extends SkolemQuantResolutionRuleCompanion with Serializable
  6. object ExpansionToResolutionProof

    Converts an expansion proof to a resolution proof.

  7. object Factor extends Serializable
  8. object Flip extends Serializable
  9. object MguFactor
  10. object MguResolution
  11. object PCNF

    Given a sequent s and a clause a in CNF(-s), PCNF computes an LK proof of a subsequent of s ++ a containing at least a

  12. object Paramod extends Serializable
  13. object Resolution extends Serializable
  14. object Resolution2RalWithAbstractions

    A converter from Robinson resolution proofs to Ral proofs, which reintroduces the lambda abstractions which we removed for the fol export.

  15. object ResolutionToExpansionProof

    Converts a resolution proof to an expansion proof.

    Converts a resolution proof to an expansion proof. ResolutionToExpansionProof( rp ) will return the expansion proof of rp and ResolutionToExpansionProof( rp, input ) is used by the CERES method to return the expansion proof of the ACNF, which is extracted from the proof projections.

    Let us first ignore splitting and subformula definitions for simplicity. However we may still have clausification inferences. The conversion then proceeds bottom-up through the resolution proof (to be precise: in a reverse post-order traversal).

    At each point in the algorithm, we associate with every subproof a set of expansion sequents and associated substitutions, i.e. we keep a Map[ResolutionProof, Set[(Substitution, ExpansionSequent)] ] with the following properties: 1. the conjunction of all deep sequents (each interpreted as a disjunction) is unsatisfiable, and 2. the substitution applied to the shallow sequent is always equal to the conclusion of the subproof.

    In every step we consider a subproof, empty its Set[(Substitution, ExpansionSequent)], and add in exchange the appropriate sets to its premises, while keeping the invariant. In this manner, these sets propagate upwards through the proof to the input sequents.

    Let us first consider the common case that the input sequents are ground unit sequents: i.e. if we obtained a resolution proof for ∀x A(x), ∀x B(x) :- ∀x C(x), then we would have the input sequents :- ∀x A(x), :- ∀x B(x), and ∀x C(x) :-. When we have finally propagated all the sets up to the input sequents, the invariant guarantees the following: we have expansion sequents with the input sequents as shallow sequents (at this point we use the requirement that the input sequents are ground), such that the conjunction of the deep sequents (interpreted as disjunctions) is unsatisfiable. This immediately implies that if we combine the expansions of the input sequents into a sequent, we get an expansion proof of ∀x A(x), ∀x B(x) :- ∀x C(x).

    In the unlikely case that the resolution proof starts from clauses, we just pretend that the clauses are derived from formulas--that is, we instead of beginning with D(x), E(x,y) :- F(y) we just imagine the proof begins with :- ∀x ∀y (¬D(x) ∨ ¬E(x,y) ∨ F(y)).

    Splitting inferences are converted to cuts in the expansion proof: formally, we can first skip all the splitting inferences in the resoltion proof; the assertions now become part of the clauses, and we get additional input sequents. For example, consider the clauses :- A(x), B(y), A(c) :-, and B(c) :-. The natural way to refute these clauses is to split the first clause into :- A(x) <-- s1 and :- B(y) <-- s2, then perform unit resolution twice, and then have a propositional contradiction. After skipping the splitting inferences we would get a proof starting from :- s1, s2, s1 :- A(x), s2 :- B(x), A(c) :-, and B(c) :-. If we replace s1 := ∀x A(x) and s2 := ∀x B(x) everywhere in the resulting expansion proof, then we can package up the expansions of s1 :- A(x) and s2 :- B(x) as cuts. The other clauses are then precisely the clause we had before splitting.

    Subformula definitions are eliminated after the conversion to expansion proofs, see gapt.proofs.expansion.eliminateDefsET.

  16. object ResolutionToLKProof
  17. object ResolutionToRal extends ResolutionToRal
  18. object Subst extends Serializable
  19. object UnitResolutionToLKProof
  20. implicit object avatarComponentsAreReplaceable extends ClosedUnderReplacement[AvatarDefinition]
  21. object containsEquationalReasoning
  22. object eliminateSplitting

    Eliminate AvatarSplit, AvatarComponent, AvatarContradiction splitting inferences from a resolution proof.

  23. object expansionProofFromInstances
  24. object findDerivationViaResolution
  25. object fixDerivation

    Sometimes, we have a resolution refutation R of a set of clauses C and want a refutation R' of a set C' such that C implies C'.

    Sometimes, we have a resolution refutation R of a set of clauses C and want a refutation R' of a set C' such that C implies C'.

    This algorithm tries to obtain R' by trying to replace clauses c from C in R by derivations of C from C'.

    In general, if R is a derivation of a clause c, the result R' of fixDerivation(R) is a derivation of a subclause of c.

  26. object forgetfulPropParam
  27. object forgetfulPropResolve
  28. object mapInputClauses
  29. object numberOfLogicalInferencesRes
  30. implicit object resolutionProofsAreReplaceable extends ClosedUnderReplacement[ResolutionProof]
  31. object simplifyResolutionProof
  32. object structuralCNF
  33. object tautologifyInitialUnitClauses

Inherited from AnyRef

Inherited from Any

Ungrouped