trait ProvableSig extends AnyRef
A common signature for edu.cmu.cs.ls.keymaerax.pt.ProvableSig's and TermProvable's for use in the btactics package. This allows for tactics to construct proof terms or not depending on which implementation they use.
This file mimics edu.cmu.cs.ls.keymaerax.core.Provable outside the core and forwards all operations to the core.
 See also
Provable
 Alphabetic
 By Inheritance
 ProvableSig
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

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

abstract
def
apply(prolongation: ProvableSig): ProvableSig
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.

abstract
def
apply(newConsequence: Sequent, rule: Rule): ProvableSig
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.
 abstract def apply(ren: URename): ProvableSig

abstract
def
apply(subst: USubst): ProvableSig
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.
 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."

abstract
def
apply(subderivation: ProvableSig, subgoal: Subgoal): ProvableSig
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.

abstract
def
apply(rule: Rule, subgoal: Subgoal): ProvableSig
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.

abstract
val
axioms: Map[String, ProvableSig]
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
 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."

abstract
val
conclusion: Sequent
the conclusion
G  D
that follows if all subgoals are valid.  abstract val defs: Declaration

abstract
def
prettyString: String
<invalid inheritdoc annotation>
 abstract def proveArithmetic(t: QETool, f: Formula): ProvableSig

abstract
def
proveArithmeticLemma(t: QETool, f: Formula): Lemma
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.
 t
The quantifierelimination tool.
 f
The formula.
 returns
a Lemma with a quantifierfree formula equivalent to f and evidence as provided by the tool.

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

abstract
val
rules: Map[String, ProvableSig]
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
 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(USubst)

abstract
def
startProof(goal: Formula): ProvableSig
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.

abstract
def
startProof(goal: Sequent): ProvableSig
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.
 abstract val steps: Int

abstract
def
sub(subgoal: Subgoal): ProvableSig
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.

abstract
val
subgoals: IndexedSeq[Sequent]
the premises
Gi  Di
that, if they are all valid, imply the conclusion.
Concrete 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(fw: (ProvableSig) ⇒ ProvableSig): ProvableSig
Apply forward tactic on all subgoals.

def
apply(fw: (ProvableSig) ⇒ ProvableSig, subgoal: Subgoal): ProvableSig
Apply forward tactic
fw
atsubgoal
. 
final
def
asInstanceOf[T0]: T0
 Definition Classes
 Any

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)

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

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

def
equals(arg0: Any): Boolean
 Definition Classes
 AnyRef → Any

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

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

def
hashCode(): Int
 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.
 See also
Provable.isProved

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

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

final
def
notifyAll(): Unit
 Definition Classes
 AnyRef
 Annotations
 @native()

def
reapply(defs: Declaration): ProvableSig
Returns a copy of this provable with the definitions replaced by
defs
. 
def
reapply(underlying: Provable): ProvableSig
Returns a copy of this provable with the underlying provable replaced by
underlying
. 
final
def
synchronized[T0](arg0: ⇒ T0): T0
 Definition Classes
 AnyRef

def
toString(): String
 Definition Classes
 AnyRef → Any

val
underlyingProvable: Provable
The core's Provable that this object really represents.

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

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

final
def
wait(arg0: Long): 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 structuresExpression
 Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
 Sequents of formulasProvable
 Proof certificates transformed by rules/axiomsRule
 Proof rules as well asUSubstOne
for (onepass) uniform substitutions and renaming.StaticSemantics
 Static semantics with free and bound variable analysisKeYmaeraXParser
.edu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter
 Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser
 Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser
 Parser reading KeYmaera X model and proof archive.kyx
filesDLParser
 Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
 Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.cmu.cs.ls.keymaerax.infrastruct
 Prover infrastructure outside the kernelUnificationMatch
 Unification algorithmRenUSubst
 Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context
 Representation for contexts of formulas in which they occur.Augmentors
 Augmenting formula and expression data structures with additional functionalityExpressionTraversal
 Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreterBelleExpr
 Tactic language expressionsSequentialInterpreter
 Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics
 Bellerophon tactic library for conducting proofs.TactixLibrary
 Main KeYmaera X tactic library including many proof tactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicSequentCalculus
 Sequent Calculus for propositional and firstorder logicHybridProgramCalculus
 Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
 Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
 Unificationbased uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]
 Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismLemma
 Lemmas are Provables stored under a name, e.g., in files.LemmaDB
 Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe
 Real arithmetic backend solversMathematicaQETool
 Mathematica interface for real arithmetic.Z3QETool
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
 Extended backends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica
 Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3
 Z3 interface for real arithmetic including simplifiers.Entry Points
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.AxIndex
 Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex
 Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax
 Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at 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, volume 9195 of LNCS, pp. 527538. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018. Videos