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
Preprove the symbolic lemmas for ndimensional Cauchy Schwartz Note: this lemma proves pretty quickly e.g.
Preprove the symbolic lemmas for ndimensional 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 <= (uv)}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 Gf(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 toplevel 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)
Preprove the following doublesided bound: (G^{2+1) p}2 <= 2*((Gp).p) <= (G^{2+1) p}2
Preprove the following doublesided 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 Subformulas 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 Subformulas 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 toplevel succedent position corresponding to [x'=f(x)&Q]P with x'=f(x) a linear, nilpotent ODE
Given a toplevel 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+x^{2x}2 will be treated as nonlinear 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 ith 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 toplevel succedent position corresponding to [x'=f(x)&Q]P
Given a toplevel succedent position corresponding to [x'=f(x)&Q]P
GP 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 toplevel succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a semialgebraic invariant, i.e.
Given a toplevel 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 toplevel succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e.
Given a toplevel 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
GP 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 toplevel succedent position corresponding to [x'=f(x)&Q]P Tries to prove that P is a closed semialgebraic invariant, i.e.
Given a toplevel 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 boundth 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 toplevel 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 timelike 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 (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