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 infrastruct

The infrastruct package provides central prover infrastructure such as unification and augmented formula analysis.

The infrastruct package provides central prover infrastructure such as unification and augmented formula analysis. This infrastructure is of basic interest and useful independently of any particular tactic language etc.

Main functionality:

Position with PosInExpr positioning within subformulas.
Context Convenience representation of formulas used as contexts that provide ways of substituting expressions in by conceptually splitting and managing the context around a position in a formula.
RenUSubst Renaming Uniform Substitutions that quickly combine and ultimately reduce to uniform renaming and uniform substitution of the kernel.
UnificationMatch single-sided matching unification algorithms.
Augmentors: Implicit convenience additions of helper functions to formulas, terms, programs, sequents that are useful for analysis and transformation.
ExpressionTraversal generic functionality for traversing expressions for analysis or transformation.

Definition Classes: keymaerax
See also: edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus

AntePosition

Augmentors

BaseMatcher

Context

DependencyAnalysis

DirectUSubstAboveURen

ExpressionTraversal

FastURenAboveUSubst

FastUSubstAboveURen

FormulaTools

FreshUnificationMatch

InsistentMatcher

LinearMatcher

Matcher

MultiRename

NonSubstUnificationMatch

PosInExpr

Position

ProvableHelper

RenUSubst

RenUSubstBase

RestrictedBiDiUnificationMatch

SchematicComposedUnificationMatch

SchematicUnificationMatch

StaticSemanticsTools

Statistics

SubstitutionHelper

SuccPosition

TopAntePosition

TopPosition

TopSuccPosition

TreeForm

URenSubstitutionPair

USubstAboveURen

USubstRenChurch

USubstRenOne

UnificationMatch

UnificationMatchBase

UnificationMatchUSubstAboveURen

UnificationTools

UniformMatcher

UniformMatching

edu.cmu.cs.ls.keymaerax.infrastruct

RenUSubstBase

abstract class RenUSubstBase extends RenUSubst

Base class for many common Renaming Uniform Substitution, combining URename and USubst. Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution.

See also: edu.cmu.cs.ls.keymaerax.core.URename
edu.cmu.cs.ls.keymaerax.core.USubst
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()

Linear Supertypes

RenUSubst, (Expression) ⇒ Expression, AnyRef, Any

Known Subclasses

DirectUSubstAboveURen, USubstAboveURen

Ordering

Alphabetic
By Inheritance

Inherited

RenUSubstBase
RenUSubst
Function1
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Instance Constructors

new RenUSubstBase(subsDefsInput: Seq[(Expression, Expression)])

Type Members

type RenUSubstRepl = (Expression, Expression)
A renaming substitution pair for a renaming uniform substitution.
A renaming substitution pair for a renaming uniform substitution.

Definition Classes
RenUSubst
See also
edu.cmu.cs.ls.keymaerax.core.SubstitutionPair
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()

Abstract Value Members

abstract def apply(p: DifferentialProgram): DifferentialProgram

Definition Classes
RenUSubst
abstract def apply(p: Program): Program

Definition Classes
RenUSubst
abstract def apply(f: Formula): Formula

Definition Classes
RenUSubst
abstract def apply(t: Term): Term

Definition Classes
RenUSubst
abstract def toCore: (Expression) ⇒ Expression
This RenUSubst implemented strictly from the core.
This RenUSubst implemented strictly from the core.

Definition Classes
RenUSubst
Note
For contract purposes
abstract def toForward: (ProvableSig) ⇒ ProvableSig
Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.
Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.

Definition Classes
RenUSubst
abstract def toTactic(form: Sequent): BelleExpr
Convert to tactic to reduce to form by successively using the respective uniform renaming and uniform substitution rules

Concrete Value Members

final def !=(arg0: Any): Boolean

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

Definition Classes
AnyRef → Any
def ++(other: RenUSubst): RenUSubst
Union of renaming uniform substitutions, i.e., both replacement lists merged.
Union of renaming uniform substitutions, i.e., both replacement lists merged.

Definition Classes
RenUSubst
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A

Definition Classes
Function1
Annotations
@unspecialized()
def apply(s: Sequent): Sequent
Apply everywhere in the sequent.
Apply everywhere in the sequent.

Definition Classes
RenUSubst
def apply(e: Expression): Expression

Definition Classes
RenUSubst → Function1
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @throws( ... )
def compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression

Definition Classes
Function1
Annotations
@unspecialized()
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 getRenamingTactic: BelleExpr
Get the renaming tactic part
Get the renaming tactic part

Definition Classes
RenUSubstBase → RenUSubst
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@native()
def isEmpty: Boolean
Returns true if there is no replacement.
Returns true if there is no replacement.

Definition Classes
RenUSubst
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 renaming: RenUSubst
The uniform renaming part of this renaming uniform substitution
The uniform renaming part of this renaming uniform substitution

Definition Classes
RenUSubstBase → RenUSubst
final val rens: Seq[(Variable, Variable)]
Renaming part, with identity renaming no-ops filtered out.
Renaming part, with identity renaming no-ops filtered out.

Attributes
protected
final val subsDefs: Seq[SubstitutionPair]
Substitution part, with identity substitution no-ops filtered out.
Substitution part, with identity substitution no-ops filtered out.

Attributes
protected
def substitution: RenUSubst
The uniform substitution part of this renaming uniform substitution
The uniform substitution part of this renaming uniform substitution

Definition Classes
RenUSubstBase → RenUSubst
See also
usubst
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def toString(): String

Definition Classes
RenUSubstBase → Function1 → AnyRef → Any
final lazy val usubst: USubst
The uniform substitution part of this renaming uniform substitution
The uniform substitution part of this renaming uniform substitution

Definition Classes
RenUSubstBase → RenUSubst
Note
lazy val and postponing applicable() until actual use case would make it possible for useAt(inst) to modify before exception. Not sure that's worth it though.
See also
substitution
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

RenUSubstBase

abstract class RenUSubstBase extends RenUSubst

Instance Constructors

Type Members

Abstract Value Members

Concrete Value Members

Inherited from RenUSubst

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

RenUSubstBase 

abstract class RenUSubstBase extends RenUSubst

Instance Constructors

Type Members

Abstract Value Members

Concrete Value Members

Inherited from RenUSubst

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped

RenUSubstBase