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:

  • edu.cmu.cs.ls.keymaerax.core - KeYmaera X kernel, proof certificates, main data structures
    • Expression - Differential dynamic logic expressions: Term, Formula, Program
    • Sequent - Sequents of formulas
    • Provable - Proof certificates transformed by rules/axioms
    • Rule - Proof rules as well as USubstOne for (one-pass) uniform substitutions and renaming.
    • StaticSemantics - Static semantics with free and bound variable analysis
    • Instead of constructing dL expressions from constructors, it is easier to use the KeYmaeraXParser.
  • edu.cmu.cs.ls.keymaerax.parser - Parser and pretty printer with concrete syntax and notation for differential dynamic logic.
    • Concrete syntax for input language Differential Dynamic Logic
    • KeYmaeraXPrettyPrinter - Pretty printer producing concrete KeYmaera X syntax
    • KeYmaeraXParser - Parser reading concrete KeYmaera X syntax
    • KeYmaeraXArchiveParser - Parser reading KeYmaera X model and proof archive .kyx files
    • DLParser - Combinator parser reading concrete KeYmaera X syntax
    • DLArchiveParser - Combinator parser reading KeYmaera X model and proof archive .kyx files
  • edu.cmu.cs.ls.keymaerax.infrastruct - Prover infrastructure outside the kernel
    • UnificationMatch - Unification algorithm
    • RenUSubst - Renaming Uniform Substitution quickly combining kernel's renaming and substitution.
    • Context - Representation for contexts of formulas in which they occur.
    • Augmentors - Augmenting formula and expression data structures with additional functionality
    • ExpressionTraversal - Generic traversal functionality for expressions
  • edu.cmu.cs.ls.keymaerax.bellerophon - Bellerophon tactic language and tactic interpreter
    • BelleExpr - Tactic language expressions
    • SequentialInterpreter - Sequential tactic interpreter for Bellerophon tactics
  • edu.cmu.cs.ls.keymaerax.btactics - Bellerophon tactic library for conducting proofs.
    • TactixLibrary - Main KeYmaera X tactic library including many proof tactics.
    • HilbertCalculus - Hilbert Calculus for differential dynamic logic
    • SequentCalculus - Sequent Calculus for propositional and first-order logic
    • HybridProgramCalculus - Hybrid Program Calculus for differential dynamic logic
    • DifferentialEquationCalculus - Differential Equation Calculus for differential dynamic logic
    • UnifyUSCalculus - Unification-based uniform substitution calculus underlying the other calculi
    • [edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic] - Forward tactic framework for conducting proofs from premises to conclusions
  • edu.cmu.cs.ls.keymaerax.lemma - Lemma mechanism
    • Lemma - Lemmas are Provables stored under a name, e.g., in files.
    • LemmaDB - Lemma database stored in files or database etc.
  • edu.cmu.cs.ls.keymaerax.tools.qe - Real arithmetic back-end solvers
    • MathematicaQETool - Mathematica interface for real arithmetic.
    • Z3QETool - Z3 interface for real arithmetic.
  • edu.cmu.cs.ls.keymaerax.tools.ext - Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.
    • Mathematica - Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.
    • Z3 - Z3 interface for real arithmetic including simplifiers.

  Entry Points

  Additional entry points and usage points for KeYmaera X API:

  • edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX - Command-line launcher for KeYmaera X supports command-line argument -help to obtain usage information
  • edu.cmu.cs.ls.keymaerax.btactics.AxIndex - Axiom indexing data structures with keys and recursors for canonical proof strategies.
  • edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo - Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.
  • edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex - Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.
  • edu.cmu.cs.ls.keymaerax.btactics.Ax - Registry for derived axioms and axiomatic proof rules that are proved from the core.

  References

  Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:

  1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 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 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

  • Syntax of differential dynamic logic:
    • Syntax of dL Expressions
    • Static Semantics
  • Proof Construction of proof certificates from
    • axioms
    • Uniform substitutions
    • Uniform renamings
    • Proof rules
  • Provides basic Stored Provables as Strings, real arithmetic interfaces, error reporting, and set lattice management for sets of symbols.

  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

• And
• AndLeft
• AndRight
• AntePos
• AnyArg
• ApplicationOf
• Assertion
• Assign
• AssignAny
• Atomic
• AtomicDifferentialProgram
• AtomicFormula
• AtomicODE
• AtomicProgram
• AtomicTerm
• BaseVariable
• BinaryComposite
• BinaryCompositeFormula
• BinaryCompositeProgram
• BinaryCompositeTerm
• Bool
• BoundRenaming
• Box
• Choice
• Close
• CloseFalse
• CloseTrue
• CoHide2
• CoHideLeft
• CoHideRight
• CommuteEquivLeft
• CommuteEquivRight
• ComparisonFormula
• Compose
• Composite
• CompositeFormula
• CompositeProgram
• CompositeTerm
• CoreException
• CriticalCoreException
• Cut
• CutLeft
• CutRight
• Diamond
• Differential
• DifferentialFormula
• DifferentialProduct
• DifferentialProgram
• DifferentialProgramConst
• DifferentialProgramKind
• DifferentialSymbol
• Divide
• DotFormula
• DotTerm
• Dual
• Ensures
• Equal
• Equiv
• EquivLeft
• EquivRight
• EquivifyRight
• Except
• ExchangeLeftRule
• ExchangeRightRule
• Exists
• Expression
• ExpressionKind
• False
• Forall
• Formula
• FormulaKind
• FuncOf
• Function
• FunctionKind
• Greater
• GreaterEqual
• HideLeft
• HideRight
• Imply
• ImplyLeft
• ImplyRight
• InapplicableRuleException
• Kind
• LeftRule
• Less
• LessEqual
• Loop
• Minus
• Modal
• NamedSymbol
• Neg
• NoProverException
• NoncriticalCoreException
• Not
• NotEqual
• NotLeft
• NotRight
• Nothing
• Number
• ODESystem
• ObjectSort
• Or
• OrLeft
• OrRight
• Pair
• Plus
• PositionRule
• Power
• PredOf
• PredicationalOf
• PrettyPrinter
• Program
• ProgramConst
• ProgramKind
• Provable
• ProvableStorageException
• ProverAssertionError
• ProverException
• QETool
• Quantified
• Real
• RenamingClashException
• RightRule
• Rule
• SeqPos
• Sequent
• SetLattice
• SkolemClashException
• Skolemize
• Sort
• Space
• SpaceDependent
• StateDependent
• StaticSemantics
• SubderivationSubstitutionException
• SubstitutionAdmissibility
• SubstitutionClashException
• SubstitutionPair
• SuccPos
• SystemConst
• Term
• TermKind
• Test
• Times
• Trafo
• True
• Tuple
• URename
• USubstChurch
• USubstOne
• UnaryComposite
• UnaryCompositeFormula
• UnaryCompositeProgram
• UnaryCompositeTerm
• UniformRenaming
• Unit
• UnitFunctional
• UnitPredicational
• UnknownOperatorException
• UnprovedException
• Variable
• Version

edu.cmu.cs.ls.keymaerax.core

DifferentialProduct 

Companion class DifferentialProduct