package cdgl
- Alphabetic
- Public
- All
Type Members
- case class AndEL(child: Proof) extends Proof with Product with Serializable
- case class AndER(child: Proof) extends Proof with Product with Serializable
- case class AndI(left: Proof, right: Proof) extends Proof with Product with Serializable
- case class BAssignE(child: Proof) extends Proof with Product with Serializable
- case class BAssignI(e: Assign, child: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class BChoiceEL(child: Proof) extends Proof with Product with Serializable
- case class BChoiceER(child: Proof) extends Proof with Product with Serializable
- case class BChoiceI(left: Proof, right: Proof) extends Proof with Product with Serializable
- case class BComposeE(child: Proof) extends Proof with Product with Serializable
- case class BComposeI(child: Proof) extends Proof with Product with Serializable
- case class BDualE(child: Proof) extends Proof with Product with Serializable
- case class BDualI(child: Proof) extends Proof with Product with Serializable
- case class BRandomE(child: Proof, f: Term) extends Proof with Product with Serializable
- case class BRandomI(x: Variable, child: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class BRepeatEL(child: Proof) extends Proof with Product with Serializable
- case class BRepeatER(child: Proof) extends Proof with Product with Serializable
- case class BRepeatI(pre: Proof, step: Proof, post: Proof, a: Program, ys: Option[List[Variable]] = None) extends Proof with Product with Serializable
- case class BSolve(ode: ODESystem, post: Formula, child: Proof, s: Variable = Variable("s"), t: Variable = Variable("t"), ys: Option[List[Variable]] = None) extends Proof with Product with Serializable
- case class BTestE(left: Proof, right: Proof) extends Proof with Product with Serializable
- case class BTestI(fml: Formula, child: Proof) extends Proof with Product with Serializable
- case class Compare(f: Term, g: Term, kPos: Proof) extends Proof with Product with Serializable
-
case class
ConstantMetric(t: Term, theGhost: Variable, child: Proof) extends Metric with Product with Serializable
Constant metric requires real scalar term t to decrease by at least positive constant n each iteration, and stores previous metric value in theGhost.
-
final
case class
Context(c: List[Formula]) extends Product with Serializable
A context is a conjunction of assumption formulas.
A context is a conjunction of assumption formulas. Variable references proceed from the head of the list and binding rules introduce assumptions at the head, i.e., assumption 0 is the first element and the most recently added.
- c
List of assumptions
- case class DAssignE(child: Proof) extends Proof with Product with Serializable
- case class DAssignI(e: Assign, child: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class DC(left: Proof, right: Proof) extends Proof with Product with Serializable
- case class DChoiceE(child: Proof, left: Proof, right: Proof) extends Proof with Product with Serializable
- case class DChoiceIL(other: Program, child: Proof) extends Proof with Product with Serializable
- case class DChoiceIR(other: Program, child: Proof) extends Proof with Product with Serializable
- case class DComposeE(child: Proof) extends Proof with Product with Serializable
- case class DComposeI(child: Proof) extends Proof with Product with Serializable
- case class DDualE(child: Proof) extends Proof with Product with Serializable
- case class DDualI(child: Proof) extends Proof with Product with Serializable
- case class DG(init: Assign, rhs: Plus, child: Proof) extends Proof with Product with Serializable
- case class DGo(child: Proof) extends Proof with Product with Serializable
- case class DI(ode: ODESystem, pre: Proof, step: Proof, ys: Option[List[Variable]] = None) extends Proof with Product with Serializable
- case class DRandomE(left: Proof, right: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class DRandomI(e: Assign, child: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class DRepeatE(child: Proof, post: Proof, step: Proof) extends Proof with Product with Serializable
- case class DRepeatI(m: Metric, init: Proof, step: Proof, post: Proof) extends Proof with Product with Serializable
- case class DSolve(ode: ODESystem, post: Formula, durPos: Proof, dc: Proof, child: Proof, s: Variable = Variable("s"), t: Variable = Variable("t"), ys: Option[List[Variable]] = None) extends Proof with Product with Serializable
- case class DStop(child: Proof, other: Program) extends Proof with Product with Serializable
- case class DTestEL(child: Proof) extends Proof with Product with Serializable
- case class DTestER(child: Proof) extends Proof with Product with Serializable
- case class DTestI(left: Proof, right: Proof) extends Proof with Product with Serializable
- case class DV(const: Proof, dur: Proof, rate: Proof, post: Proof, t: Variable = Variable("t"), ys: Option[List[Variable]] = None) extends Proof with Product with Serializable
- case class DW(ode: ODESystem, child: Proof, ys: Option[List[Variable]] = None) extends Proof with Product with Serializable
- case class EquivEL(child: Proof, assump: Proof) extends Proof with Product with Serializable
- case class EquivER(child: Proof, assump: Proof) extends Proof with Product with Serializable
- case class EquivI(fml: Equiv, left: Proof, right: Proof) extends Proof with Product with Serializable
- case class ExistsE(left: Proof, right: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class ExistsI(e: Assign, child: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class FalseE(child: Proof, fml: Formula) extends Proof with Product with Serializable
- case class ForallE(child: Proof, f: Term) extends Proof with Product with Serializable
- case class ForallI(x: Variable, child: Proof, y: Option[Variable] = None) extends Proof with Product with Serializable
- case class Hyp(p: ProofVariable) extends Proof with Product with Serializable
- case class ImplyE(left: Proof, right: Proof) extends Proof with Product with Serializable
- case class ImplyI(fml: Formula, child: Proof) extends Proof with Product with Serializable
-
final
case class
Judgement(ante: Context, succ: Formula) extends Product with Serializable
Judgement G |- P is a context G with a single succedent formula P
-
sealed
trait
Metric extends AnyRef
An effectively-well-found convergence metric used for Angelic loop convergence reasoning <*>
- case class Mon(left: Proof, right: Proof, ys: Option[List[Variable]] = None) extends Proof with Product with Serializable
- case class NotE(left: Proof, right: Proof) extends Proof with Product with Serializable
- case class NotI(p: Formula, child: Proof) extends Proof with Product with Serializable
- case class OrE(child: Proof, left: Proof, right: Proof) extends Proof with Product with Serializable
- case class OrIL(other: Formula, child: Proof) extends Proof with Product with Serializable
- case class OrIR(other: Formula, child: Proof) extends Proof with Product with Serializable
-
sealed
trait
Proof extends AnyRef
CdGL forward proof terms
-
case class
ProofException(msg: String, context: Context = Context.empty) extends Exception with Product with Serializable
Raised when a proof term does not proof check
Raised when a proof term does not proof check
- msg
Description of error
- case class QE(p: Formula, child: Proof) extends Proof with Product with Serializable
- case class Triv() extends Proof with Product with Serializable
Value Members
- object Context extends Serializable
- object Proof
-
object
ProofChecker
Checks proof terms.
Checks proof terms.
- See also
- object TermTactics
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