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 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

• :+
• ArchiveParser
• AtomicBinaryFormat
• AtomicFormat
• AxiomFileMode
• BasePrettyPrinter
• BinaryNotation
• BinaryOpSpec
• Bottom
• DLArchiveParser
• DLAxiomParser
• DLParser
• DLParserUtils
• Declaration
• EOF
• ExpressionMode
• ExternalEvidence
• FormatProvider
• FullPrettyPrinter
• FullPrettyPrinter0
• InterpretedSymbols
• KeYmaera3PrettyPrinter
• KeYmaeraXArchiveParser
• KeYmaeraXArchiveParserBase
• KeYmaeraXArchivePrinter
• KeYmaeraXAxiomParser
• KeYmaeraXExtendedLemmaParser
• KeYmaeraXLegacyArchivePrinter
• KeYmaeraXLexer
• KeYmaeraXNoContractPrettyPrinter
• KeYmaeraXOmitInterpretationPrettyPrinter
• KeYmaeraXParser
• KeYmaeraXPrecedencePrinter
• KeYmaeraXPrettierPrinter
• KeYmaeraXPrettyPrinter
• KeYmaeraXPrinter
• KeYmaeraXSkipPrinter
• KeYmaeraXStoredProvableParser
• KeYmaeraXWeightedPrettyPrinter
• LeftAssociative
• LemmaFileMode
• LexException
• LexerMode
• Location
• MixedBinary
• Name
• NonAssociative
• NoneFormatProvider
• NullaryNotation
• ODEToInterpreted
• OpNotation
• OpSpec
• ParseException
• ParsedArchiveEntry
• Parser
• ParserHelper
• ParserInit
• PostfixFormat
• PrefixFormat
• PrettierPrintFormatProvider
• PrettyPrintFormatProvider
• PrettyPrinter
• ProblemFileMode
• ProofEvidence
• Region
• ReservedSymbols
• RightAssociative
• SequentParser
• Signature
• Stack
• StoredProvableMode
• StringConverter
• SubstitutionParser
• SuffixRegion
• TacticReservedSymbols
• Terminal
• TernaryNotation
• TernaryOpSpec
• TernaryPrefixFormat
• TokenParser
• UnaryNotation
• UnaryOpSpec
• UnificationSubstitutionParser
• UnitOpSpec
• UnknownLocation

edu.cmu.cs.ls.keymaerax.parser

Signature 