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.
Branching proofs in backward tableaux sequent order are straightforward, yet might become more readable when closing branches righttoleft 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) )
, Proofs in Hilbertcalculus 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)
, 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)
, Proofs in backward tableaux sequent order are straightforward
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)
, 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)
, 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
,soundnesscritical logical framework.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
 Alphabetic
 By Inheritance
 Provable
 Serializable
 Serializable
 Product
 Equals
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

type
Subgoal = Int
Position types for the subgoals of a Provable.
Value Members

final
def
!=(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

final
def
##(): Int
 Definition Classes
 AnyRef → Any

final
def
==(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

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 followsG1  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 soundnesscritical derived function since implemented in terms of other apply functions

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 followsG1  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 soundnesscritical derived function since implemented in terms of other apply functions

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
soundnesscritical. And soundnesscritical 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. 219266, 2017. Theorem 26+27."

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
soundnesscritical

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
soundnesscritical. And soundness needs Rule to be sealed.

final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

def
clone(): AnyRef
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @native() @throws( ... )
 val conclusion: Sequent

final
def
eq(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

def
finalize(): scala.Unit
 Attributes
 protected[java.lang]
 Definition Classes
 AnyRef
 Annotations
 @throws( classOf[java.lang.Throwable] )

final
def
getClass(): Class[_]
 Definition Classes
 AnyRef → Any
 Annotations
 @native()

final
def
isInstanceOf[T0]: Boolean
 Definition Classes
 Any

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
soundnesscritical

final
def
ne(arg0: AnyRef): Boolean
 Definition Classes
 AnyRef

final
def
notify(): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

final
def
notifyAll(): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @native()
 def prettyString: String

final
def
proved: Sequent
What conclusion this Provable proves if isProved.

def
sub(subgoal: Subgoal): Provable
SubProvable: Get a subProvable corresponding to a Provable with the given subgoal as conclusion.
SubProvable: Get a subProvable 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 soundnesscritical only helpful for completenesscritical
 val subgoals: IndexedSeq[Sequent]

final
def
synchronized[T0](arg0: ⇒ T0): T0
 Definition Classes
 AnyRef

def
toString(): String
 Definition Classes
 Provable → AnyRef → Any

final
def
wait(): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @throws( ... )

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

final
def
wait(arg0: Long): scala.Unit
 Definition Classes
 AnyRef
 Annotations
 @native() @throws( ... )
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core
 KeYmaera X kernel, proof certificates, main data structuresedu.cmu.cs.ls.keymaerax.core.Expression
 Differential dynamic logic expressionsedu.cmu.cs.ls.keymaerax.core.Sequent
 Sequents of formulasedu.cmu.cs.ls.keymaerax.core.Rule
 Proof rulesedu.cmu.cs.ls.keymaerax.core.Provable
 Proof certificateedu.cmu.cs.ls.keymaerax.btactics
 Tactic language libraryedu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
 Main tactic libraryedu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicedu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
 Sequent Calculus for propositional and firstorder logicedu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus
 Unificationbased Uniform Substitution Calculusedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreteredu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr
 Tactic language expressionsedu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
 Sequential tactic interpreteredu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
 Parser for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter
 Pretty printer for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser
 Parser for KeYmaera X problem files.kyx
edu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismedu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB
 Lemma database stored in filesedu.cmu.cs.ls.keymaerax.tools
 Arithmetic backendsedu.cmu.cs.ls.keymaerax.tools.Mathematica
 Mathematica interface for real arithmetic and ODE solver etc.edu.cmu.cs.ls.keymaerax.tools.Z3
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.Polya
 Polya interface for real arithmetic.Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX
 Commandline launcher for KeYmaera X supports commandline argumenthelp
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.References
Full references are provided elsewhere http://keymaeraX.org/, the main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219265, 2017.
2. Nathan Fulton, Stefan Mitsch, JanDavid Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.