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 bellerophon
    Definition Classes
    keymaerax
  • 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 cdgl
    Definition Classes
    keymaerax
  • package cli
    Definition Classes
    keymaerax
  • package codegen

    Code-generation tools to generate C-Code etc.

    Code-generation tools to generate C-Code etc. from expressions.

    Definition Classes
    keymaerax
    To do

    Stub. Describe for real.

  • package core

    KeYmaera X Kernel is the soundness-critical core of the Axiomatic Tactical Theorem Prover KeYmaera X.

    KeYmaera X Kernel is the soundness-critical core of the Axiomatic Tactical Theorem Prover KeYmaera X.

    KeYmaera X Kernel

    The KeYmaera X Kernel implements Differential Dynamic Logic and defines

    Usage Overview

    The KeYmaera X Kernel package provides the soundness-critical core of KeYmaera X. It provides ways of constructing proofs that, by construction, can only be constructed using the proof rules that the KeYmaera X Kernel provides. The proof tactics that KeYmaera X provides give you a more powerful and flexible and easier way of constructing and searching for proofs, but they internally reduce to what is shown here.

    Constructing Proofs

    The proof certificates of KeYmaera X are of type edu.cmu.cs.ls.keymaerax.core.Provable. edu.cmu.cs.ls.keymaerax.core.Provable.startProof(goal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable* begins a new proof of a edu.cmu.cs.ls.keymaerax.core.Sequent containing the conjectured differential dynamic logic formula. A proof rule of type edu.cmu.cs.ls.keymaerax.core.Rule can be applied to any subgoal of a edu.cmu.cs.ls.keymaerax.core.Provable by edu.cmu.cs.ls.keymaerax.core.Provable.apply(rule:edu\.cmu\.cs\.ls\.keymaerax\.core\.Rule,subgoal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable\.Subgoal):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable* to advance the proof until that Provable has been proved since edu.cmu.cs.ls.keymaerax.core.Provable.isProved is true. Subgoals are identified by integers.

    import scala.collection.immutable._
val verum = new Sequent(IndexedSeq(), IndexedSeq(True))
// conjecture
val provable = Provable.startProof(verum)
// construct a proof
val proof = provable(CloseTrue(SuccPos(0)), 0)
// check if proof successful, i.e. no remaining subgoals
if (proof.isProved) println("Successfully proved " + proof.proved)

    Of course, edu.cmu.cs.ls.keymaerax.btactics make it much easier to describe proof search procedures compared to the above explicit proof construction. The tactics internally construct proofs this way, but add additional flexibility and provide convenient ways of expressing proof search strategies in a tactic language.

    Combining Proofs

    Multiple Provable objects for subderivations obtained from different sources can also be merged into a single Provable object by substitution with edu.cmu.cs.ls.keymaerax.core.Provable.apply(edu.cmu.cs.ls.keymaerax.core.Provable,Int). The above example can be continued to merge proofs as follows:

    // ... continued from above
val more = new Sequent(IndexedSeq(),
    IndexedSeq(Imply(Greater(Variable("x"), Number(5)), True)))
// another conjecture
val moreProvable = Provable.startProof(more)
// construct another (partial) proof
val moreProof = moreProvable(ImplyRight(SuccPos(0)), 0)(HideLeft(AntePos(0)), 0)
// merge proofs by gluing their Provables together (substitution)
val mergedProof = moreProof(proof, 0)
// check if proof successful, i.e. no remaining subgoals
if (mergedProof.isProved) println("Successfully proved " + mergedProof.proved)

    More styles for proof construction are shown in Provable's.

    Differential Dynamic Logic

    The language of differential dynamic logic is described in KeYmaera X by its syntax and static semantics.

    Syntax

    The immutable algebraic data structures for the expressions of differential dynamic logic are of type edu.cmu.cs.ls.keymaerax.core.Expression. Expressions are categorized according to their kind by the syntactic categories of the grammar of differential dynamic logic:

    1. terms are of type edu.cmu.cs.ls.keymaerax.core.Term of kind edu.cmu.cs.ls.keymaerax.core.TermKind

    2. formulas are of type edu.cmu.cs.ls.keymaerax.core.Formula of kind edu.cmu.cs.ls.keymaerax.core.FormulaKind

    3. hybrid programs are of type edu.cmu.cs.ls.keymaerax.core.Program of kind edu.cmu.cs.ls.keymaerax.core.ProgramKind

    4. differential programs are of type edu.cmu.cs.ls.keymaerax.core.DifferentialProgram of kind edu.cmu.cs.ls.keymaerax.core.DifferentialProgramKind

    See Section 2.1

    Static Semantics

    The static semantics of differential dynamic logic is captured in edu.cmu.cs.ls.keymaerax.core.StaticSemantics in terms of the free variables and bound variables that expressions have as well as their signatures (set of occurring symbols). See Section 2.4

    Theorem Prover

    The KeYmaera X Prover Kernel provides uniform substitutions, uniform and bound variable renaming, and axioms of differential dynamic logic. For efficiency, it also directly provides propositional sequent proof rules and Skolemization.

    Axioms

    The axioms and axiomatic rules of differential dynamic logic can be looked up with edu.cmu.cs.ls.keymaerax.core.Provable.axioms and edu.cmu.cs.ls.keymaerax.core.Provable.rules respectively. All available axioms are listed in edu.cmu.cs.ls.keymaerax.core.Provable.axioms, all available axiomatic rules are listed in edu.cmu.cs.ls.keymaerax.core.Provable.rules which both ultimately come from the file edu.cmu.cs.ls.keymaerax.core.AxiomBase. See Sections 4 and 5.0 Additional axioms are available as derived axioms and lemmas in edu.cmu.cs.ls.keymaerax.btactics.Ax.

    Uniform Substitutions

    Uniform substitutions uniformly replace all occurrences of a given predicate p(.) by a formula in (.) and likewise for function symbols f(.) and program constants. Uniform substitutions and their application mechanism for differential dynamic logic are implemented in edu.cmu.cs.ls.keymaerax.core.USubst. See Section 3 and one-pass Section 3

    Uniform substitutions can be used on proof certificates with the edu.cmu.cs.ls.keymaerax.core.Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubst):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*, including uniform substitution instances of axioms or axiomatic rules. See Section 3

    Sequent Proof Rules

    All proof rules for differential dynamic logic, including the uniform substitution and bound variable renaming rules as well as efficient propositional sequent proof rules and Skolemization edu.cmu.cs.ls.keymaerax.core.Skolemize are all of type edu.cmu.cs.ls.keymaerax.core.Rule, which are the only proof rules that can ever be applied to a proof. See sequent calculus

    Additional Capabilities

    Stored Provable Mechanism

    A Stored Provable represents a Provable as a String that can be reloaded later as well as an interface to real arithmetic decision procedures are defined in edu.cmu.cs.ls.keymaerax.core.Provable.fromStorageString() and edu.cmu.cs.ls.keymaerax.core.QETool.

    Error Reporting

    Errors from the prover core are reported as exceptions of type edu.cmu.cs.ls.keymaerax.core.ProverException whose main responsibility is to propagate problems in traceable ways to the user by augmenting them with contextual information. The prover core throws exceptions of type edu.cmu.cs.ls.keymaerax.core.CoreException.

    Set Lattice

    A data structure for sets (or rather lattice completions of sets) is provided in edu.cmu.cs.ls.keymaerax.core.SetLattice based on Scala's immutable sets.

    Overall Code Complexity

    Overall, the majority of the KeYmaera X Prover Microkernel implementation consists of data structure declarations or similar mostly self-evident code. This includes straightforward variable categorization in StaticSemantics. The highest complexity is for the uniform substitution application mechanism. The highest information density is in the axiom list.

    Definition Classes
    keymaerax
    Note

    Code Review 2020-02-17

    See also

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

    Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425-441. Springer, 2019.

    Andre Platzer and Yong Kiam Tan. Differential equation invariance axiomatization. J. ACM. 67(1), 6:1-6:66, 2020.

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. arXiv 1503.01981

    Andre Platzer. Uniform substitution for differential game logic. In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Automated Reasoning, 9th International Joint Conference, IJCAR 2018, volume 10900 of LNCS, pp. 211-227. Springer 2018.

    Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp and Andre 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, LNCS. Springer, 2015.

    Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

    Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012

    Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541-550. IEEE 2012

    Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008.

    edu.cmu.cs.ls.keymaerax.core.Provable

    edu.cmu.cs.ls.keymaerax.core.Expression

    edu.cmu.cs.ls.keymaerax.core.StaticSemantics

    edu.cmu.cs.ls.keymaerax.core.USubstOne

  • package fcpsutils

    (Course infrastructure helpers).

    (Course infrastructure helpers).

    Definition Classes
    keymaerax
  • package hydra

    HyDRA Hybrid Distributed Reasoning Architecture server with a REST-API and database.

    HyDRA Hybrid Distributed Reasoning Architecture server with a REST-API and database. HyDRA provides a simplified high-level programming interface to the KeYmaeara X prover. It provides components for proof tree simplification, tactic search, and custom tactic scheduling policies, as well as for storing and accessing proofs in files or databases. These components can be accessed remotely through a REST-API.

    Definition Classes
    keymaerax
    To do

    Stub. Describe for real.

  • package infrastruct

    The infrastruct package provides central prover infrastructure such as unification and augmented formula analysis.

    The infrastruct package provides central prover infrastructure such as unification and augmented formula analysis. This infrastructure is of basic interest and useful independently of any particular tactic language etc.

    Main functionality:

    • Position with PosInExpr positioning within subformulas.
    • Context Convenience representation of formulas used as contexts that provide ways of substituting expressions in by conceptually splitting and managing the context around a position in a formula.
    • RenUSubst Renaming Uniform Substitutions that quickly combine and ultimately reduce to uniform renaming and uniform substitution of the kernel.
    • UnificationMatch single-sided matching unification algorithms.
    • Augmentors: Implicit convenience additions of helper functions to formulas, terms, programs, sequents that are useful for analysis and transformation.
    • ExpressionTraversal generic functionality for traversing expressions for analysis or transformation.
    Definition Classes
    keymaerax
    See also

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

  • package launcher

    KeYmaera X command line launcher for starting its main program with the web UI.

    KeYmaera X command line launcher for starting its main program with the web UI.

    Definition Classes
    keymaerax
    To do

    Stub. Describe for real.

  • package lemma

    Non-soundness-critical implementation of the lemma mechanism.

    Non-soundness-critical implementation of the lemma mechanism.

    Lemma Mechanism

    An implementation of a lemma data base using files edu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB. A factory edu.cmu.cs.ls.keymaerax.lemma.LemmaDBFactory provides instances of lemma databases.

    Definition Classes
    keymaerax
    Examples: 

    1. // prove a lemma
val proved = TactixLibrary.proveBy(
   Sequent(IndexedSeq(), IndexedSeq("true | x>5".asFormula)),
   orR(1) & close
 )
// store a lemma
val lemmaDB = LemmaDBFactory.lemmaDB
val evidence = ToolEvidence(immutable.Map("input" -> proved.toString, "output" -> "true")) :: Nil))
val lemmaID = lemmaDB.add(
  Lemma(proved, evidence, Some("Lemma  test"))
)
// use a lemma
LookupLemma(lemmaDB, lemmaID)

      The lemma database returned by the factory can be configured.

      2. , 

    2. LemmaDBFactory.setLemmaDB(new FileLemmaDB)
val lemmaDB = LemmaDBFactory.lemmaDB
  • CachedLemmaDB
  • Evidence
  • FileLemmaDB
  • Lemma
  • LemmaDB
  • LemmaDBBase
  • LemmaDBFactory
  • package parser

    Parser & Pretty-Printer for Differential Dynamic Logic

    Parser & Pretty-Printer for Differential Dynamic Logic

    Defines the concrete syntax of differential dynamic logic as used in KeYmaera X. Provides a parser to read string and file inputs with differential dynamic logic. Conversely provides a pretty-printer to format differential dynamic logic expression data structure as human readable concrete syntax.

    PrettyPrinter: Expression => String
Parser: String => Expression

    Usage Overview

    The default pretty-printer for the concrete syntax in KeYmaera X is in edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter. The corresponding parser for the concrete syntax in edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser. Also see Grammar of KeYmaera X Syntax

    val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
println("Printed:  " + print)
    Printing Differential Dynamic Logic

    edu.cmu.cs.ls.keymaerax.parser.PrettyPrinter defines the interface for all differential dynamic logic pretty printers in KeYmaera X.

    PrettyPrinter: Expression => String

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter implements the pretty-printer for the concrete syntax of differential dynamic logic used in KeYmaera X. A pretty-printer is an injective function from differential dynamic logic expressions to strings.

    Printing formulas to strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter.apply:

    val pp = KeYmaeraXPrettyPrinter
// "x < -y"
val fml0 = Less(Variable("x"),Neg(Variable("y")))
val fml0str = pp(fml0)
// "true -> [x:=1;]x>=0"
val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
val fml1str = pp(fml1)
    Printing Fully Parenthesized Forms

    Fully parenthesized strings are obtained using the edu.cmu.cs.ls.keymaerax.parser.FullPrettyPrinter printer:

    val pp = FullPrettyPrinter
// "x < -(y)"
val fml0 = Less(Variable("x"),Neg(Variable("y")))
val fml0str = pp(fml0)
// "true -> ([x:=1;](x>=0))"
val fml1 = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
val fml1str = pp(fml1)

    The fully-parenthesized pretty printer corresponding to a pretty printer can also be obtained using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrinter.fullPrinter

    Parsing Differential Dynamic Logic

    edu.cmu.cs.ls.keymaerax.parser.Parser defines the interface for all differential dynamic logic parsers in KeYmaera X.

    Parser: String => Expression

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser implements the parser for the concrete syntax of differential dynamic logic used in KeYmaera X. A parser is a function from input strings to differential dynamic logic expressions.

    Parsing formulas from strings is straightforward using edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.apply:

    val parser = KeYmaeraXParser
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")

    The parser parses any dL expression, so will also accept terms or programs from strings, which will lead to appropriate types:

    val parser = KeYmaeraXParser
// formulas
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")
// terms
val term0 = parser("x+5")
val term1 = parser("x^2-2*x+7")
val term2 = parser("x*y/3+(x-1)^2+5*z")
// programs
val prog0 = parser("x:=1;")
val prog1 = parser("x:=1;x:=5;x:=-1;")
val prog2 = parser("x:=1;{{x'=5}++x:=0;}")
    Parsing Only Formulas of Differential Dynamic Logic

    The parser that only parses formulas is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.formulaParser

    // the formula parser only accepts formulas
val parser = KeYmaeraXParser.formulaParser
// formulas
val fml0 = parser("x!=5")
val fml1 = parser("x>0 -> [x:=x+1;]x>1")
val fml2 = parser("x>=0 -> [{x'=2}]x>=0")
// terms will cause exceptions
try { parser("x+5") } catch {case e: ParseException => println("Rejected")}
// programs will cause exceptions
try { parser("x:=1;") } catch {case e: ParseException => println("Rejected")}

    Similarly, a parser that only parses terms is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.termParser and a parser that only parses programs is obtained via edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.programParser

    Parsing Pretty-Printed Strings

    Corresponding parsers and pretty-printers match with one another. Parsing a pretty-printed expression results in the original expression again:

    parse(print(e)) == e

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser and are inverses in this sense. The converse print(parse(s)) == s is not quite the case, because there can be minor spacing and superfluous parentheses differences. The following slightly weaker form still holds:

    parse(print(parse(s))) == parse(s)

    Parsing the pretty-print of an expression with compatible printers and parsers always gives the original expression back:

    val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val fml = Imply(True, Box(Assign(Variable("x"), Number(1)), GreaterEqual(Variable("x"), Number(0))))
// something like "true -> [x:=1;]x>=0" modulo spacing
val print = pp(fml)
val reparse = parser(print)
if (fml == reparse) println("Print and reparse successful") else println("Discrepancy")
    Pretty-Printing Parsed Strings

    It can be quite helpful to print an expression that has been parsed to check how it got parsed:

    val parser = KeYmaeraXParser
val pp = KeYmaeraXPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
println("Printed:  " + print)
println("Original: " + input)
println("Can differ slightly by spacing and parentheses")

    Recall that the default pretty printer uses compact parentheses and braces. That is, it only prints them when necessary to disambiguate. For storage purposes and disambiguation it can be better to use fully parenthesized printouts, which is what edu.cmu.cs.ls.keymaerax.parser.FullPrettyPrinter achieves:

    val parser = KeYmaeraXParser
val pp = FullPrettyPrinter
val input = "x^2>=0 & x<44 -> [x:=2;{x'=1&x<=10}]x>=1"
val parse = parser(input)
println("Parsed:   " + parse)
val print = pp(parse)
// (((x)^(2)>=0)&(x < 44))->([{x:=2;}{{x'=1&x<=10}}](x>=1))
println("Printed:  " + print)
println("Original: " + input)
    Pretty-Printing Sequents

    Sequents can be pretty-printed using the default pretty printer via edu.cmu.cs.ls.keymaerax.core.Sequent.prettyString

    val parser = KeYmaeraXParser
val sequent = Sequent(IndexedSeq(parse("x<22"), parse("x>0")), IndexedSeq(parse("[x:=x+1;]x<23")))
println("Printed:  " + sequent.prettyString)
    Definition Classes
    keymaerax
    See also

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

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

    Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

    Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp and Andre 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, LNCS. Springer, 2015.

    Grammar of Differential Dynamic Logic

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter

  • package pt

    Proof-term checker turns proof terms to proof certificates.

    Proof-term checker turns proof terms to proof certificates. edu.cmu.cs.ls.keymaerax.pt.ProofChecker turns a proof term to the edu.cmu.cs.ls.keymaerax.core.Provable that it proves.

    ProofChecker : ProofTerm * Formula => Provable

    This package defines

    Definition Classes
    keymaerax
  • package scalatactic

    Scala API for proof and tactics management etc.

    Scala API for proof and tactics management etc.

    Definition Classes
    keymaerax
    To do

    Stub. Describe for real.

  • package tacticsinterface

    Simple interface to the tactics exposed to the web UI and REST-API.

    Simple interface to the tactics exposed to the web UI and REST-API. Tactic combinator parser. Main tactics are provided in edu.cmu.cs.ls.keymaerax.tactics.TactixLibrary

    Definition Classes
    keymaerax
    To do

    Stub. Describe for real.

    See also

    edu.cmu.cs.ls.keymaerax.tactics

  • package tools

    Arithmetic back-ends and arithmetic utilities for tactics, including an SMT interface.

    Arithmetic back-ends and arithmetic utilities for tactics, including an SMT interface.

    Definition Classes
    keymaerax
    To do

    Stub. Describe for real.

  • package utils
    Definition Classes
    keymaerax

package lemma

Non-soundness-critical implementation of the lemma mechanism.

Lemma Mechanism

An implementation of a lemma data base using files edu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB. A factory edu.cmu.cs.ls.keymaerax.lemma.LemmaDBFactory provides instances of lemma databases.

Examples: 

  1. // prove a lemma
val proved = TactixLibrary.proveBy(
   Sequent(IndexedSeq(), IndexedSeq("true | x>5".asFormula)),
   orR(1) & close
 )
// store a lemma
val lemmaDB = LemmaDBFactory.lemmaDB
val evidence = ToolEvidence(immutable.Map("input" -> proved.toString, "output" -> "true")) :: Nil))
val lemmaID = lemmaDB.add(
  Lemma(proved, evidence, Some("Lemma  test"))
)
// use a lemma
LookupLemma(lemmaDB, lemmaID)

    The lemma database returned by the factory can be configured.

    2. , 

  2. LemmaDBFactory.setLemmaDB(new FileLemmaDB)
val lemmaDB = LemmaDBFactory.lemmaDB
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. lemma
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. class CachedLemmaDB extends LemmaDB with Logging

    Extends an arbitrary LemmaDB with caching functionality to reduce the cost of repeated accesses to the same Lemma within a given KeYmaeraX session.

    Extends an arbitrary LemmaDB with caching functionality to reduce the cost of repeated accesses to the same Lemma within a given KeYmaeraX session.

    Created by bbohrer on 8/3/16.

  2. trait Evidence extends AnyRef

    "Weak" Correctness evidence for lemmas

  3. class FileLemmaDB extends LemmaDBBase with Logging

    File-based lemma DB implementation.

    File-based lemma DB implementation. Stores one lemma per file in the user's home directory under .keymaerax/cache/lemmadb/ directory. Lemma file names are created automatically and in a thread-safe manner.

    Note

    Prefer LemmaDBFactory.lemmaDB over instantiating directly to get an instance of a lemma database and ensure thread safety. Created by smitsch on 4/27/15.

  4. final case class Lemma(fact: ProvableSig, evidence: List[Evidence], name: Option[String] = None) extends Product with Serializable

    Lemmas are named Provables, supported by some evidence of how they came about.

    Lemmas are named Provables, supported by some evidence of how they came about. The soundness-critical part in a lemma is its provable fact, which can only be obtained from the prover core.

    Example: 

    1. // prove a lemma
val proved = TactixLibrary.proveBy(
   Sequent(IndexedSeq(), IndexedSeq("true | x>5".asFormula)),
   orR(1) & close
 )
// store a lemma
val lemmaDB = LemmaDBFactory.lemmaDB
val evidence = ToolEvidence(immutable.Map("input" -> proved.toString, "output" -> "true")) :: Nil))
val lemmaID = lemmaDB.add(
  Lemma(proved, evidence, Some("Lemma  test"))
)

// retrieve a lemma
val lemmaFact = lemmaDB.get(lemmaID).get.fact
// use a lemma literally
TactixLibrary.by(lemmaFact)
// use a uniform substitution instance of a lemma
TactixLibrary.byUS(lemmaFact)
    Note

    Construction is not soundness-critical so constructor is not private, because Provables can only be constructed by prover core.

    See also

    ProvableSig.proveArithmeticLemma

    edu.cmu.cs.ls.keymaerax.lemma.LemmaDB

    lemma.Lemma.fromString

  5. trait LemmaDB extends AnyRef

    Store and retrieve lemmas from a lemma database.

    Store and retrieve lemmas from a lemma database. Use edu.cmu.cs.ls.keymaerax.lemma.LemmaDBFactory.lemmaDB to get an instance of a lemma database.

    Example:

    1. Storing and using a lemma

      import edu.cmu.cs.ls.keymaerax.lemma.LemmaDBFactory
val lemmaDB = LemmaDBFactory.lemmaDB
// prove a lemma
val proved = TactixLibrary.proveBy(
   Sequent(IndexedSeq(), IndexedSeq("true | x>5".asFormula)),
   orR(1) & close
 )
// store a lemma
val evidence = ToolEvidence(immutable.Map("input" -> proved.toString, "output" -> "true")) :: Nil))
val lemmaID = lemmaDB.add(
  Lemma(proved, evidence, Some("Lemma  test"))
)
// use a lemma
LookupLemma(lemmaDB, lemmaID)
    See also

    Lemma

  6. abstract class LemmaDBBase extends LemmaDB

    Common Lemma Database implemented from string-based storage primitives.

    Common Lemma Database implemented from string-based storage primitives. Common logic shared by most lemma DB implementations. Most lemma DBs can (and should) be implemented by extending this class and implementing the abstract methods for basic storage operations.

Value Members

  1. object Lemma extends Serializable

    Facility for reading lemmas back in from their string representation.

  2. object LemmaDBFactory

    Returns lemma database instances.

    Returns lemma database instances. Prefer using this factory over instantiating lemma databases directly.

    Example: 

    1. val lemmaDB = LemmaDBFactory.lemmaDB

      Created by smitsch on 9/1/15.

Inherited from AnyRef

Inherited from Any

Ungrouped