Packages

  • package root

    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.

    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:

    Entry Points

    Additional entry points and usage points for KeYmaera X API:

    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

    Definition Classes
    root
  • package edu
    Definition Classes
    root
  • package cmu
    Definition Classes
    edu
  • package cs
    Definition Classes
    cmu
  • package ls
    Definition Classes
    cs
  • package keymaerax
    Definition Classes
    ls
  • package btactics

    Tactic library in the Bellerophon tactic language.

    Tactic library in the Bellerophon tactic language.

    All tactics are implemented in the Bellerophon tactic language, including its dependent tactics, which ultimately produce edu.cmu.cs.ls.keymaerax.core.Provable proof certificates by the Bellerophon interpreter. The Provables that tactics produce can be extracted, for example, with edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.proveBy().

    Proof Styles

    KeYmaera X supports many different proof styles, including flexible combinations of the following styles:

    1. Explicit proof certificates directly program the proof rules from the core.

    2. Explicit proofs use tactics to describe a proof directly mentioning all or most proof steps.

    3. Proof by search relies mainly on proof search with occasional additional guidance.

    4. Proof by pointing points out facts and where to use them.

    5. Proof by congruence is based on equivalence or equality or implicational rewriting within a context.

    6. Proof by chase is based on chasing away operators at an indicated position.

    Explicit Proof Certificates

    The most explicit types of proofs can be constructed directly using the edu.cmu.cs.ls.keymaerax.core.Provable certificates in KeYmaera X's kernel without using any tactics. Also see edu.cmu.cs.ls.keymaerax.core.

    import edu.cmu.cs.ls.keymaerax.core._
// explicit proof certificate construction of |- !!p() <-> p()
val proof = (Provable.startProof(
  "!!p() <-> p()".asFormula)
  (EquivRight(SuccPos(0)), 0)
  // right branch
    (NotRight(SuccPos(0)), 1)
    (NotLeft(AntePos(1)), 1)
    (Close(AntePos(0),SuccPos(0)), 1)
  // left branch
    (NotLeft(AntePos(0)), 0)
    (NotRight(SuccPos(1)), 0)
    (Close(AntePos(0),SuccPos(0)), 0)
)
    Explicit Proofs

    Explicit proofs construct similarly explicit proof steps, just with explicit tactics from TactixLibrary: The only actual difference is the order of the branches, which is fixed to be from left to right in tactic branching. Tactics also use more elegant signed integers to refer to antecedent positions (negative) or succedent positions (positive).

    import TactixLibrary._
// Explicit proof tactic for |- !!p() <-> p()
val proof = TactixLibrary.proveBy("!!p() <-> p()".asFormula,
   equivR(1) & <(
     (notL(-1) &
       notR(2) &
       closeId)
     ,
     (notR(1) &
       notL(-2) &
       closeId)
     )
 )
    Proof by Search

    Proof by search primarily relies on proof search procedures to conduct a proof. That gives very short proofs but, of course, they are not always entirely informative about how the proof worked. It is easiest to see in simple situations where propositional logic proof search will find a proof but works well in more general situations, too.

    import TactixLibrary._
// Proof by search of |- (p() & q()) & r() <-> p() & (q() & r())
val proof = TactixLibrary.proveBy("(p() & q()) & r() <-> p() & (q() & r())".asFormula,
   prop
)

    Common tactics for proof by search include edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.prop(), edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.auto() and the like.

    Proof by Pointing

    Proof by pointing emphasizes the facts to use and is implicit about the details on how to use them exactly. Proof by pointing works by pointing to a position in the sequent and using a given fact at that position. For example, for proving

    ⟨v:=2*v+1;⟩v!=0 <-> 2*v+1!=0

    it is enough to point to the highlighted position using the Ax.diamond axiom fact ![a;]!p(||) <-> ⟨a;⟩p(||) at the highlighted position to reduce the proof to a proof of

    ![v:=2*v+1;]!(v!=0) <-> 2*v+1!=0

    which is, in turn, easy to prove by pointing to the highlighted position using the Ax.assignbAxiom axiom [x:=t();]p(x) <-> p(t()) at the highlighted position to reduce the proof to

    !!(2*v+1!=0) <-> 2*v+1!=0

    Finally, using double negation !!p() <-> p() at the highlighted position yields the following

    2*v+1!=0 <-> 2*v+1!=0

    which easily proves by reflexivity p() <-> p().

    Proof by pointing matches the highlighted position against the highlighted position in the fact and does what it takes to use that knowledge. There are multiple variations of proof by pointing in edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.useAt and edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.byUS, which are also imported into edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary. The above proof by pointing implements directly in KeYmaera X:

    import TactixLibrary._
// Proof by pointing of  |- <v:=2*v+1;>v!=0 <-> 2*v+1!=0
val proof = TactixLibrary.proveBy("<v:=2*v+1;>q(v) <-> q(2*v+1)".asFormula,
  // use Ax.diamond axiom backwards at the indicated position on
  // |- __<v:=2*v+1;>q(v)__ <-> q(2*v+1)
  useExpansionAt(Ax.diamond)(1, 0::Nil) &
  // use Ax.assignbAxiom axiom forward at the indicated position on
  // |- !__[v:=2*v+1;]!q(v)__ <-> q(2*v+1)
  useAt(Ax.assignbAxiom(1, 0::0::Nil) &
  // use double negation at the indicated position on
  // |- __!!q(2*v+1)__ <-> q(2*v+1)
  useAt(Ax.doubleNegation)(1, 0::Nil) &
  // close by (an instance of) reflexivity |- p() <-> p()
  // |- q(2*v+1) <-> q(2*v+1)
  byUS(Ax.equivReflexive)
)

    Another example is:

    import TactixLibrary._
// Proof by pointing of  |- <a;++b;>p(x) <-> (<a;>p(x) | <b;>p(x))
val proof = TactixLibrary.proveBy("<a;++b;>p(x) <-> (<a;>p(x) | <b;>p(x))".asFormula,
  // use Ax.diamond axiom backwards at the indicated position on
  // |- __<a;++b;>p(x)__  <->  <a;>p(x) | <b;>p(x)
  useExpansionAt(Ax.diamond)(1, 0::Nil) &
  // use Ax.choiceb axiom forward at the indicated position on
  // |- !__[a;++b;]!p(x)__  <->  <a;>p(x) | <b;>p(x)
  useAt(Ax.choiceb)(1, 0::0::Nil) &
  // use Ax.diamond axiom forward at the indicated position on
  // |- !([a;]!p(x) & [b;]!p(x))  <->  __<a;>p(x)__ | <b;>p(x)
  useExpansionAt(Ax.diamond)(1, 1::0::Nil) &
  // use Ax.diamond axiom forward at the indicated position on
  // |- !([a;]!p(x) & [b;]!p(x))  <->  ![a;]!p(x) | __<b;>p(x)__
  useExpansionAt(Ax.diamond)(1, 1::1::Nil) &
  // use propositional logic to show
  // |- !([a;]!p(x) & [b;]!p(x))  <->  ![a;]!p(x) | ![b;]!p(x)
  prop
)

    edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.stepAt also uses proof by pointing but figures out the appropriate fact to use on its own. Here's a similar proof:

    import TactixLibrary._
// Proof by pointing with steps of  |- ⟨a++b⟩p(x) <-> (⟨a⟩p(x) | ⟨b⟩p(x))
val proof = TactixLibrary.proveBy("p(x) <-> (p(x) | p(x))".asFormula,
  // use Ax.diamond axiom backwards at the indicated position on
  // |- __⟨a++b⟩p(x)__  <->  ⟨a⟩p(x) | ⟨b⟩p(x)
  useExpansionAt(Ax.diamond)(1, 0::Nil) &
  // |- !__[a;++b;]!p(x)__  <->  ⟨a⟩p(x) | ⟨b⟩p(x)
  // step Ax.choiceb axiom forward at the indicated position
  stepAt(1, 0::0::Nil) &
  // |- __!([a;]!p(x) & [b;]!p(x))__  <-> ⟨a⟩p(x) | ⟨b⟩p(x)
  // step deMorgan forward at the indicated position
  stepAt(1, 0::Nil) &
  // |- __![a;]!p(x)__ | ![b;]!p(x)  <-> ⟨a⟩p(x) | ⟨b⟩p(x)
  // step Ax.diamond forward at the indicated position
  stepAt(1, 0::0::Nil) &
  // |- ⟨a⟩p(x) | __![b;]!p(x)__  <-> ⟨a⟩p(x) | ⟨b⟩p(x)
  // step Ax.diamond forward at the indicated position
  stepAt(1, 0::1::Nil) &
  // |- ⟨a⟩p(x) | ⟨b⟩p(x)  <-> ⟨a⟩p(x) | ⟨b⟩p(x)
  byUS(Ax.equivReflexive)
)

    Likewise, for proving

    x>5 |- !([x:=x+1; ++ x:=0;]x>=6) | x<2

    it is enough to point to the highlighted position

    x>5 |- !([x:=x+1; ++ x:=0;]x>=6) | x<2

    and using the Ax.choiceb axiom fact [a;++b;]p(||) <-> [a;]p(||) & [b;]p(||) to reduce the proof to a proof of

    x>5 |- !([x:=x+1;]x>6 & [x:=0;]x>=6) | x<2

    which is, in turn, easy to prove by pointing to the assignments using Ax.assignbAxiom axioms and ultimately asking propositional logic.

    More proofs by pointing are shown in edu.cmu.cs.ls.keymaerax.btactics.Ax source code.

    Proof by Congruence

    Proof by congruence is based on equivalence or equality or implicational rewriting within a context. This proof style can make quite quick inferences leading to significant progress using the CE, CQ, CT congruence proof rules or combinations thereof.

    import TactixLibrary._
// |- x*(x+1)>=0 -> [y:=0;x:=__x^2+x__;]x>=y
val proof = TactixLibrary.proveBy("x*(x+1)>=0 -> [y:=0;x:=x^2+x;]x>=y".asFormula,
  CEat(proveBy("x*(x+1)=x^2+x".asFormula, QE)) (1, 1::0::1::1::Nil) &
  // |- x*(x+1)>=0 -> [y:=0;x:=__x*(x+1)__;]x>=y by CE/CQ using x*(x+1)=x^2+x at the indicated position
  // step uses top-level operator [;]
  stepAt(1, 1::Nil) &
  // |- x*(x+1)>=0 -> [y:=0;][x:=x*(x+1);]x>=y
  // step uses top-level operator [:=]
  stepAt(1, 1::Nil) &
  // |- x*(x+1)>=0 -> [x:=x*(x+1);]x>=0
  // step uses top-level [:=]
  stepAt(1, 1::Nil) &
  // |- x*(x+1)>=0 -> x*(x+1)>=0
  prop
)

    Proof by congruence can also make use of a fact in multiple places at once by defining an appropriate context C:

    import TactixLibrary._
val C = Context("x<5 & ⎵ -> [{x' = 5*x & ⎵}](⎵ & x>=1)".asFormula)
// |- x<5 & __x^2<4__ -> [{x' = 5*x & __x^2<4__}](__x^2<4__ & x>=1)
val proof = TactixLibrary.proveBy("x<5 & x^2<4 -> [{x' = 5*x & x^2<4}](x^2<4 & x>=1)".asFormula,
  CEat(proveBy("-2x^2<4".asFormula, QE), C) (1))
)
// |- x<5 & (__-2 [{x' = 5*x & __-2=1) by CE
println(proof.subgoals)
    Proof by Chase

    Proof by chase chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices. The canonical examples use edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase() to chase away differential forms:

    import TactixLibrary._
val proof = TactixLibrary.proveBy("[{x'=22}](2*x+x*y>=5)'".asFormula,
 // chase the differential prime away in the postcondition
 chase(1, 1 :: Nil)
 // |- [{x'=22}]2*x'+(x'*y+x*y')>=0
)
// Remaining subgoals: |- [{x'=22}]2*x'+(x'*y+x*y')>=0
println(proof.subgoals)
    import TactixLibrary._
val proof = TactixLibrary.proveBy("[{x'=22}](2*x+x*y>=5)' <-> [{x'=22}]2*x'+(x'*y+x*y')>=0".asFormula,
  // chase the differential prime away in the left postcondition
  chase(1, 0:: 1 :: Nil) &
  // |- [{x'=22}]2*x'+(x'*y+x*y')>=0 <-> [{x'=22}]2*x'+(x'*y+x*y')>=0
  byUS(Ax.equivReflexive)
)

    Yet edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase() is also useful to chase away other operators, say, modalities:

    import TactixLibrary._
// proof by chase of |- [?x>0;x:=x+1;x:=2*x; ++ ?x=0;x:=1;]x>=1
val proof = TactixLibrary.proveBy(
  "[?x>0;x:=x+1;x:=2*x; ++ ?x=0;x:=1;]x>=1".asFormula,
  // chase the box in the succedent away
  chase(1,Nil) &
  // |- (x>0->2*(x+1)>=1)&(x=0->1>=1)
  QE
)

    Additional Mechanisms

    Definition Classes
    keymaerax
    To do

    Expand descriptions

    See also

    Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.

    edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary

    edu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus

    edu.cmu.cs.ls.keymaerax.btactics.SequentCalculus

    edu.cmu.cs.ls.keymaerax.btactics.HybridProgramCalculus

    edu.cmu.cs.ls.keymaerax.btactics.DifferentialEquationCalculus

    edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus

  • object TaylorModelArith

    Taylor model arithmetic

    Taylor model arithmetic

    Here, a Taylor model is a data structure maintaining a proof that some term is element of the Taylor model.

    Definition Classes
    btactics
  • class TemplateLemmas extends TaylorModel

    generic lemmas for evolution of ODE ode with Taylor model approiximations of order order

    generic lemmas for evolution of ODE ode with Taylor model approiximations of order order

    Definition Classes
    TaylorModelArith
  • TimeStep

class TimeStep extends AnyRef

Infrastructure for a concrete Taylor model time step:

Input: (linearly) preconditioned Taylor model (TM_l o RM_r), initial time t0, x0.provable: context |- x = TM_l(r) (zero interval term) r0.provable: context |- r = TM_r(e) t0: context |- t = t0 (implicitly) context |- e \in [-1, 1] (suitable for IntervalArithmeticV2) // @todo: make these assumptions more explicit

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TimeStep
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new TimeStep(x0: Seq[TM], r0: Seq[TM], t0: ProvableSig, h: BigDecimal)(implicit options: TaylorModelOptions, timeStepOptions: TimeStepOptions)

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. val boxTMEnclosure1: Formula
  6. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  7. val context: IndexedSeq[Formula]
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  10. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. val initialCondition1: Formula
  14. val initialConditionFmls1: List[Formula]
  15. val initialConditionPrv: ProvableSig
  16. val initialStateEqs: Seq[ProvableSig]
  17. val instantiation: USubstOne
  18. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  19. val localTime: Term
  20. def mkTerm(coeff: (BigDecimal, BigDecimal)): Term
  21. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  22. val nonnegativeTimeStep: ProvableSig
  23. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  24. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. val numbericCondition1: Formula
  26. val numbericConditionPrv: ProvableSig
  27. val numericAssumptionPrv: ProvableSig
  28. val qeTool: BigDecimalTool
  29. val rIntervals: IndexedSeq[(Term, Term, ProvableSig)]
  30. val rightTmDomainPrv: ProvableSig
  31. val rvars: IndexedSeq[Term]
  32. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  33. val t1: Term
  34. val t1Eq: Equal
  35. val t1Prv: ProvableSig
  36. val taylorModelsFml: Formula
  37. val taylorModelsIvl: List[(Exists, Exists, ProvableSig, (Term, PolynomialArithV2.Polynomial, Term, Term, ProvableSig))]
  38. val timeEq: Equal
  39. val timeFml: Formula
  40. def timeStepLemma(P: Formula): (ProvableSig, Seq[TM], Seq[TM], (Seq[TM], Seq[TM], ProvableSig))

    Computes concrete Taylor models to perform a time step on an (unbounded time) ode evolution:

    Computes concrete Taylor models to perform a time step on an (unbounded time) ode evolution:

    returns

    (provable, TM_ivl, (TM_h, t1_eq)) where provable: ivlContext |- eqContext |- " " Γ, s ∈ [0, h], x = TM_ivl(s, r) |- P() ;; Γ, t=t0+h, x = TM_h(r) |- [{x'=ode(x)}]P -------------------------------------------------------------------------------------------------------------- Γ, t=t0, x=TM0(r) |- [{x'=ode(x)}]P TM_ivl.context = ivlContext TM_h.context = eqContext t1_eq: eqContext |- t=t0+h

  41. def timeStepLemma: ProvableSig

    * computes a concrete Taylor Model in the variables r of the right Taylor model [{x'=ode(x)&t0<=t&t<=t0+h}]x=TM(r)

  42. val timebounds: IndexedSeq[LessEqual]
  43. def toString(): String
    Definition Classes
    AnyRef → Any
  44. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  45. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  46. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped