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

  • case class TwoThreeTreePolynomialRing(variableOrdering: Ordering[Term], monomialOrdering: Ordering[IndexedSeq[(Term, Int)]]) extends PolynomialRing with Product with Serializable

    A polynomial is represented as a set of monomials stored in a 2-3 Tree, the ordering is lexicographic A monomial is represented as a coefficient and a power-product.

    A polynomial is represented as a set of monomials stored in a 2-3 Tree, the ordering is lexicographic A monomial is represented as a coefficient and a power-product. A coefficient is represented as a pair of BigDecimals for num/denom. A power product is represented densely as a list of exponents

    All data-structures maintain a proof of input term = representation of data structure as Term

    Representations of data structures (recursively applied on rhs):

    • 3-Node (l, v1, m, v2, r) is "l + v1 + m + v2 + r"
    • 2-Node (l, v, r) is "l + v + r"
    • monomial (c, pp) is "c * pp"
    • coefficient (num, denom) is "num / denom"
    • power product [e1, ..., en] is "x1e1 * ... * xn en", where instead of "x0", we write "1" in order to avoid trouble with 00, i.e., nonzero-assumptions on x or the like

    All operations on the representations update the proofs accordingly.

    Definition Classes
    btactics
  • Branch2
  • Branch3
  • Coefficient
  • Empty
  • Growth
  • Monomial
  • Polynomial
  • PowerProduct
  • SparsePowerProduct
  • Sprout
  • Stay
  • TreePolynomial
  • UnknownPolynomialImplementationException

case class Coefficient(num: BigDecimal, denom: BigDecimal, prvO: Option[ProvableSig] = None) extends Product with Serializable

prv: lhs = rhs lhs: input term (arbitrary, trace of construction) rhs: Divide(Number(num), Number(denom))

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Coefficient
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Coefficient(num: BigDecimal, denom: BigDecimal, prvO: Option[ProvableSig] = None)

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def *(that: Coefficient): Coefficient
  4. def +(that: Coefficient): Coefficient
  5. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  6. def approx(prec: Int): (ProvableSig, Coefficient, Coefficient)
  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def bigDecimalOption: Option[ProvableSig]
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  10. lazy val defaultPrv: ProvableSig
  11. val denom: BigDecimal
  12. val denomN: Number
  13. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. val eq: Equal
  15. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  16. def forgetPrv: Coefficient
  17. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  18. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  19. val lhs: Term
  20. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  21. def normalized: (ProvableSig, Term)

    normalized to a nicer output form, i.e., simplify rhs with 0 / d = 0 n / d = bd

  22. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  23. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  24. val num: BigDecimal
  25. val numN: Number
  26. val prv: ProvableSig
  27. val prvO: Option[ProvableSig]
  28. val rhs: Divide
  29. def rhsString: String
  30. def split(newNum: BigDecimal, newdenom: BigDecimal): (ProvableSig, Coefficient, Coefficient)
  31. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  32. def unary_-: Coefficient
  33. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  34. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  35. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from AnyRef

Inherited from Any

Ungrouped