package infrastruct
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 singlesided 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.
 Alphabetic
 By Inheritance
 infrastruct
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

trait
AntePosition extends Position
A position guaranteed to identify an antecedent position, so on the lefthand side of the sequent turnstile.
A position guaranteed to identify an antecedent position, so on the lefthand side of the sequent turnstile.
 See also
AntePos
Sequent

trait
BaseMatcher extends Matcher with Logging
Basic matcher infrastructure that simply forwards all unification functionality to BaseMatcher.unify().
Basic matcher infrastructure that simply forwards all unification functionality to BaseMatcher.unify(). Only apply() functions wrap exceptions in context while unify() functions simply pass it upwards.

sealed
trait
Context[+T <: Expression] extends (Expression) ⇒ Formula
Convenience wrapper around contexts such as f(.) or p(.) or C{_} to make it easy to instantiate their arguments.
Convenience wrapper around contexts such as f(.) or p(.) or C{_} to make it easy to instantiate their arguments.
 T
the type/kind of expression that this context is representing.
Split a formula at a position into subformula and its context, then instantiate this context with other subformulas:
val parser = KeYmaeraXParser val f = parser("x^2>=0 & x<44 > [x:=2;{x'=1&x<=10}]x>=1") // split f into context ctx and subformula g such that f is ctx{g} val (ctx,g) = Context.at(f, PosInExpr(1::1::Nil)) println(f + " is the same as " + ctx(g)) // put another formula h in in place of g val h = parser("x^2>y") // x^2>=0 & x<44 > [x:=2;{x'=1&x<=10}]x^2>y) val result = ctx(h) println(result)
Example: 
final
class
DirectUSubstAboveURen extends RenUSubstBase
Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substitution.
Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substitution.
s(RG)  s(RD)  USubst RG  RD  URen G  D
Semantic renaming may be supported if need be.
DirectUSubstAboveURen is a direct implementation in tactics land of a joint renaming and substitution algorithm. It uses a single direct fast USubstRen for direct internal applications via DirectUSubstAboveURen.apply() but schedules separate uniform substitutions and uniform renamings to the core when asked. The first fast pass supports semantic renaming, which is useful during unification to "apply" renamings already to predicationals without clash. The final core pass does not support semantic renaming, but is only needed for the final unifier.
 Note
reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.
 See also

final
class
FastURenAboveUSubst extends RenUSubst
Fast implementation of: Renaming Uniform Substitution that, in goaldirected backwards Sequent direction, first runs a uniform substitution below and on the result subsequently the uniform renaming above it.
Fast implementation of: Renaming Uniform Substitution that, in goaldirected backwards Sequent direction, first runs a uniform substitution below and on the result subsequently the uniform renaming above it.
R(s(G))  R(s(D))  URen s(G)  s(D)  USubst G  D
The direct application mechanism via apply() fastforwards to the fast joint USubstRen infrastructure. Its tactical / prover core implementation works in sync using prover core operations by scheduling separate uniform substitutions and uniform renamings to the core when asked.
Cleverly exploits semantic renaming on Provables on demand (although not in full generality yet).
 Note
reading in Hilbert direction from top to bottom, the uniform renaming comes abiove first then the subsequent uniform substitution comes below as second.
 See also

final
class
FastUSubstAboveURen extends RenUSubst
Fast implementation of: Renaming Uniform Substitution that, in goaldirected backwards Sequent direction, first runs a uniform renaming below and on the result subsequently the uniform substitution above it.
Fast implementation of: Renaming Uniform Substitution that, in goaldirected backwards Sequent direction, first runs a uniform renaming below and on the result subsequently the uniform substitution above it.
s(RG)  s(RD)  USubst RG  RD  URen G  D
The direct application mechanism via apply() fastforwards to the fast joint USubstRen infrastructure. Its tactical / prover core implementation works in sync using prover core operations by scheduling separate uniform substitutions and uniform renamings to the core when asked.
 Note
reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.
 See also

class
FreshUnificationMatch extends SchematicComposedUnificationMatch
Unification/matching algorithm for fresh shapes (with builtin names such as those in axioms).
Unification/matching algorithm for fresh shapes (with builtin names such as those in axioms). Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast singlepass matcher. Note
Expects shape to have fresh names that do not occur in the input. Usually shape has all builtin names ending in underscore _ and no input is like that.

trait
InsistentMatcher extends Matcher with Logging
A matcher that insists on always matching as if there were arbitrary expressions as opposed to specializing to Term versus Formula etc.

trait
Matcher extends (Expression, Expression) ⇒ RenUSubst
Matcher(shape, input)
matches second argumentinput
against the patternshape
of the first argument but not vice versa.Matcher(shape, input)
matches second argumentinput
against the patternshape
of the first argument but not vice versa. Matcher leavesinput
alone and only substitutes intoshape
, i.e., gives a singlesided matcher.The following notation is used to indicate that
u
is the unifier computed for matching inputt
against shapes
:s = t  u
That is
u
is the result of callingMatcher.apply(s,t)
.val s = Matcher("p()&q()".asFormula, "x<=0 & x^2>=0".asFormula) // gives {p() ~> x<=0, q() ~> x^2>=0} println(s)
, val s = Matcher("[a;++b;]p()".asFormula, "[x:=x+1; ++ {x'=x}]y<=0".asFormula) // gives {a ~> x:=x+1, b ~> {x'=x}, p() ~> y<=0} println(s)
, val s = Matcher("[a;++b;]p()".asFormula, "[x:=x+1; ++ {x'=x}]x>=0".asFormula) // gives {a ~> x:=x+1, b ~> {x'=x}, p() ~> x>=0} println(s)
, // will throw UnificationException val s = Matcher("[a;++b;]p()".asFormula, "[x:=x+1;{x'=x}]x>=0".asFormula)
 See also
UnificationException
Examples: 
final
case class
MultiRename(rens: Seq[(Variable, Variable)], semantic: Boolean = true) extends (Expression) ⇒ Expression with Product with Serializable
Uniformly rename multiple variables at once.
Uniformly rename multiple variables at once. Uniformly all occurrences of
what
andwhat'
torepl
andrepl'
and vice versa, for all (what,repl) in renames.Performs semantic renaming, i.e. leaves program constants etc. unmodified.
 semantic
true
to also support program constants, predicationals etc and leaving them unmodified. 'false' to clash instead.

sealed
case class
PosInExpr(pos: List[Int] = Nil) extends Product with Serializable
Positions identify subexpressions of an expression.
Positions identify subexpressions of an expression. A position is a finite sequence of binary numbers where
0
identifies the left or only subexpression of an expression and1
identifies the right subexpression of an expression. For example,0.1
is the right child of the left child. And,0.1.0.0
is the left child of the left child of the right child of the left child.
import StringConverter._ val fml = "(x>2 & x+1<9) > [x:=2*x+1; y:=0;] x^2>=2".asFormula // explicitly use FormulaAugmentor print(FormulaAugmentor(fml).sub(PosInExpr(0::0::Nil))) // x>2 // implicitly use FormulaAugmentor functions on formulas import Augmentors._ print(fml.sub(PosInExpr(0::0::Nil))) // x>2; print(fml.sub(PosInExpr(0::1::Nil))) // x+1<9 print(fml.sub(PosInExpr(0::1::0::Nil))) // x+1 print(fml.sub(PosInExpr(0::1::0::0::Nil))) // x print(fml.sub(PosInExpr(0::1::0::1::Nil))) // 1 print(fml.sub(PosInExpr(0::1::1::Nil))) // 9 print(fml.sub(PosInExpr(1::1::Nil))) // x^2>=2 print(fml.sub(PosInExpr(1::0::Nil))) // x:=2*x+1; y:=0; print(fml.sub(PosInExpr(1::0::0::Nil))) // x:=2*x+1; print(fml.sub(PosInExpr(1::0::1::Nil))) // y:=0; print(fml.sub(PosInExpr(1::0::0::1::Nil))) // 2*x+1
 See also
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.positionOf()
Context.at()
Context.replaceAt()
Context.splitPos()
Example: 
sealed
trait
Position extends AnyRef
Position at which formula and subexpresion ofa a sequent to apply a tactic.
Position at which formula and subexpresion ofa a sequent to apply a tactic.
 To do
use AntePos and SuccPos directly instead of index etc.
Position should essentially become a nice typepreserving name for a pair of a SeqPos and a PosInExpr.
 See also

sealed
trait
RenUSubst extends (Expression) ⇒ Expression
Renaming Uniform Substitution, combining URename and USubst in a way that has both a direct application like apply functions of USubstRen as well as a translation to equivalent tactical/core prover operations.
Renaming Uniform Substitution, combining URename and USubst in a way that has both a direct application like apply functions of USubstRen as well as a translation to equivalent tactical/core prover operations.
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.infrastruct.Augmentors.TermAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()

abstract
class
RenUSubstBase extends RenUSubst
Base class for many common Renaming Uniform Substitution, combining URename and USubst.
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.infrastruct.Augmentors.TermAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()
 class RestrictedBiDiUnificationMatch extends FreshUnificationMatch

abstract
class
SchematicComposedUnificationMatch extends SchematicUnificationMatch
Generic schematic unification/matching algorithm for tactics.
Generic schematic unification/matching algorithm for tactics. Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast singlepass matcher. Defined by recursive unification from compositions. 
abstract
class
SchematicUnificationMatch extends BaseMatcher
Generic schematic unification/matching algorithm for tactics.
Generic schematic unification/matching algorithm for tactics. Their
unify(shape, input)
function matches second argumentinput
against the patternshape
of the first argument, but not vice versa. Thus, the matcher leavesinput
alone and only substitutes intoshape
. Reasonably fast singlepass matcher that is defined by recursive unification from compositions. Note
Central recursive unification implementation.
 See also
 class SubstitutionHelper extends AnyRef

trait
SuccPosition extends Position
A position guaranteed to identify a succedent position, so on the righthand side of the sequent turnstile.
A position guaranteed to identify a succedent position, so on the righthand side of the sequent turnstile.
 See also
SuccPos
Sequent

trait
TopAntePosition extends AntePosition with TopPosition
A toplevel antecedent position

trait
TopPosition extends Position
A position guaranteed to identify a toplevel position

trait
TopSuccPosition extends SuccPosition with TopPosition
A toplevel succedent position

final
case class
URenSubstitutionPair(what: Expression, repl: Expression) extends Product with Serializable
Like a edu.cmu.cs.ls.keymaerax.core.SubstitutionPair replacing
what~>repl
but not checked for substitutability.Like a edu.cmu.cs.ls.keymaerax.core.SubstitutionPair replacing
what~>repl
but not checked for substitutability. 
final
class
USubstAboveURen extends RenUSubstBase
Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
s(RG)  s(RD)  USubst RG  RD  URen G  D
 Note
reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.

type
USubstRen = USubstRenOne
Choice of standalone Renaming Uniform Substitution operation implementation

final
case class
USubstRenChurch(subsDefsInput: Seq[(Expression, Expression)]) extends (Expression) ⇒ Expression with Product with Serializable
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst.
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst. This implementation uses Churchstyle uniform substitution implementation a la USubstChurch. 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, simultaneously.
 Note
This implementation performs semantic renaming.
 See also

final
case class
USubstRenOne(subsDefsInput: Seq[(Expression, Expression)]) extends (Expression) ⇒ Expression with Product with Serializable
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst to uniformly substitute while simultaneously uniformly renaming multiple variables.
Standalone Renaming Uniform Substitution operation, simultaneously combining URename and USubst to uniformly substitute while simultaneously uniformly renaming multiple variables.
This implementation uses onepass uniform substitution implementation a la USubstOne. 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, simultaneously.
 Note
This implementation performs semantic renaming.
 See also

class
UnificationMatchBase extends SchematicComposedUnificationMatch
Generic base for unification/matching algorithm for tactics.
Generic base for unification/matching algorithm for tactics. Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast singlepass matcher.  class UnificationMatchUSubstAboveURen extends Matcher with Logging
 class UniformMatcher extends UniformMatching

abstract
class
UniformMatching extends BaseMatcher
Uniform Matching algorithm for tactics by sweeping.
Uniform Matching algorithm for tactics by sweeping. Their
unify(shape, input)
function matches second argumentinput
against the patternshape
of the first argument, but not vice versa. Uniform matching leavesinput
alone and only substitutes intoshape
. Fast singlepass matcher that is defined by sweeping uniform matching.Sweeping Uniform Matching is provably sound and is fast but not necessarily complete.
 Note
Central recursive unification implementation.
,a more comprehensive unification matcher would be found when jointly abstracting replacements at join conflicts if those have a joint lattice sup/inf.
 See also
Value Members

def
USubstRen(subsDefsInput: Seq[(Expression, Expression)]): USubstRen
USubstRen factory method for standalone Renaming Uniform Substitution operation implementation, forwards to constructor.

object
AntePosition
An antecedent position of a sequent indexed base 1, so positions 1, 2, 3, ...

object
Augmentors
If imported, automatically augments core data structures with convenience wrappers for tactic purposes such as subexpression positioning, context splitting, and replacements.
If imported, automatically augments core data structures with convenience wrappers for tactic purposes such as subexpression positioning, context splitting, and replacements.
To use this implicit augmentation automatically, import it via
import edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors._
Then use it as if its methods were part of the data structures
val parser = KeYmaeraXParser val f = parser("x^2>=0 & x<44 > [x:=2;{x'=1&x<=10}]x>=1") // will obtain the x>=1 part val someSub = f.sub(PosInExpr(1::1::Nil)) println(someSub) // construct x^2>=0 & x<44 > [x:=2;{x'=1&x<=10}]x^2>y val other = f.replaceAt(PosInExpr(1::1::Nil), parser("x^2>y")) println(other)
 See also
Example: 
object
Context
Context management, position splitting, and extraction tools.
Context management, position splitting, and extraction tools. Useful for splitting a formula at a position into the subexpression at that position and the remaining context around it. Or for replacing a subexpression by another subexpression at all cost. Or for splitting a position into a formula position and a term position.
Split a formula at a position into subformula and its context
val parser = KeYmaeraXParser val f = parser("x^2>=0 & x<44 > [x:=2;{x'=1&x<=10}]x>=1") // split f into context ctx and subformula g such that f is ctx{g} val (ctx,g) = Context.at(f, PosInExpr(1::1::Nil)) // x^2>=0 & x<44 > [x:=2;{x'=1&x<=10}]_ println(ctx) // x>=1 println(f) println(f + " is the same as " + ctx(g))
 See also
Example: 
object
DependencyAnalysis
Dependency Analysis For a set of output variables, determine the set of input variables across a hybrid program that could affect their values

object
ExpressionTraversal
Generic traversal functionality for expressions for pre/post/infix traversal.

object
FormulaTools extends Logging
Tactic tools for formula manipulation and extraction.

object
LinearMatcher extends SchematicUnificationMatch
LinearMatcher(shape, input) matches second argument
input
against the LINEAR patternshape
of the first argument but not vice versa.LinearMatcher(shape, input) matches second argument
input
against the LINEAR patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into linear shape.Linear matchers require linear shapes, so no symbol can occur twice in the shape. If a symbol does occur twice, it is assumed that the identical match is found in all use cases, which is a strong assumption and can lead to unpredictable behavior. Implemented by a fast single pass. Possibly depends on using straight USubstRenOne
Matching the formula on the right against a linear pattern shape
LinearMatcher.unify("[a;](p()&q())".asFormula, "[x:=2*x;{x'=5}](0<=x&x>=y)".asFormula)
, Except when lucky, nonlinear patterns will not be matched correctly by LinearMatcher even if they are unifiable.
LinearMatcher.unify("p(f())<>[x:=f()]p(x)".asFormula, "(2*x)^2>=2*x<>[x:=2*x;]x^2>=x".asFormula)
Examples:  object Matcher

object
NonSubstUnificationMatch extends FreshUnificationMatch
Unify any term for variables in ODEs.
 object PosInExpr extends Serializable
 object Position

object
ProvableHelper
Noncritical infrastructure to transform and substitute provables.
 object RenUSubst
 object RestrictedBiDiUnificationMatch extends RestrictedBiDiUnificationMatch

object
StaticSemanticsTools
Additional tools read off from the static semantics for the tactics.
Additional tools read off from the static semantics for the tactics.

object
Statistics
Formula, term, and tactic statistics.

object
SubstitutionHelper
Created by smitsch on 2/19/15.
Created by smitsch on 2/19/15.
 To do
generalize to replacing formula by formula, too.

object
SuccPosition
A succedent position of a sequent indexed base 1, so positions 1, 2, 3, ...

object
TreeForm
Represent terms as recursive lists of logical symbols.
Represent terms as recursive lists of logical symbols. This simplified structure is useful for certain analyses that treat all the operators in a relatively uniform way. This representation flattens the term's structure as much as possible (e.g. turning a+(b+c) into (a+b+c)), to make analyses that consider the depth of a term more meaningful. Created by bbohrer on 10/23/15.
 object USubstRenChurch extends Serializable

object
UnificationMatch extends FreshUnificationMatch
Unification/matching algorithm for tactics.
Unification/matching algorithm for tactics.
Unify(shape, input)
matches second argumentinput
against the patternshape
of the first argument but not vice versa. Matcher leavesinput
alone and only substitutes intoshape
, i.e., gives a singlesided matcher. See also
 object UnificationTools
 object UniformMatcher extends UniformMatcher
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 (onepass) 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 firstorder logicHybridProgramCalculus
 Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
 Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
 Unificationbased 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 backend solversMathematicaQETool
 Mathematica interface for real arithmetic.Z3QETool
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
 Extended backends 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
 Commandline launcher for KeYmaera X supports commandline argumenthelp
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
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface 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. 219265, 2017.
2. Nathan Fulton, Stefan Mitsch, JanDavid 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. 527538. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018. Videos