edu.cmu.cs.ls.keymaerax.btactics
DifferentialEquationCalculus
Companion object DifferentialEquationCalculus
trait DifferentialEquationCalculus extends AnyRef
Differential Equation Calculus for differential dynamic logic. Basic axioms for differential equations are in HilbertCalculus.
Provides the elementary derived proof rules for differential equations from Figure 11.20 and Figure 12.9 in: Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
- To do
@Tactic only partially implemented so far
- See also
Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012
Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541-550. IEEE 2012
edu.cmu.cs.ls.keymaerax.core.AxiomBase
- Alphabetic
- By Inheritance
- DifferentialEquationCalculus
- 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
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
dC(R: List[Formula]): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( x$32 , x$33 , x$25 , x$26 , x$27 , x$28 , x$29 , x$34 , x$35 , x$31 , x$36 , x$30 )
-
def
dC(R: Formula): DependentPositionWithAppliedInputTactic
DC: Differential Cut a new invariant, use old(x) to refer to initial values of variable x.
DC: Differential Cut a new invariant, use old(x) to refer to initial values of variable x. Use special function old(.) to introduce a discrete ghost for the starting value of a variable that can be used in the evolution domain constraint.
Use: Show: G |- [x'=f(x)&Q&R]P, D G |- [x'=f(x)&Q]R, D ---------------------------------------------- dC(R) G |- [x'=f(x)&Q]P, D
Also works in context, e.g.:
Use: Show: G |- A->[x'=f(x)&Q&R]P, D G |- A->[x'=f(x)&Q]R, D ---------------------------------------------- dC(R) G |- A->[x'=f(x)&Q]P, D
- R
the formula that will be cut into the differential equation (in that order if it is a list). The formulas are typically shown to be differential invariants subsequently. They can use old(x) and old(y) etc. to refer to the initial values of x and y, respectively.
x>0 |- [{x'=2&x>0}]x>=0 x>0 |- [{x'=2}]x>0 -----------------------------------------------dC("x>0".asFormula)(1) x>0 |- [{x'=2}]x>=0
, x>0, x_0=x |- [{x'=2&x>=x_0}]x>=0 x>0, x_0=x |- [{x'=2}]x>=x_0 -------------------------------------------------------------------dC("x>=old(x)".asFormula)(1) x>0 |- [{x'=2}]x>=0
, x>0, v>=0, x_0=x |- [{x'=v,v'=1&v>=0&x>=x_0}]x>=0 x>0, v>=0 |- [{x'=v,v'=1}]v>=0 x>0, v>=0, x_0=x |- [{x'=v,v'=1&v>=0}]x>=x_0 --------------------------------------------------dC("v>=0".asFormula, "x>=old(x)".asFormula)(1) x>0, v>=0 |- [{x'=v,v'=1}]x>=0
- Note
dC is often needed when FV(post) depend on BV(ode) that are not in FV(constraint).
Examples: -
def
dG(E: Expression, G: Option[Formula]): DependentPositionWithAppliedInputTactic
dG(ghost,r): Differential Ghost add auxiliary differential equations with extra variables ghost of the form y'=a*y+b and the postcondition replaced by r, if provided.
dG(ghost,r): Differential Ghost add auxiliary differential equations with extra variables ghost of the form y'=a*y+b and the postcondition replaced by r, if provided.
G |- \exists y [x'=f(x),y'=g(x,y)&q(x)]r(x,y), D ---------------------------------------------------------- dG using p(x) <-> \exists y. r(x,y) by QE G |- [x'=f(x)&q(x)]p(x), D
- Annotations
- @Tactic( x$80 , x$81 , x$73 , x$74 , x$75 , x$76 , x$77 , x$82 , x$83 , x$78 , x$79 , x$84 )
proveBy("x>0->[{x'=-x}]x>0".asFormula, implyR(1) & dG("{y'=(1/2)*y}".asDifferentialProgram, Some("x*y^2=1".asFormula))(1) & diffInd()(1, 0::Nil) & QE )
with optional instantiation of initial y
proveBy("x>0->[{x'=-x}]x>0".asFormula, implyR(1) & dG("{y'=(1/2)*y}".asDifferentialProgram, Some("x*y^2=1".asFormula))(1) & existsR("1/x^(1/2)".asFormula)(1) & diffInd()(1) & QE )
- Note
Uses QE to prove p(x) <-> \exists y. r(x,y)
Example: -
def
dGold(y: Variable, t1: Term, t2: Term, p: Option[Formula]): DependentPositionWithAppliedInputTactic
- Annotations
- @Tactic( x$85 , x$90 , x$86 , x$88 , x$87 , x$91 , x$92 , x$93 , x$94 , x$95 , x$89 , x$96 )
-
def
dI(auto: Symbol = 'full): DependentPositionTactic
dI: Differential Invariant proves a formula to be an invariant of a differential equation (with the usual steps to prove it invariant).
dI: Differential Invariant proves a formula to be an invariant of a differential equation (with the usual steps to prove it invariant). (uses DI, DW, DE, QE)
- auto
One of 'none, 'diffInd, 'full. Whether or not to automatically close and use DE, DW. 'full: tries to close everything after diffInd rule (turning free variables to constants)
* -------------------------- G |- [x'=f(x)&q(x)]p(x), D
'none: behaves as using DI axiom per cheat sheet
G, q(x) |- p(x), D G, q(x) |- [x'=f(x)&q(x)](p(x))', D --------------------------------------------------------- G |- [x'=f(x)&q(x)]p(x), D
'diffInd: behaves as dI rule per cheat sheet
G, q(x) |- p(x), D q(x) |- [x':=f(x)]p'(x') @note derive on (p(x))' already done ---------------------------------------------- G |- [x'=f(x)&q(x)]p(x), D
* ---------------------diffInd('full)(1) x>=5 |- [{x'=2}]x>=5
, x>=5, true |- x>=5 true |- [{x':=2}]x'>=0 --------------------------------------------diffInd('diffInd)(1) x>=5 |- [{x'=2}]x>=5
, x>=5, true |- x>=5 x>=5, true |- [{x'=2}](x>=5)' ---------------------------------------------------diffInd('none)(1) x>=5 |- [{x'=2}]x>=5
, x>=5 |- [x:=x+1;](true -> x>=5&2>=0) -------------------------------------diffInd('full)(1, 1::Nil) x>=5 |- [x:=x+1;][{x'=2}]x>=5
, proveBy("x^2>=2->[{x'=x^3}]x^2>=2".asFormula, implyR(1) & diffInd()(1) & QE )
- See also
Examples: -
def
dIClose: DependentPositionTactic
dIClose: Differential Invariant proves a formula to be an invariant of a differential equation closing with the usual steps to prove it invariant.
dIClose: Differential Invariant proves a formula to be an invariant of a differential equation closing with the usual steps to prove it invariant. (uses DI, DW, DE, QE). Tries to close everything after diffInd rule (turning free variables to constants)
* -------------------------- dIClose G |- [x'=f(x)&q(x)]p(x), D
- Annotations
- @Tactic( x$56 , x$57 , x$49 , x$50 , x$51 , x$52 , x$53 , x$54 , x$58 , x$55 , x$59 , x$60 )
* ---------------------dIClose(1) x>=5 |- [{x'=2}]x>=5
, x>=5 |- [x:=x+1;](true -> x>=5&2>=0) -------------------------------------dIClose(1, 1::Nil) x>=5 |- [x:=x+1;][{x'=2}]x>=5
- See also
Examples: -
def
dIRule: DependentPositionTactic
dIRule: Differential Invariant proves a formula to be an invariant of a differential equation.
dIRule: Differential Invariant proves a formula to be an invariant of a differential equation. (uses DI, DW, DE).
G, q(x) |- p(x), D q(x) |- [x':=f(x)]p'(x') @note derive on (p(x))' already done ---------------------------------------------- dIRule G |- [x'=f(x)&q(x)]p(x), D
- Annotations
- @Tactic( x$44 , x$45 , x$37 , x$38 , x$39 , x$40 , x$41 , x$42 , x$46 , x$43 , x$47 , x$48 )
x>=5, true |- x>=5 true |- [{x':=2}]x'>=0 --------------------------------------------dIRule(1) x>=5 |- [{x'=2}]x>=5
- See also
Example: -
def
dIX: DependentPositionTactic
- Annotations
- @Tactic( x$61 , x$69 , x$62 , x$63 , x$64 , x$65 , x$66 , x$67 , x$70 , x$68 , x$71 , x$72 )
-
def
dR(formula: Formula, hide: Boolean = true): DependentPositionTactic
Refine top-level antecedent/succedent ODE domain constraint G|- [x'=f(x)&R]P, D G|- [x'=f(x)&Q]R, (D)? ---------------------------------------------- dR G|- [x'=f(x)&Q]P, D
Refine top-level antecedent/succedent ODE domain constraint G|- [x'=f(x)&R]P, D G|- [x'=f(x)&Q]R, (D)? ---------------------------------------------- dR G|- [x'=f(x)&Q]P, D
- formula
the formula R to refine Q to
- hide
whether to keep the extra succedents (D) around (default true), which makes position management easier
-
lazy val
dW: DependentPositionTactic
DW: Differential Weakening uses evolution domain constraint so
[{x'=f(x)&q(x)}]p(x)
reduces to\forall x (q(x)->p(x))
.DW: Differential Weakening uses evolution domain constraint so
[{x'=f(x)&q(x)}]p(x)
reduces to\forall x (q(x)->p(x))
.- Note
FV(post)/\BV(x'=f(x)) subseteq FV(q(x)) usually required to have a chance to succeed.
- See also
-
lazy val
dWPlus: DependentPositionTactic
Same as dW but preserves information about the initial conditions
Same as dW but preserves information about the initial conditions
- See also
- def diffInvariant(invariants: List[Formula]): DependentPositionWithAppliedInputTactic
-
def
diffInvariant(invariant: Formula): DependentPositionWithAppliedInputTactic
DC+DI: Prove the given list of differential invariants in that order by DC+DI via dC followed by dI Combines differential cut and differential induction.
DC+DI: Prove the given list of differential invariants in that order by DC+DI via dC followed by dI Combines differential cut and differential induction. Use special function old(.) to introduce a ghost for the starting value of a variable that can be used in the evolution domain constraint. Uses diffInd to prove that the formulas are differential invariants. Fails if diffInd cannot prove invariants.
- Annotations
- @Tactic( x$102 , x$103 , x$97 , x$98 , x$99 , x$104 , x$105 , x$106 , x$107 , x$101 , x$100 , x$108 )
x>0 |- [{x'=2&x>0}]x>=0 ------------------------diffInvariant("x>0".asFormula)(1) x>0 |- [{x'=2}]x>=0
, x>0, x_0=x |- [{x'=2&x>x_0}]x>=0 ---------------------------------diffInvariant("x>old(x)".asFormula)(1) x>0 |- [{x'=2}]x>=0
, x>0, v>=0, x_0=x |- [{x'=v,v'=1 & v>=0&x>x_0}]x>=0 ---------------------------------------------------diffInvariant("v>=0".asFormula, "x>old(x)".asFormula)(1) x>0, v>=0 |- [{x'=v,v'=1}]x>=0
- See also
Examples: -
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
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
openDiffInd: DependentPositionTactic
DIo: Open Differential Invariant proves an open formula to be an invariant of a differential equation (with the usual steps to prove it invariant) openDiffInd: proves an inequality to be an invariant of a differential equation (by DIo, DW, DE, QE) For strict inequalities, it uses open diff ind (<,>)
DIo: Open Differential Invariant proves an open formula to be an invariant of a differential equation (with the usual steps to prove it invariant) openDiffInd: proves an inequality to be an invariant of a differential equation (by DIo, DW, DE, QE) For strict inequalities, it uses open diff ind (<,>)
* ---------------------openDiffInd(1) x^2>5 |- [{x'=x^3+x^4}]x^2>5
, * ---------------------openDiffInd(1) x^3>5 |- [{x'=x^3+x^4}]x^3>5
, proveBy("x^2>9->[{x'=x^4}]x^2>9".asFormula, implyR(1) & openDiffInd()(1) )
Examples: -
lazy val
solve: DependentPositionTactic
diffSolve: solve a differential equation
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
.diffSolve: solve a differential equation
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
. Similarly,[x'=f(x)&q(x)]p(x)
turns to\forall t>=0 (\forall 0<=s<=t q(solution(s)) -> [x:=solution(t)]p(x))
.- Annotations
- @Tactic( x$1 , x$9 , x$2 , x$3 , x$4 , x$5 , x$6 , x$8 , x$10 , x$7 , x$11 , x$12 )
-
lazy val
solveEnd: DependentPositionTactic
diffSolve with evolution domain check at duration end: solve
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
.diffSolve with evolution domain check at duration end: solve
[x'=f]p(x)
to\forall t>=0 [x:=solution(t)]p(x)
. Similarly,[x'=f(x)&q(x)]p(x)
turns to\forall t>=0 (q(solution(t)) -> [x:=solution(t)]p(x))
.- Annotations
- @Tactic( x$18 , x$19 , x$13 , x$14 , x$15 , x$20 , x$21 , x$17 , x$22 , x$16 , x$23 , x$24 )
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
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 (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