edu.cmu.cs.ls.keymaerax.btactics
DifferentialEquationCalculus
Companion trait DifferentialEquationCalculus
object DifferentialEquationCalculus extends DifferentialEquationCalculus
Differential Equation Calculus for differential dynamic logic.
- See also
- Alphabetic
- By Inheritance
- DifferentialEquationCalculus
- 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
- Definition Classes
- DifferentialEquationCalculus
- 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.
- Definition Classes
- DifferentialEquationCalculus
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
- Definition Classes
- DifferentialEquationCalculus
- 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
- Definition Classes
- DifferentialEquationCalculus
- 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
- Definition Classes
- DifferentialEquationCalculus
* ---------------------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
- Definition Classes
- DifferentialEquationCalculus
- 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
- Definition Classes
- DifferentialEquationCalculus
- 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
- Definition Classes
- DifferentialEquationCalculus
- 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
- Definition Classes
- DifferentialEquationCalculus
-
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))
.- Definition Classes
- DifferentialEquationCalculus
- 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
- Definition Classes
- DifferentialEquationCalculus
- See also
-
def
diffInvariant(invariants: List[Formula]): DependentPositionWithAppliedInputTactic
- Definition Classes
- DifferentialEquationCalculus
-
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.
- Definition Classes
- DifferentialEquationCalculus
- 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 (<,>)
- Definition Classes
- DifferentialEquationCalculus
* ---------------------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))
.- Definition Classes
- DifferentialEquationCalculus
- 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))
.- Definition Classes
- DifferentialEquationCalculus
- 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