Packages

final case class Provable extends Product with Serializable

Provable(conclusion, subgoals) is the proof certificate representing certified provability of conclusion from the premises in subgoals. If subgoals is an empty list, then conclusion is provable. Otherwise conclusion is provable from the set of all assumptions in subgoals.

 G1 |- D1 ... Gn |- Dn    (subgoals)
-----------------------
         G |- D           (conclusion)

Invariant: All Provables ever produced are locally sound, because only the prover kernel can create Provable objects and chooses not to use the globally sound uniform substitution rule.

Examples:
  1. Branching proofs in backward tableaux sequent order are straight-forward, yet might become more readable when closing branches right-to-left to keep explicit subgoals:

    // explicit proof certificate construction of |- !!p() <-> p()
    val proof = (Provable.startProof(
      "!!p() <-> p()".asFormula)
      (EquivRight(SuccPos(0)), 0)
      // right branch
        (NotRight(SuccPos(0)), 1)
        (NotLeft(AntePos(1)), 1)
        (Close(AntePos(0),SuccPos(0)), 1)
      // left branch
        (NotLeft(AntePos(0)), 0)
        (NotRight(SuccPos(1)), 0)
        (Close(AntePos(0),SuccPos(0)), 0)
    )
  2. ,
  3. Proofs in Hilbert-calculus style order can also be based exclusively on subsequent merging

    import scala.collection.immutable._
    val fm = Greater(Variable("x"), Number(5))
    // x>0 |- x>0
    val left = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(fm)))(
      Close(AntePos(0), SuccPos(0)), 0)
    // |- true
    val right = Provable.startProof(Sequent(IndexedSeq(), IndexedSeq(True)))(
      CloseTrue(SuccPos(0)), 0)
    val right2 = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(True)))(
      HideLeft(AntePos(0)), 0) (right, 0)
    // gluing order for subgoals is irrelevant. Could use: (right2, 1)(left, 0))
    val merged = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(And(fm, True))))(
      AndRight(SuccPos(0)), 0) (
      left, 0)(
        right2, 0)
    // |- x>5 -> x>5 & true
    val finGoal = new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True))))
    val proof = Provable.startProof(finGoal)(
      ImplyRight(SuccPos(0)), 0) (merged, 0)
    // proof of finGoal
    println(proof.proved)
  4. ,
  5. Proofs in forward Hilbert order are straightforward with merging of branches

    import scala.collection.immutable._
    val fm = Greater(Variable("x"), Number(5))
    // proof of x>5 |- x>5 & true merges left and right branch by AndRight
    val proof = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(And(fm, True))))(
      AndRight(SuccPos(0)), 0) (
      // left branch: x>5 |- x>5
      Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(fm)))(
        Close(AntePos(0), SuccPos(0)), 0),
      0) (
      //right branch: |- true
      Provable.startProof(Sequent(IndexedSeq(), IndexedSeq(True)))(
        CloseTrue(SuccPos(0)), 0)(
          // x>5 |- true
          Sequent(IndexedSeq(fm), IndexedSeq(True)), HideLeft(AntePos(0))),
      0) (
      // |- x>5 -> x>5 & true
      new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True)))),
      ImplyRight(SuccPos(0))
    )
    // proof of finGoal:  |- x>5 -> x>5 & true
    println(proof.proved)
  6. ,
  7. Proofs in backward tableaux sequent order are straight-forward

    import scala.collection.immutable._
    val fm = Greater(Variable("x"), Number(5))
    // |- x>5 -> x>5 & true
    val finGoal = new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True))))
    // conjecture
    val finProvable = Provable.startProof(finGoal)
    // construct a proof
    val proof = finProvable(
      ImplyRight(SuccPos(0)), 0)(
        AndRight(SuccPos(0)), 0)(
        HideLeft(AntePos(0)), 1)(
        CloseTrue(SuccPos(0)), 1)(
        Close(AntePos(0), SuccPos(0)), 0)
    // proof of finGoal
    println(proof.proved)
  8. ,
  9. Multiple Provable objects for subderivations obtained from different sources can also be merged

    // ... continuing other example
    val more = new Sequent(IndexedSeq(),
      IndexedSeq(Imply(Greater(Variable("x"), Number(5)), True)))
    // another conjecture
    val moreProvable = Provable.startProof(more)
    // construct another (partial) proof
    val moreProof = moreProvable(ImplyRight(SuccPos(0)), 0)(HideLeft(AntePos(0)), 0)
    // merge proofs by gluing their Provables together
    val mergedProof = moreProof(proof, 0)
    // check if proof successful
    if (mergedProof.isProved) println("Successfully proved " + mergedProof.proved)
  10. ,
  11. Proofs can be constructed in (backward/tableaux) sequent order using Provables:

    import scala.collection.immutable._
    val verum = new Sequent(IndexedSeq(), IndexedSeq(True))
    // conjecture
    val provable = Provable.startProof(verum)
    // construct a proof
    val proof = provable(CloseTrue(SuccPos(0)), 0)
    // check if proof successful
    if (proof.isProved) println("Successfully proved " + proof.proved)
Note

For soundness: No reflection should bypass constructor call privacy, nor reflection to bypass immutable val algebraic data types.

,

Only private constructor calls for soundness

,

soundness-critical logical framework.

See also

Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Provable
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. type Subgoal = Int

    Position types for the subgoals of a Provable.

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def apply(prolongation: Provable): Provable

    Substitute Subderivation Forward: Prolong this Provable with the given prolongation.

    Substitute Subderivation Forward: Prolong this Provable with the given prolongation. This Provable with conclusion G |- D transforms as follows

      G1 |- D1 ... Gn |- Dn                  G1 |- D1 ... Gn |- Dn
    -------------------------       =>     -------------------------
             G |- D                                 G0 |- D0

    provided

             G |- D
    ------------------------- prolongation
            G0 |- D0
    prolongation

    the subderivation used to prolong this Provable. Where subderivation has a subgoal equaling our conclusion.

    returns

    A Provable derivation that proves prolongation's conclusion from our subgoals.

    Note

    not soundness-critical derived function since implemented in terms of other apply functions

  5. def apply(newConsequence: Sequent, rule: Rule): Provable

    Apply Rule Forward: Apply given proof rule forward in Hilbert style to prolong this Provable to a Provable for concludes.

    Apply Rule Forward: Apply given proof rule forward in Hilbert style to prolong this Provable to a Provable for concludes. This Provable with conclusion G |- D transforms as follows

      G1 |- D1 ... Gn |- Dn                  G1 |- D1 ... Gn |- Dn
    -------------------------       =>     -------------------------
             G |- D                              newConsequence

    provided

             G |- D
    ------------------------- rule
          newConsequence
    newConsequence

    the new conclusion that the rule shows to follow from this.conclusion

    rule

    the proof rule to apply to concludes to reduce it to this.conclusion.

    returns

    A Provable derivation that proves concludes from the same subgoals by using the given proof rule. Will return a Provable with the same subgoals but an updated conclusion.

    Note

    not soundness-critical derived function since implemented in terms of other apply functions

  6. final def apply(subst: USubst): Provable

    Apply a uniform substitution to a (locally sound!) Provable.

    Apply a uniform substitution to a (locally sound!) Provable. Substitutes both subgoals and conclusion with the same uniform substitution subst.

     G1 |- D1 ... Gn |- Dn              s(G1) |- s(D1) ... s(Gn) |- s(Dn)
    -----------------------     =>     -----------------------------------   (USR)
             G |- D                                s(G) |- s(D)
    subst

    The uniform substitution (of no free variables) to be used on the premises and conclusion of this Provable.

    returns

    The Provable resulting from applying subst to our subgoals and conclusion.

    Note

    soundness-critical. And soundness-critical that only locally sound Provables can be constructed (otherwise implementation would be more complicated).

    See also

    Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017. Theorem 26+27."

  7. final def apply(subderivation: Provable, subgoal: Subgoal): Provable

    Substitute subderivation as a proof of subgoal.

    Substitute subderivation as a proof of subgoal. Merge: Replace premise subgoal by the given subderivation. Use the given provable derivation in place of the indicated subgoal of this Provable, returning the resulting concatenated Provable.

    In particular, if subderivation.isProved, then the given subgoal will disappear, otherwise it will be replaced by the subgoals of subderivation (with the first subgoal of subderivation in place of subgoal and all other subgoals at the end).

    This function implements the substitution principle for hypotheses.

     G1 |- D1 ... Gi |- Di ... Gn |- Dn              G1 |- D1 ... Gr1 |- Dr1 ... Gn |- Dn Gr2 |- Dr2 ... Grk | Drk
    ------------------------------------     =>     ---------------------------------------------------------------
                   G |- D                                         G |- D

    using the given subderivation

    Gr1 |- Dr1  Gr2 |- Dr2 ... Grk |- Drk
    ------------------------------------ (subderivation)
                 Gi |- Di
    subderivation

    the Provable derivation that proves premise subgoal.

    subgoal

    the index of our subgoal that the given subderivation concludes.

    returns

    A Provable derivation that joins our derivation and subderivation to a joint derivation of our conclusion using subderivation to show our subgoal. Will return a Provable with the same conclusion but an updated set of premises.

    Note

    soundness-critical

  8. final def apply(rule: Rule, subgoal: Subgoal): Provable

    Apply Rule: Apply given proof rule to the indicated subgoal of this Provable, returning the resulting Provable

    Apply Rule: Apply given proof rule to the indicated subgoal of this Provable, returning the resulting Provable

     G1 |- D1 ... Gi |- Di ... Gn |- Dn              G1 |- D1 ... Gr1 |- Dr1 ... Gn |- Dn Gr2 |- Dr2 ... Grk | Drk
    ------------------------------------     =>     ---------------------------------------------------------------
                   G |- D                                         G |- D

    using the rule instance

    Gr1 |- Dr1  Gr2 |- Dr2 ... Grk |- Drk
    ------------------------------------ (rule)
                 Gi |- Di
    rule

    the proof rule to apply to the indicated subgoal of this Provable derivation.

    subgoal

    which of our subgoals to apply the given proof rule to.

    returns

    A Provable derivation that proves the premise subgoal by using the given proof rule. Will return a Provable with the same conclusion but an updated set of premises.

    Note

    soundness-critical. And soundness needs Rule to be sealed.

  9. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  10. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  11. val conclusion: Sequent
  12. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  13. def finalize(): scala.Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  14. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  16. final def isProved: Boolean

    Checks whether this Provable proves its conclusion.

    Checks whether this Provable proves its conclusion.

    returns

    true if conclusion is proved by this Provable, false if subgoals are missing that need to be proved first.

    Note

    soundness-critical

  17. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. final def notify(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  19. final def notifyAll(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. def prettyString: String
  21. final def proved: Sequent

    What conclusion this Provable proves if isProved.

  22. def sub(subgoal: Subgoal): Provable

    Sub-Provable: Get a sub-Provable corresponding to a Provable with the given subgoal as conclusion.

    Sub-Provable: Get a sub-Provable corresponding to a Provable with the given subgoal as conclusion. Provables resulting from the returned subgoal can be merged into this Provable to prove said subgoal.

    subgoal

    the index of our subgoal for which to return a new open Provable.

    returns

    an initial unfinished open Provable for the subgoal i:

     Gi |- Di
    ----------
     Gi |- Di

    which is suitable for being merged back into this Provable for subgoal i subsequently.

    Note

    not soundness-critical only helpful for completeness-critical

  23. val subgoals: IndexedSeq[Sequent]
  24. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  25. def toString(): String
    Definition Classes
    Provable → AnyRef → Any
  26. final def wait(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  27. final def wait(arg0: Long, arg1: Int): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. final def wait(arg0: Long): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Ungrouped