package parser
- Alphabetic
- Public
- All
Type Members
- case class BelleBinaryOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean) extends BelleOpSpec with Product with Serializable
- case class BelleBranchingOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (Seq[BelleExpr]) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
- case class BelleDefTacticOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (String, BelleExpr) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
- case class BelleLetOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (Expression, Expression, BelleExpr) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
-
sealed
trait
BelleOpSpec extends AnyRef
- Note
Needs some work because the constructors for Belle expressions are far more diverse than the constructors for KeYmaera X expressions
- case class BelleRepeatOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (BelleExpr, Int, BelleType) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
- case class BelleSaturatingOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (BelleExpr, BelleType) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
- sealed abstract class BelleTerminal extends AnyRef
- case class BelleUSubstOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (Seq[(BelleType, (RenUSubst) ⇒ BelleExpr)]) ⇒ BelleExpr) extends BelleOpSpec with Product with Serializable
- case class BelleUnaryOpSpec(terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean) extends BelleOpSpec with Product with Serializable
- case class BelleUnitOpSpec[T, S](terminal: BelleTerminal, precedence: Int, leftAssoc: Boolean, constructor: (T) ⇒ S) extends BelleOpSpec with Product with Serializable
-
class
DLBelleParser extends DLTacticParser
Bellerophon tactic parser for Differential Dynamic Logic reads input strings in the concrete syntax of Bellerophon tactics for KeYmaera X.
Bellerophon tactic parser for Differential Dynamic Logic reads input strings in the concrete syntax of Bellerophon tactics for KeYmaera X. It uses
tacticProvider
to map names and inputs to concrete tactic expressions.- See also
- class DLMockBelleParser extends DLTacticParser
-
trait
DLTacticParser extends TacticParser
DL tactic parser with fastparse-compatible entry point.
-
case class
PosInBelleExpr(idxs: Seq[Int]) extends Product with Serializable
Used to indicate the position in an expression.
Used to indicate the position in an expression. Usually for error reporing purposes.
- class PositionException extends Exception
- case class PrinterException(msg: String) extends Exception with Product with Serializable
-
trait
TacticParser extends (String) ⇒ BelleExpr
Parser interface for Bellerophon tactics of KeYmaera X.
Parser interface for Bellerophon tactics of KeYmaera X. Provides a parser to read string inputs as a Bellerophon tactic. A parser is a function from input strings to Bellerophon expressions.
Parser: String => BelleExpr
Parsers are adjoint to printers, i.e., they reparse printed expressions as the original expressions but fail to parse syntactically ill-formed strings:
parser(printer(tactic)) == tactic
- See also
Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer. Bellerophon: Tactical theorem proving for hybrid systems. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207-224. Springer, 2017.
Value Members
- object BRANCH_COMBINATOR extends BelleTerminal
-
object
BelleLexer extends (String) ⇒ List[BelleToken] with Logging
A lexer for the Bellerophon tactics language.
- object BelleOpSpec
- object BelleParseException
-
object
BelleParser extends TacticParser with Logging
The Bellerophon parser
The Bellerophon parser
- See also
-
object
BellePrettyPrinter extends (BelleExpr) ⇒ String
A pretty-printer for the Bellerophon tactics language.
A pretty-printer for the Bellerophon tactics language.
- Note
Prefer this implementation over BelleExpr.prettyString.
- object CLOSE_PAREN extends BelleTerminal
- object COLON extends BelleTerminal
- object COMMA extends BelleTerminal
- object EOF extends BelleTerminal
- object OPEN_PAREN extends BelleTerminal
- object SEQ_COMBINATOR extends BelleTerminal
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 structuresExpression
- Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (one-pass) uniform substitutions and renaming.StaticSemantics
- Static semantics with free and bound variable analysisKeYmaeraXParser
.edu.cmu.cs.ls.keymaerax.parser
- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter
- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser
- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser
- Parser reading KeYmaera X model and proof archive.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.cmu.cs.ls.keymaerax.infrastruct
- Prover infrastructure outside the kernelUnificationMatch
- Unification algorithmRenUSubst
- 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 functionalityExpressionTraversal
- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon
- Bellerophon tactic language and tactic interpreterBelleExpr
- Tactic language expressionsSequentialInterpreter
- Sequential tactic interpreter for Bellerophon tacticsedu.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 logicSequentCalculus
- Sequent Calculus for propositional and first-order logicHybridProgramCalculus
- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
- 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 conclusionsedu.cmu.cs.ls.keymaerax.lemma
- Lemma mechanismLemma
- 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 solversMathematicaQETool
- 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 informationedu.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