Packages

object Provable extends Serializable

Starting new Provables to begin a proof, either with unproved conjectures or with proved axioms or axiomatic proof rules.

See also

Provable.axioms

Provable.rules

Provable$.startProof(goal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

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

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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. val axiom: Map[String, Formula]

    immutable list of sound axioms, i.e., valid formulas of differential dynamic logic.

    immutable list of sound axioms, i.e., valid formulas of differential dynamic logic. (convenience method)

  6. val axioms: Map[String, Provable]

    immutable list of Provables of sound axioms, i.e., valid formulas of differential dynamic logic.

    immutable list of Provables of sound axioms, i.e., valid formulas of differential dynamic logic.

        *
---------- (axiom)
 |- axiom
    Note

    soundness-critical: only valid formulas are sound axioms.

    See also

    "Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. arXiv 1503.01981, 2015."

  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. final def diffAdjoint(dim: Int): Provable

    Axiom schema for differential adjoints, schematic in given dimension.

    Axiom schema for differential adjoints, schematic in given dimension.

    <{x_'=f_(x_) & q_(x_)}>x_=y_ <-> <{y_'=-f_(y_) & q_(y_)}>x_=y_
    dim

    The dimension of ODE x_'=f_(x_)

  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  11. def finalize(): scala.Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  12. final def fromStorageString(storedProvable: String): Provable

    Parses a Stored Provable String representation back again as a Provable.

    Parses a Stored Provable String representation back again as a Provable. Soundness depends on the fact that the String came from toStorageString(), which is checked in a lightweight fashion using checksums.

    storedProvable

    The String obtained via toStorageString(fact:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable):String*.

    returns

    The Provable that represents storedProvable.

    Exceptions thrown

    ProvableStorageException if storedProvable is illegal.

    See also

    Provable.toStorageString(fact:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable):String*

  13. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. final def implicitFunc(f: Function, pr: Provable): Provable

    Existence-guarded axiom schema for defining equality of interpreted functions, schematic in the function.

    Existence-guarded axiom schema for defining equality of interpreted functions, schematic in the function.

    *
--- (with proof of |- \\exists x_ P(x_,._1,...,._n))
|- ._0 = f<< P(._0,._1,...,._n) >>(._1,...,._n)  <->  P(.0,._1,...,._n)
    f

    the interpreted function

    pr

    the proof of existence of the function's value.

  16. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  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. final def proveArithmetic(tool: QETool, f: Formula): Provable

    Proves a formula f in real arithmetic using an external tool for quantifier elimination.

    Proves a formula f in real arithmetic using an external tool for quantifier elimination.

           *
-------------- (tool)
 |- f<->QE(f)
    tool

    The quantifier-elimination tool that computes the equivalent QE(f).

    f

    The formula.

    returns

    a Provable with an equivalence of f to the quantifier-free formula equivalent to f, justified by tool.

    See also

    QETool.quantifierElimination()

  21. val rules: Map[String, Provable]

    immutable list of Provables of locally sound axiomatic proof rules.

    immutable list of Provables of locally sound axiomatic proof rules.

     Gi |- Di
---------- (axiomatic rule)
  G |- D
    Note

    soundness-critical: only list locally sound rules.

    See also

    "Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. arXiv 1503.01981, 2015."

    Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubstOne):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

  22. def startProof(goal: Formula): Provable

    Begin a new proof for the desired conclusion formula from no antecedent.

    Begin a new proof for the desired conclusion formula from no antecedent.

     |- goal
---------
 |- goal
    goal

    the desired conclusion formula for the succedent.

    returns

    a Provable whose subgoals need to be all proved in order to prove goal.

    Note

    Not soundness-critical (convenience method)

  23. final def startProof(goal: Sequent): Provable

    Begin a new proof for the desired conclusion goal

    Begin a new proof for the desired conclusion goal

     goal
------
 goal
    goal

    the desired conclusion.

    returns

    a Provable whose subgoals need to be all proved in order to prove goal.

    Note

    soundness-critical

  24. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  25. final def toStorageString(fact: Provable): String

    Stored Provable representation as a string of the given Provable that will reparse correctly.

    Stored Provable representation as a string of the given Provable that will reparse correctly.

    Note

    If store printer is injective function, then only fact reparses via fromStorageString unless checksum modified or not injective.

    See also

    Provable.fromStorageString(storedProvable:String):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

  26. def toString(): String
    Definition Classes
    AnyRef → Any
  27. final def vectorialDG(dim: Int): (Provable, Provable)

    Axiom schema for vectorial differential ghosts, schematic in dimension.

    Axiom schema for vectorial differential ghosts, schematic in dimension. Schema returns two Provables, one for each direction of the differential ghost axiom. This reduces duplication of code constructing the ghost vectors.

    [{y_'=g(||),c{|y_|}&q(|y_|)}] (||y_||^2) <= f(|y_|)
-> ( [{y_'=g(||),c{|y_|}&q(|y_|)}]p(|y_|) -> [{c{|y_|}&q(|y_|)}]p(|y_|) )

[{c{|y_|}&q(|y_|)}]p(|y_|) -> [{y_'=g(||),c{|y_|}&q(|y_|)}]p(|y_|)
    dim

    The number of ghost variables

  28. final def wait(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long, arg1: Int): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from AnyRef

Inherited from Any

Ungrouped