object ODEInvariance
Implements ODE tactics based on the differential equation axiomatization.
Created by yongkiat on 05/14/18.
- See also
Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.
- Alphabetic
- By Inheritance
- ODEInvariance
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- case class Conj(left: Instruction, right: Instruction) extends Instruction with Product with Serializable
- case class ConjFml(left: Inst, right: Inst) extends Inst with Product with Serializable
- case class Darboux(is_eq: Boolean, cofactor: Term, pr: ProvableSig) extends Instruction with Product with Serializable
- case class Disj(left: Instruction, right: Instruction) extends Instruction with Product with Serializable
- case class DisjFml(left: Inst, right: Inst) extends Inst with Product with Serializable
- case class EqFml(rank: Int, groebner: List[Term], cofactors: List[List[Term]]) extends Inst with Product with Serializable
- case class GeqFml(rank: Int, groebner: List[Term], cofactors: List[List[Term]]) extends Inst with Product with Serializable
- case class GtFml(rank: Int) extends Inst with Product with Serializable
- sealed trait Inst extends AnyRef
- sealed trait Instruction extends AnyRef
- case class Strict(bound: Int) extends Instruction with Product with Serializable
- case class Triv() extends Instruction with Product with Serializable
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 affine_norm_bound(n: Int): ProvableSig
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
cauchy_schwartz_bound(n: Int): ProvableSig
Pre-prove the symbolic lemmas for n-dimensional Cauchy Schwartz Note: this lemma proves pretty quickly e.g.
Pre-prove the symbolic lemmas for n-dimensional Cauchy Schwartz Note: this lemma proves pretty quickly e.g. for n=10
- n
the dimension to use
- returns
the symbolic bound (u.v)2 <= (||u||||v||)2
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
- lazy val dCClosure: DependentPositionTactic
-
val
dFP: DependentPositionTactic
Implements differential fixed point
Implements differential fixed point
G, x=x0 |- [x'=f(x)& Q & x=x0]P G|-f(x)=0 --- (dFP) G |- [x'=f(x)&Q]P
-
val
dRI: DependentPositionTactic
Implements (conjunctive) differential radical invariants
Implements (conjunctive) differential radical invariants
G,Q |- /\_i p_i*=0 --- (dRI) G |- [x'=f(x)&Q]/\_i p_i=0
This proof rule is complete for open semialgebraic domain constraints Q This requires a top-level postcondition which rearranges to be a conjunction of equalities
- See also
Khalil Ghorbal, Andrew Sogokon, and André Platzer. Invariance of conjunctions of polynomial equalities for algebraic differential equations.
- def dgVdbx(Gco: List[List[Term]], ps: List[Term], negate: Boolean = false): DependentPositionTactic
- val dgVdbxAuto: DependentPositionTactic
- def diffDivConquer(p: Term, cofactor: Option[Term] = None): DependentPositionTactic
-
def
domainStuck: DependentPositionTactic
- Annotations
- @Tactic( x$28 , x$29 , x$30 , x$25 , x$26 , x$31 , x$32 , x$27 , x$33 , x$34 , x$35 , x$36 )
- def dot_prod(v1: List[Term], v2: List[Term]): Term
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
fStar(ode: ODESystem, f: Formula): (Formula, Inst)
Given a formula f in normal form (conjunction/disjunction of >=0, >0 or =0), generates the formula f* This is accompanied by an extra data structure that caches additional information at each step
Given a formula f in normal form (conjunction/disjunction of >=0, >0 or =0), generates the formula f* This is accompanied by an extra data structure that caches additional information at each step
- ode
: the ODE system
- f
: the formula in semialgebraic normal form
- returns
: (f*, i)
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
def
frobenius_subord_bound(n: Int): (ProvableSig, ProvableSig)
Pre-prove the following double-sided bound: -(||G||2+1) ||p||2 <= 2*((Gp).p) <= (||G||2+1) ||p||2
Pre-prove the following double-sided bound: -(||G||2+1) ||p||2 <= 2*((Gp).p) <= (||G||2+1) ||p||2
The arithmetic is guided as follows: For each row (G_i.p)2 <= ||G_i||2 ||p||2 (Cauchy Schwartz) Which implies ||Gp||2 = sum_i (G_i.p)2 <= sum_i ||G_i||2 ||p||^2
Then since ((Gp).p)2 <= ||Gp||2 ||p||2 (Cauchy Schwartz) This yields ((Gp).p)2 <= (sum_i ||G_i||2) ||p||2 ||p||^2
Then use a usubst lemma to get: 2((Gp).p) <= (1+sum_i ||G_i||2) ||p||2 and also: 2((Gp).p) >= -(1+sum_i ||G_i||2) ||p||2
- n
the dimension to use
- returns
the symbolic bounds (||G||2 + 1) ||p||2 <= 2*((Gp).p) <= (||G||2 + 1) ||p||2
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getDiffAdjInst(odels: List[AtomicODE]): ProvableSig
Get the correct instantiation of diff adjoints from a list of atomic ODEs
Get the correct instantiation of diff adjoints from a list of atomic ODEs
- odels
the list of atomic ODEs
- returns
the instantiated axiom
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def linFormODE(p: DifferentialProgram): Option[(List[List[Term]], List[Term], List[BaseVariable])]
-
def
localProgressFml(ode: ODESystem, f: Formula, bound: Option[Int] = None): Formula
Computes the local progress formula f* f* is assumed to consist of atomic comparisons normalized to have 0 on RHS (<=0,>=0,<0,>0,=0,!=0), And, Or Sub-formulas outside this grammar are ignored if strict = false
Computes the local progress formula f* f* is assumed to consist of atomic comparisons normalized to have 0 on RHS (<=0,>=0,<0,>0,=0,!=0), And, Or Sub-formulas outside this grammar are ignored if strict = false
- ode
: the ODEs under consideration
- f
: the formula f to compute f* for
- bound
: optionally bounds the number of higher Lie derivatives that are considered
- def lpgen(inst: Inst): BelleExpr
- def lpstep: DependentPositionTactic
- def matvec_prod(m: List[List[Term]], v: List[Term]): List[Term]
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def nilpotentSolve(solveEnd: Boolean): DependentPositionTactic
-
val
nilpotentSolveTimeVar: Variable
Given a top-level succedent position corresponding to [x'=f(x)&Q]P with x'=f(x) a linear, nilpotent ODE
Given a top-level succedent position corresponding to [x'=f(x)&Q]P with x'=f(x) a linear, nilpotent ODE
Adds the (polynomial) solution x=Phi(x_0,t) of that ODE to the domain constraint
--- QE Q(Phi(x_0,t)), t>=0 |- P(Phi(x_0,t)) --- (only continues if solveEnd = true) G,x=x_0, t=0 |- [x'=f(x),t'=1& Q&t>=0& x=Phi(x_0,t)]P --------------- (nilpotent solve) G |- [x'=f(x)&Q]P
- returns
See the rule rendition above Special failure cases: 1) Linearity heuristic checks fail e.g.: x'=1+x2-x2 will be treated as non-linear even though it is really linear
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
pStar(ode: ODESystem, p: Term, bound: Option[Int], geq: Boolean = true): Formula
Given a bound i, generate the local progress formula up to that bound i.e.
Given a bound i, generate the local progress formula up to that bound i.e. the i-th Lie derivative is strict: p>=0 & (p=0 -> (p'>=0 & (p'=0 -> ...) & (p=0&... -> p'^i >0) Computes up to the rank if bound = None
- ode
: the ODEs under consideration
- p
: the polynomial p to generate p*>0
- bound
: number of higher Lie derivatives to generate
- geq
: generate for >= (or <= if false)
- returns
( p*>0 )
-
def
pStarGeq(ode: ODESystem, p: Term): (Formula, (Int, List[Term], List[List[Term]]))
Given a polynomial p, and an ODE system, generates the formula p*>0 along with additional information for p*=0 (as provided by rank(ode,p)) -- this avoids recomputation of the cofactors The rank r is reduced according to equalities already present in the domain constraint In other words, the generated p* satisfies: <x'=f(x)&Q>O & p*>=0 -> <x'=f(x)& p>=0 >O
Given a polynomial p, and an ODE system, generates the formula p*>0 along with additional information for p*=0 (as provided by rank(ode,p)) -- this avoids recomputation of the cofactors The rank r is reduced according to equalities already present in the domain constraint In other words, the generated p* satisfies: <x'=f(x)&Q>O & p*>=0 -> <x'=f(x)& p>=0 >O
- ode
: the ODE system
- p
: the polynomial p
- returns
: (p*>0, p*=0, rank)
-
def
pStarHom(ode: DifferentialProgram, p: Term, bound: Int): Formula
Homomorphically extend pStar to max and min terms
Homomorphically extend pStar to max and min terms
- ode
: the ODEs under consideration
- p
: the term p>=0 (including max/min terms)
- bound
: number of higher Lie derivatives to generate
- returns
p*>0
-
def
rank(ode: ODESystem, polys: List[Term]): (Int, List[Term], List[List[Term]])
Explicitly calculate the conjunctive rank of a list of polynomials (uses conjunctive optimization from SAS'14)
Explicitly calculate the conjunctive rank of a list of polynomials (uses conjunctive optimization from SAS'14)
- ode
the ODESystem to use
- polys
the polynomials to compute rank for
- returns
the (conjunctive) rank, the Groebner basis closed under Lie derivation, and its cofactors (in that order)
- def rankOneFml(ode: DifferentialProgram, dom: Formula, f: Formula): Option[Formula]
- def rewriteODEAt(ode2: DifferentialProgram): DependentPositionTactic
-
def
sAI: DependentPositionTactic
Given a top-level succedent position corresponding to [x'=f(x)&Q]P
Given a top-level succedent position corresponding to [x'=f(x)&Q]P
G|-P Q,Q*,P |- P* Q,Q-*, !P |- (!P)-* --------------- (sAI) G |- [x'=f(x)&Q]P
- returns
closes the subgoal if P is indeed invariant,
- See also
Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.
-
def
sAIRankOne(doReorder: Boolean = true, skipClosed: Boolean = true): DependentPositionTactic
Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a semialgebraic invariant, i.e.
Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a semialgebraic invariant, i.e. G|- [x'=f(x)&Q]P P is assumed to be formed from conjunctions, disjunctions and inequalities This does not go via (closed) real induction, and so also applies for strict inequalities However, all of the sub formulas need to be "recursively" rank 1, i.e. they are provable either: 1) with darboux inequalities p'>=qp (for p>=0 , p>0) 2) with a barrier certificate
This tactic reorders conjunctions internally to try and find an order that works
- doReorder
whether to reorder conjunctions
- skipClosed
whether to skip over closed invariants (this should be used if the outer tactic already tried sAIclosedPlus, which is much faster than this one anyway) The option only applies if doReorder = true
- See also
Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.
-
def
sAIclosed: DependentPositionTactic
Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e.
Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e. G|- [x'=f(x)&Q]P
G|-P Q,P |- P* --------------- (sAIc) G |- [x'=f(x)&Q]P
P is assumed to be formed from conjunctions, disjunction, p<=q, p>=q, p=q which are collectively normalized to f>=0 (f possibly involving max,min and abs)
TODO: Add Q* to the antecedents in the second premise
- returns
closes the subgoal if P is indeed invariant, This should only fail if either: 1) P fails to normalize to f>=0 form (it isn't closed) 2) it is not invariant
- See also
Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.
-
def
sAIclosedPlus(bound: Int = 1): DependentPositionTactic
Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e.
Given a top-level succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e. G|- [x'=f(x)&Q]P P is assumed to be formed from conjunctions, disjunction, p<=q, p>=q, p=q which are collectively normalized to f>=0 (f possibly involving max,min and abs)
Current tactic limitations: 1) Assumes that P is already in the antecedents, otherwise leaves that subgoal open 2) It does not characterize local progress for domain constraint Q 3) For polynomials p>=0 in the normalized form that are NOT rank 1, this tactic currently requires checks the progress formula (p*>0) up to a given bound, rather than p*>=0
- bound
(default 1): the bound on higher Lie derivatives to check for strict inequality, i.e. for p>=0, this is generated p>=0 & (p=0 -> (p'>=0 & (p'=0 -> ...p'^bound > 0 ...)) (i.e. the bound-th Lie derivative is required to be strict)
- returns
closes the subgoal if P is indeed invariant, fails if P fails to normalize to f>=0 form, or if one of tactic limitations is met
- See also
Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
timeBound: DependentPositionTactic
Given a top-level succedent of the form [{t'=c,x'=f(x)& Q & t=d}]P proves P invariant because the domain constraint prevents progress This tactic is relatively flexible: t'=c can be any time-like ODE (except c cannot be 0) t=d requires d to be a constant number, which forces the whole ODE to be frozen (of course, P should be true initially)
-
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