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

Proof term language
edu.cmu.cs.ls.keymaerax.pt.ProofChecker to interpret the proof term language

Definition Classes: keymaerax

AxiomTerm

BananaODE

ConSubst

ConversionException

Defun

DefunSubst

Depred

DepredSubst

ElidingProvable

FOLRConstant

ForwardNewConsequenceTerm

FunSubst

HOLConverter

IAAllElim

IABoxSplit

IADC

IADE

IADG

IADIEq

IADS

IADW

IADiffEffectSys

IADiffLinear

IAEqualCommute

IAEquivReflexive

IAI

IAImpSelf

IAK

IAV

IAallInst

IAassign

IAassignEq

IAassignany

IAbox

IAchoice

IAcompose

IAconstFcong

IAdConst

IAdMinus

IAdMult

IAdPlus

IAdassign

IAdvar

IAllSpace

IAloopIter

IAnd

IAndL

IAndR

IApplyLrule

IApplyRrule

IAssign

IAssignRand

IAtest

IAx

IAxRule

IBRenameL

IBRenameR

ICE

ICQ

ICT

IChoice

ICloseId

ICohide2

ICohideR

ICohideRR

ICommuteEquivR

IConst

ICut

ICutLeft

ICutRight

IDIGeqSchema

IDMap

IDiamond

IDiffAssign

IDiffVar

IDifferential

IEquivBackwardL

IEquivForwardL

IEquivL

IEquivR

IEquivifyR

IEvolveODE

IExists

IFNC

IFOLRConstant

IFunction

IFunctional

IGeq

IHideL

IHideR

IImplyL

IImplyR

IInContext

ILoop

INBSpace

INot

INotL

IODE

IOProd

IOSing

IOVar

IPlus

IPrUSubst

IPro

IProp

IPvar

IRuleApplication

ISequence

ISkolem

IStart

ISub

ITest

ITimes

ITrueR

IURename

IVar

Iaxiom

IaxiomaticRule

Iformula

Ihp

Ilrule

Imonb

Ipt

Irrule

IruleApp

IsabelleConverter

Ispace

Isubst

Itrm

NoProof

NonSubst

ProlongationTerm

ProofChecker

ProofTerm

ProvableSig

RuleApplication

RuleTerm

ScalaBuilder

SexpBuilder

SourceBuilder

StartProof

Sub

SymMode

TermProvable

URenameTerm

UsubstProvableTerm

edu.cmu.cs.ls.keymaerax.pt

ProvableSig

Companion trait ProvableSig

object ProvableSig

See also: Provable

Linear Supertypes

AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

ProvableSig
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Value Members

final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
var PROOF_TERMS_ENABLED: Boolean
Whether to use proof terms instead of eliding them
final def asInstanceOf[T0]: T0

Definition Classes
Any
val axiom: Map[String, Formula]
immutable list of sound axioms, i.e., valid formulas of differential dynamic logic.
immutable list of sound axioms, i.e., valid formulas of differential dynamic logic. (convenience method)
def axioms: Map[String, ProvableSig]
immutable list of Provables of sound axioms, i.e., valid formulas of differential dynamic logic.
immutable list of Provables of sound axioms, i.e., valid formulas of differential dynamic logic.
```
    *
---------- (axiom)
 |- axiom
```
See also
"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, 2015."
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @throws( ... )
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@native()
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@native()
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@native()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@native()
def proveArithmetic(t: QETool, f: Formula): ProvableSig
def proveArithmeticLemma(t: QETool, f: Formula): Lemma
Proves a formula f in real arithmetic using an external tool for quantifier elimination.
Proves a formula f in real arithmetic using an external tool for quantifier elimination.
t
The quantifier-elimination tool.
f
The formula.
returns
a Lemma with a quantifier-free formula equivalent to f and evidence as provided by the tool.
def rules: Map[String, ProvableSig]
immutable list of Provables of locally sound axiomatic proof rules.
immutable list of Provables of locally sound axiomatic proof rules.
```
 Gi |- Di
---------- (axiomatic rule)
  G |- D
```
See also
"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, 2015."
Provable.apply(USubst)
def startPlainProof(goal: Formula): ProvableSig
Starts a proof without definitions.
def startPlainProof(goal: Sequent): ProvableSig
Starts a proof without definitions.
def startProof(goal: Formula, defs: Declaration): ProvableSig
Begin a new proof for the desired conclusion formula from no antecedent.
Begin a new proof for the desired conclusion formula from no antecedent.
```
 |- goal
---------
 |- goal
```
goal
the desired conclusion formula for the succedent.
returns
a Provable whose subgoals need to be all proved in order to prove goal.
def startProof(goal: Sequent, defs: Declaration): ProvableSig
Begin a new proof for the desired conclusion goal
Begin a new proof for the desired conclusion goal
```
 goal
------
 goal
```
goal
the desired conclusion.
returns
a Provable whose subgoals need to be all proved in order to prove goal.
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def toString(): String

Definition Classes
AnyRef → Any
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@native() @throws( ... )

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

ProvableSig

Companion trait ProvableSig

object ProvableSig

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

ProvableSig 

Companion trait ProvableSig

object ProvableSig

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

ProvableSig