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

  • package coasterx
    Definition Classes
    btactics
  • AccelEnvelope
  • CoasterXParser
  • CoasterXProver
  • CoasterXSpec
  • CoasterXTestLib

class CoasterXProver extends AnyRef

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

Instance Constructors

  1. new CoasterXProver(spec: CoasterXSpec, env: AccelEnvelope, reuseComponents: Boolean = true, countSteps: Boolean = false, debugLevel: Int = 1, useNaive: Boolean)

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. val DEBUG_SECTION: Option[Int]
  5. val MAX_TIMEFN_DEPTH: Int
  6. def apply(fileName: String): ProvableSig
  7. def arcProofQ1: ProvableSig
  8. def arcProofQ1CCW: ProvableSig
  9. def arcProofQ2: ProvableSig
  10. def arcProofQ2CCW: ProvableSig
  11. def arcProofQ3: ProvableSig
  12. def arcProofQ3CW: ProvableSig
  13. def arcProofQ4: ProvableSig
  14. def arcProofQ4CW: ProvableSig
  15. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  16. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  17. def coHideL(is: List[Int], pr: ProvableSig): BelleExpr
  18. def coHideL(i: Int, pr: ProvableSig): BelleExpr
  19. def coHideLPr(i: Int, pr: ProvableSig): ProvableSig
  20. def componentTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, section: Section, v: Term, yInit: Term, i: Int, nSections: Int, initD: TPoint): ProvableSig
  21. var currTimefnDepth: Int
  22. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  23. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  24. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  25. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  26. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  27. def hideYs(iSection: Int, nSections: Int): (BelleExpr, Int)
  28. def hideYsAfter(iSection: Int, nSections: Int, yDefStart: Int = 2): (BelleExpr, Int)
  29. def interpret(e: BelleExpr, pr: ProvableSig): ProvableSig
  30. def invImpliesPost(pr: ProvableSig, nSections: Int): ProvableSig
  31. def invariant(align: (AFile, Formula), env: AccelEnvelope): Formula
  32. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  33. var lemmaDB: LemmaDB
  34. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  35. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  36. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  37. def preImpliesInv(pr: ProvableSig, nSections: Int): ProvableSig
  38. def proveAllComponents(global: ProvableSig, locals: List[ProvableSig], points: List[(Term, Term)], segments: List[Section], v: Term, yInit: Term, i: Int, nSections: Int, initsD: List[TPoint]): ProvableSig
  39. def proveArcArith(pr: ProvableSig, theta1: Number, deltaTheta: Number, bl: TPoint, tr: TPoint, iSection: Int, nSections: Int): ProvableSig
  40. def proveConjs(f: (Int, ProvableSig) ⇒ ProvableSig, pr: ProvableSig, conjDepth: Int, conjI: Int = 0): ProvableSig
  41. def proveLineArith(pr: ProvableSig, bl: TPoint, tr: TPoint, iSection: Int, nSections: Int): ProvableSig
  42. def proveLineArithFromDW(pr: ProvableSig, bl: TPoint, tr: TPoint, iSection: Int, nSections: Int): ProvableSig
  43. def provePosts(pr: ProvableSig, fml: Formula, p1: TPoint, p2: TPoint, section: Section, v: Number, yInit: Term, i: Int, j: Int, nSections: Int, initD: TPoint): BelleExpr
  44. def quad1CCWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  45. def quad1CWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  46. def quad2CCWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  47. def quad2CWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  48. def quad3CCWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  49. def quad3CWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  50. def quad4CCWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  51. def quad4CWTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, bl: TPoint, tr: TPoint, v0: Term, yInit: Term, theta1: Number, deltaTheta: Number, nYs: Int, iSection: Int): ProvableSig
  52. def resetLemmaDB(): Unit
  53. def rotAnte(pr: ProvableSig): ProvableSig
  54. def sectionTactic(pr: ProvableSig, p1: TPoint, p2: TPoint, v0: Term, yInit: Term, section: Section, iSection: Int, nSections: Int, initD: TPoint): ProvableSig
  55. def selectSection(iSection: Int, nSections: Int, pr: ProvableSig): ProvableSig
  56. def splitComponents(pr: ProvableSig, i: Int = 0): (ProvableSig, List[ProvableSig])
  57. def storeLemma(fact: ProvableSig, name: Option[String]): String
  58. def straightProofDown: ProvableSig
  59. def straightProofUp: ProvableSig
  60. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  61. def timeFn[T](msg: String, f: () ⇒ T): T
  62. def toString(): String
    Definition Classes
    AnyRef → Any
  63. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  64. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  65. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped