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
- Alphabetic
- By Inheritance
- Provable
- Serializable
- Serializable
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
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
-
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)
-
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."
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
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_)
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): scala.Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
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*
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
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.
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
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()
-
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()
-
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*
-
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)
-
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
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
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*
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
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
-
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 structuresExpression
- Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (one-pass) 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 first-order logicHybridProgramCalculus
- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
- Unification-based 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 back-end solversMathematicaQETool
- Mathematica interface for real arithmetic.Z3QETool
- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
- Extended back-ends 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
- Command-line launcher for KeYmaera X supports command-line argument-help
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
- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface 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. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David 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. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos