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 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.
- 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 left-hand side of the sequent turnstile.
A position guaranteed to identify an antecedent position, so on the left-hand 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 goal-directed 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 goal-directed 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() fast-forwards 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 goal-directed 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 goal-directed 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() fast-forwards 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 built-in names such as those in axioms).
Unification/matching algorithm for fresh shapes (with built-in 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 single-pass matcher.- Note
Expects shape to have fresh names that do not occur in the input. Usually shape has all built-in 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 single-sided 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 type-preserving 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 single-pass 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 single-pass 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 right-hand side of the sequent turnstile.
A position guaranteed to identify a succedent position, so on the right-hand side of the sequent turnstile.
- See also
SuccPos
Sequent
-
trait
TopAntePosition extends AntePosition with TopPosition
A top-level antecedent position
-
trait
TopPosition extends Position
A position guaranteed to identify a top-level position
-
trait
TopSuccPosition extends SuccPosition with TopPosition
A top-level 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 Church-style 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 one-pass 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 single-pass 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 single-pass 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
Non-critical 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 single-sided 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 (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