package core
KeYmaera X Kernel is the soundnesscritical core of the Axiomatic Tactical Theorem Prover KeYmaera X.
KeYmaera X Kernel
The KeYmaera X Kernel implements Differential Dynamic Logic and defines
 Syntax of differential dynamic logic:
 Proof Construction of proof certificates from
 Provides basic Stored Provables as Strings, real arithmetic interfaces, error reporting, and set lattice management for sets of symbols.
Usage Overview
The KeYmaera X Kernel package provides the soundnesscritical core of KeYmaera X. It provides ways of constructing proofs that, by construction, can only be constructed using the proof rules that the KeYmaera X Kernel provides. The proof tactics that KeYmaera X provides give you a more powerful and flexible and easier way of constructing and searching for proofs, but they internally reduce to what is shown here.
Constructing Proofs
The proof certificates of KeYmaera X are of type edu.cmu.cs.ls.keymaerax.core.Provable. edu.cmu.cs.ls.keymaerax.core.Provable.startProof(goal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable* begins a new proof of a edu.cmu.cs.ls.keymaerax.core.Sequent containing the conjectured differential dynamic logic formula. A proof rule of type edu.cmu.cs.ls.keymaerax.core.Rule can be applied to any subgoal of a edu.cmu.cs.ls.keymaerax.core.Provable by edu.cmu.cs.ls.keymaerax.core.Provable.apply(rule:edu\.cmu\.cs\.ls\.keymaerax\.core\.Rule,subgoal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable\.Subgoal):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable* to advance the proof until that Provable has been proved since edu.cmu.cs.ls.keymaerax.core.Provable.isProved is true. Subgoals are identified by integers.
import scala.collection.immutable._ val verum = new Sequent(IndexedSeq(), IndexedSeq(True)) // conjecture val provable = Provable.startProof(verum) // construct a proof val proof = provable(CloseTrue(SuccPos(0)), 0) // check if proof successful, i.e. no remaining subgoals if (proof.isProved) println("Successfully proved " + proof.proved)
Of course, edu.cmu.cs.ls.keymaerax.btactics make it much easier to describe proof search procedures compared to the above explicit proof construction. The tactics internally construct proofs this way, but add additional flexibility and provide convenient ways of expressing proof search strategies in a tactic language.
Combining Proofs
Multiple Provable objects for subderivations obtained from different sources can also be merged into a single Provable object by substitution with edu.cmu.cs.ls.keymaerax.core.Provable.apply(edu.cmu.cs.ls.keymaerax.core.Provable,Int). The above example can be continued to merge proofs as follows:
// ... continued from above val more = new Sequent(IndexedSeq(), IndexedSeq(Imply(Greater(Variable("x"), Number(5)), True))) // another conjecture val moreProvable = Provable.startProof(more) // construct another (partial) proof val moreProof = moreProvable(ImplyRight(SuccPos(0)), 0)(HideLeft(AntePos(0)), 0) // merge proofs by gluing their Provables together (substitution) val mergedProof = moreProof(proof, 0) // check if proof successful, i.e. no remaining subgoals if (mergedProof.isProved) println("Successfully proved " + mergedProof.proved)
More styles for proof construction are shown in Provable's.
Differential Dynamic Logic
The language of differential dynamic logic is described in KeYmaera X by its syntax and static semantics.
Syntax
The immutable algebraic data structures for the expressions of differential dynamic logic are of type edu.cmu.cs.ls.keymaerax.core.Expression. Expressions are categorized according to their kind by the syntactic categories of the grammar of differential dynamic logic:
1. terms are of type edu.cmu.cs.ls.keymaerax.core.Term of kind edu.cmu.cs.ls.keymaerax.core.TermKind
2. formulas are of type edu.cmu.cs.ls.keymaerax.core.Formula of kind edu.cmu.cs.ls.keymaerax.core.FormulaKind
3. hybrid programs are of type edu.cmu.cs.ls.keymaerax.core.Program of kind edu.cmu.cs.ls.keymaerax.core.ProgramKind
4. differential programs are of type edu.cmu.cs.ls.keymaerax.core.DifferentialProgram of kind edu.cmu.cs.ls.keymaerax.core.DifferentialProgramKind
See Section 2.1
Static Semantics
The static semantics of differential dynamic logic is captured in edu.cmu.cs.ls.keymaerax.core.StaticSemantics in terms of the free variables and bound variables that expressions have as well as their signatures (set of occurring symbols). See Section 2.4
Theorem Prover
The KeYmaera X Prover Kernel provides uniform substitutions, uniform and bound variable renaming, and axioms of differential dynamic logic. For efficiency, it also directly provides propositional sequent proof rules and Skolemization.
Axioms
The axioms and axiomatic rules of differential dynamic logic can be looked up with edu.cmu.cs.ls.keymaerax.core.Provable.axioms and edu.cmu.cs.ls.keymaerax.core.Provable.rules respectively. All available axioms are listed in edu.cmu.cs.ls.keymaerax.core.Provable.axioms, all available axiomatic rules are listed in edu.cmu.cs.ls.keymaerax.core.Provable.rules which both ultimately come from the file edu.cmu.cs.ls.keymaerax.core.AxiomBase. See Sections 4 and 5.0 Additional axioms are available as derived axioms and lemmas in edu.cmu.cs.ls.keymaerax.btactics.Ax.
Uniform Substitutions
Uniform substitutions uniformly replace all occurrences of a given predicate p(.) by a formula in (.) and likewise for function symbols f(.) and program constants. Uniform substitutions and their application mechanism for differential dynamic logic are implemented in edu.cmu.cs.ls.keymaerax.core.USubst. See Section 3 and onepass Section 3
Uniform substitutions can be used on proof certificates with the edu.cmu.cs.ls.keymaerax.core.Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubst):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*, including uniform substitution instances of axioms or axiomatic rules. See Section 3
Sequent Proof Rules
All proof rules for differential dynamic logic, including the uniform substitution and bound variable renaming rules as well as efficient propositional sequent proof rules and Skolemization edu.cmu.cs.ls.keymaerax.core.Skolemize are all of type edu.cmu.cs.ls.keymaerax.core.Rule, which are the only proof rules that can ever be applied to a proof. See sequent calculus
Additional Capabilities
Stored Provable Mechanism
A Stored Provable represents a Provable as a String that can be reloaded later as well as an interface to real arithmetic decision procedures are defined in edu.cmu.cs.ls.keymaerax.core.Provable.fromStorageString() and edu.cmu.cs.ls.keymaerax.core.QETool.
Error Reporting
Errors from the prover core are reported as exceptions of type edu.cmu.cs.ls.keymaerax.core.ProverException whose main responsibility is to propagate problems in traceable ways to the user by augmenting them with contextual information. The prover core throws exceptions of type edu.cmu.cs.ls.keymaerax.core.CoreException.
Set Lattice
A data structure for sets (or rather lattice completions of sets) is provided in edu.cmu.cs.ls.keymaerax.core.SetLattice based on Scala's immutable sets.
Overall Code Complexity
Overall, the majority of the KeYmaera X Prover Microkernel implementation consists of data structure declarations or similar mostly selfevident code. This includes straightforward variable categorization in StaticSemantics. The highest complexity is for the uniform substitution application mechanism. The highest information density is in the axiom list.
 Note
Code Review 20200217
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425441. Springer, 2019.
Andre Platzer and Yong Kiam Tan. Differential equation invariance axiomatization. J. ACM. 67(1), 6:16:66, 2020.
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
Andre Platzer. Uniform substitution for differential game logic. In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Automated Reasoning, 9th International Joint Conference, IJCAR 2018, volume 10900 of LNCS, pp. 211227. Springer 2018.
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
Nathan Fulton, Stefan Mitsch, JanDavid Quesel, Marcus Volp and Andre 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, LNCS. Springer, 2015.
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 1324. IEEE 2012
Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541550. IEEE 2012
Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143189, 2008.
 Alphabetic
 By Inheritance
 core
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

case class
And(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable
& logical conjunction: and.

case class
AndLeft(pos: AntePos) extends LeftRule with Product with Serializable
&L And left.
&L And left.
G, p, q  D  (&L And left) p&q, G  D

case class
AndRight(pos: SuccPos) extends RightRule with Product with Serializable
&R And right
&R And right
G  p, D G  q, D  (&R And right) G  p&q, D

case class
AntePos extends SeqPos with Product with Serializable
Antecedent Positions of formulas in a sequent, i.e.
Antecedent Positions of formulas in a sequent, i.e. in the assumptions on the left of the sequent arrow.

trait
ApplicationOf extends Composite
Function/predicate/predicational application.

class
Assertion extends AnyRef
A wrapper around the Java
assert
keyword.A wrapper around the Java
assert
keyword. Lazy evaluation of conditions and messages.Disabled by default. Enable at runtime with
java ea
. Disable withjava da
. 
case class
Assign(x: Variable, e: Term) extends AtomicProgram with Product with Serializable
x:=e assignment and/or differential assignment x':=e.

case class
AssignAny(x: Variable) extends AtomicProgram with Product with Serializable
x:=* nondeterministic assignment and/or nondeterministic differential assignment x':=*.

trait
Atomic extends Expression
Atomic expressions that do not have any proper subexpressions.

trait
AtomicDifferentialProgram extends AtomicProgram with DifferentialProgram
Atomic differential programs that have no subdifferentialequations (but may still have subterms)

trait
AtomicFormula extends Formula with Atomic
Atomic formulas that have no subformulas (but may still have subterms).

case class
AtomicODE(xp: DifferentialSymbol, e: Term) extends AtomicDifferentialProgram with Product with Serializable
x'=e atomic differential equation where x is evolving for some time with timederivative e.

trait
AtomicProgram extends Program with Atomic
Atomic programs that have no subprograms (but may still have subterms or subformulas).

trait
AtomicTerm extends Term with Atomic
Atomic terms that have no proper subterms.

case class
BaseVariable(name: String, index: Option[Int] = None, sort: Sort = Real) extends Variable with Product with Serializable
Elementary variable called
name
with an index of a fixed sort (that is not a differential variable). 
trait
BinaryComposite extends Composite
Binary composite expressions that are composed of two subexpressions.

trait
BinaryCompositeFormula extends BinaryComposite with CompositeFormula
Binary Composite Formulas, i.e.
Binary Composite Formulas, i.e. formulas composed of two subformulas.

trait
BinaryCompositeProgram extends BinaryComposite with CompositeProgram
Binary Composite Programs, i.e.
Binary Composite Programs, i.e. programs composed of two subprograms.

trait
BinaryCompositeTerm extends BinaryComposite with CompositeTerm
Binary Composite Terms, i.e.
Binary Composite Terms, i.e. terms composed of two subterms.

final
case class
BoundRenaming(what: Variable, repl: Variable, pos: SeqPos) extends PositionRule with Product with Serializable
Performs bound renaming renaming all occurrences of variable what (and its associated DifferentialSymbol) to repl.
Performs bound renaming renaming all occurrences of variable what (and its associated DifferentialSymbol) to repl. Proper bound renaming requires the replacement to be a fresh variable that does not occur previously.
G  [repl:=e]r(P), D  BR (where what',repl,repl' do not occur in P) G  [what:=e]P, D
where
r(P)
is the result of uniformly renamingwhat
to the (fresh)repl
inP
. The proof rule works accordingly for diamond modalities, nondeterministic assignments, or quantifiers, or in the antecedent.G  <repl:=e>r(P), D  BR (where what',repl,repl' do not occur in P) G  <what:=e>P, D
G  \forall repl r(P), D  BR (where what',repl,repl' do not occur in P) G  \forall what P, D
G  \exists repl r(P), D  BR (where what',repl,repl' do not occur in P) G  \exists what P, D
G, [repl:=e]r(P)  D  BR (where what',repl,repl' do not occur in P) G, [what:=e]P  D
 what
What variable (and its associated DifferentialSymbol) to replace.
 repl
The target variable to replace what with.
 pos
The position at which to perform a bound renaming.
 Note
soundnesscritical: For bound renaming purposes semantic renaming would be unsound.
 See also

case class
Box(program: Program, child: Formula) extends Modal with Product with Serializable
box modality all runs of program satisfy child: [program]child.

case class
Choice(left: Program, right: Program) extends BinaryCompositeProgram with Product with Serializable
left++right nondeterministic choice running either left or right.

case class
Close(assume: AntePos, pos: SuccPos) extends Rule with Product with Serializable
Close / Identity rule proving an assumption available in the antecedent.
Close / Identity rule proving an assumption available in the antecedent.
*  (Id) p, G  p, D

case class
CloseFalse(pos: AntePos) extends LeftRule with Product with Serializable
Close by false among the antecedent assumptions.
Close by false among the antecedent assumptions.
*  (close false) false, G  D

case class
CloseTrue(pos: SuccPos) extends RightRule with Product with Serializable
Close by true among the succedent desiderata.
Close by true among the succedent desiderata.
*  (close true) G  true, D

case class
CoHide2(pos1: AntePos, pos2: SuccPos) extends Rule with Product with Serializable
CoHide2 hides all but the two indicated positions.
CoHide2 hides all but the two indicated positions.
p  q  (CoHide2) p, G  q, D

case class
CoHideLeft(pos: AntePos) extends LeftRule with Product with Serializable
CoHide left.
CoHide left.
p   (CoHide left) p, G  D
 Note
Rarely useful (except for contradictory
,p
)Not used, just contained for symmetry reasons

case class
CoHideRight(pos: SuccPos) extends RightRule with Product with Serializable
CoHide right.
CoHide right.
 p  (CoHide right) G  p, D

case class
CommuteEquivLeft(pos: AntePos) extends LeftRule with Product with Serializable
Commute equivalence left
Commute equivalence left
q<>p, G  D  (<>cL) p<>q, G  D
 Note
Not used, just contained for symmetry reasons

case class
CommuteEquivRight(pos: SuccPos) extends RightRule with Product with Serializable
Commute equivalence right
Commute equivalence right
G  q<>p, D  (<>cR) G  p<>q, D

trait
ComparisonFormula extends AtomicFormula with BinaryComposite
Atomic comparison formula composed of two terms.

case class
Compose(left: Program, right: Program) extends BinaryCompositeProgram with Product with Serializable
left;right sequential composition running right after left.

trait
Composite extends Expression
Composite expressions that are composed of subexpressions

trait
CompositeFormula extends Formula with Composite
Composite formulas composed of subformulas.

trait
CompositeProgram extends Program with Composite
Composite programs that are composed of subprograms.

trait
CompositeTerm extends Term with Composite
Composite terms that are composed of subterms.

class
CoreException extends ProverException
Reasoning exceptions directly from the KeYmaera X Prover Kernel.
Reasoning exceptions directly from the KeYmaera X Prover Kernel. The most important distinction of prover kernel exceptions are CriticalCoreException for unsound logical mistakes versus NoncriticalCoreException for plausible but inappropriate reasoning attempts.

class
CriticalCoreException extends CoreException
Critical reasoning exceptions directly from the KeYmaera X Prover Core that indicate a proof step was attempted that would be unsound, and was consequently denied.

case class
Cut(c: Formula) extends Rule with Product with Serializable
Cut in the given formula
c
to usec
on the first branch and provingc
on the second branch.Cut in the given formula
c
to usec
on the first branch and provingc
on the second branch.G, c  D G  D, c  (cut) G  D
The ordering of premises is optimistic, i.e., the premise using the cutin formula
c
comes before the one provingc
. Note
c will be added at the end on the subgoals

case class
CutLeft(c: Formula, pos: AntePos) extends Rule with Product with Serializable
Cut in the given formula c in place of p on the left.
Cut in the given formula c in place of p on the left.
c, G  D G  D, p>c  (Cut Left) p, G  D
Forward Hilbert style rules can move further away, implicationally, from the sequent implication. Backwards tableaux style sequent rules can move closer, implicationally, toward the sequent implication.
 Note
this would perhaps surprising that inconsistent posititioning within this rule, unlike in ImplyLeft?

case class
CutRight(c: Formula, pos: SuccPos) extends Rule with Product with Serializable
Cut in the given formula c in place of p on the right.
Cut in the given formula c in place of p on the right.
G  c, D G  c>p, D  (Cut right) G  p, D
Forward Hilbert style rules can move further away, implicationally, from the sequent implication. Backwards tableaux style sequent rules can move closer, implicationally, toward the sequent implication.

case class
Diamond(program: Program, child: Formula) extends Modal with Product with Serializable
diamond modality some run of program satisfies child: ⟨program⟩child.

case class
Differential(child: Term) extends RUnaryCompositeTerm with Product with Serializable
(child)' differential of the term
child
.(child)' differential of the term
child
. See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.

case class
DifferentialFormula(child: Formula) extends UnaryCompositeFormula with Product with Serializable
Differential formula are differentials of formulas in analogy to differential terms (child)'.
Differential formula are differentials of formulas in analogy to differential terms (child)'. In theory they are only used in the form (e>=k)' which is (e)'>=(k)'. In practice, derived forms are useful.

final
class
DifferentialProduct extends DifferentialProgram with BinaryComposite
left,right parallel product of differential programs.
left,right parallel product of differential programs. This data structure automatically leftreassociates to list form so that
left
never is a Differential Product. DifferentialProduct(AtomicDifferentialProgram, DifferentialProduct(AtomicDifferentialProgram, ....)) Note
This is a case class except for an override of the apply function to ensure leftassociative representation.
,Private constructor so only DifferentialProduct.apply can ever create this, which will reassociate et al.

sealed
trait
DifferentialProgram extends Program
Differential programs of differential dynamic logic.
Differential programs of differential dynamic logic.
Differential Programs are of the form
 AtomicDifferentialProgram atomic differential programs are not composed of other differential programs
x'=e
atomic differential equation as AtomicODE(DifferentialSymbol,Term)c
differential program constant as DifferentialProgramConst
 BinaryCompositeDifferentialProgram except it's the only composition for differential programs.
c,d
differential product as DifferentialProduct(DifferentialProgram], DifferentialProgram])
 AtomicDifferentialProgram atomic differential programs are not composed of other differential programs

case class
DifferentialProgramConst(name: String, space: Space = AnyArg) extends AtomicDifferentialProgram with SpaceDependent with NamedSymbol with Product with Serializable
Uninterpreted differential program constant, limited to the given state space.
Uninterpreted differential program constant, limited to the given state space. The semantics of arity 0 DifferentialProgramConst symbol is looked up by the state, with the additional promise that taboos are neither free nor bound, so the run does not depend on the value of taboos nor does the value of taboos change when space=Except(taboos).
 space
The part of the state space that the interpretation/replacement of this symbol is limited to have free or bound.
AnyArg is
the default allowing full read/write access to the state.Taboo(x)
meansx
can neither be free nor bound.

case class
DifferentialSymbol(x: Variable) extends Variable with RTerm with Product with Serializable
Differential symbol x' for variable x.
Differential symbol x' for variable x. Differential symbols are also called differential variables, because they are symbolic but are also variables.

case class
Divide(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable
/ real division of reals where
right
nonzero. 
case class
DotTerm(s: Sort = Real, idx: Option[Int] = None) extends Expression with NamedSymbol with AtomicTerm with Product with Serializable
•: Placeholder for terms in uniform substitutions of given sort.
•: Placeholder for terms in uniform substitutions of given sort. Reserved nullary function symbols \\cdot for uniform substitutions are unlike ordinary function symbols by convention.

case class
Dual(child: Program) extends UnaryCompositeProgram with Product with Serializable
child^d
dual program continuing game child after passing control to the opponent.

implicit final
class
Ensures[A] extends AnyVal
Contracts (like scala.Predef.Ensuring) implemented with Javastyle assertions (see assertion)

case class
Equal(left: Term, right: Term) extends ComparisonFormula with Product with Serializable
equality left = right.=

case class
Equiv(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable
<> logical biimplication: equivalent.

case class
EquivLeft(pos: AntePos) extends LeftRule with Product with Serializable
<>L Equiv left.
<>L Equiv left.
p&q, G  D !p&!q, G  D  (<> Equiv left) p<>q, G  D
 Note
Positions remain stable when decomposed this way around.

case class
EquivRight(pos: SuccPos) extends RightRule with Product with Serializable
<>R Equiv right.
<>R Equiv right.
G, p  D, q G, q  D, p  (<>R Equiv right) G  p<>q, D

case class
EquivifyRight(pos: SuccPos) extends RightRule with Product with Serializable
Equivify Right: Convert implication to equivalence.
Equivify Right: Convert implication to equivalence.
G  a<>b, D  G  a>b, D

case class
Except(taboos: Seq[Variable]) extends Space with Product with Serializable
The sort denoting a slice of the state space that does not include/depend on/affect variables
taboos
. 
case class
ExchangeLeftRule(pos1: AntePos, pos2: AntePos) extends Rule with Product with Serializable
Exchange left rule reorders antecedent.
Exchange left rule reorders antecedent.
q, p, G  D  (Exchange left) p, q, G  D

case class
ExchangeRightRule(pos1: SuccPos, pos2: SuccPos) extends Rule with Product with Serializable
Exchange right rule reorders succedent.
Exchange right rule reorders succedent.
G  q, p, D  (Exchange right) G  p, q, D

case class
Exists(vars: Seq[Variable], child: Formula) extends Quantified with Product with Serializable
\exists vars existentially quantified formula for some real value of vars.

sealed
trait
Expression extends AnyRef
Expressions of differential dynamic logic.
Expressions of differential dynamic logic. Expressions are categorized according to the syntactic categories of the grammar of differential dynamic logic:
1. terms are of type edu.cmu.cs.ls.keymaerax.core.Term of kind edu.cmu.cs.ls.keymaerax.core.TermKind 2. formulas are of type edu.cmu.cs.ls.keymaerax.core.Formula of kind edu.cmu.cs.ls.keymaerax.core.FormulaKind 3. hybrid programs are of type edu.cmu.cs.ls.keymaerax.core.Program of kind edu.cmu.cs.ls.keymaerax.core.ProgramKind 4. differential programs are of type edu.cmu.cs.ls.keymaerax.core.DifferentialProgram of kind edu.cmu.cs.ls.keymaerax.core.DifferentialProgramKind 5. function symbols are degenerate expressions that are syntactically incomplete, since not yet applied to arguments via FuncOf to form a term or via PredOf or PredicationalOf to form a formula.
See Section 2.1
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.

case class
Forall(vars: Seq[Variable], child: Formula) extends Quantified with Product with Serializable
\forall vars universally quantified formula for all real values of vars.

sealed
trait
Formula extends Expression
Formulas of differential dynamic logic.
Formulas of differential dynamic logic. Also includes formulas of differential game logic, which only differ in the permitted mention of Dual.
Formulas are of the form
 AtomicFormula atomic formulas that are not composed of other formulas
true
truth as True andfalse
as FalseP
nullary predicational as UnitPredicational writtenP()
in internal syntax._
dot as reserved nullary predicational DotFormula for formula argument placeholders
 ComparisonFormula are AtomicFormula composed of two terms but not composed of formulas
 ApplicationOf predicate applications
 UnaryCompositeFormula unary composite formulas composed of one child formula
!P
logical negation as Not(Formula)(P)'
differential formula as DifferentialFormula(Formula])
 BinaryCompositeFormula binary composite formulas composed of a left and a right formula
 Quantified quantified formulas quantifying a variable
 Modal modal formulas with a program and a formula child
 AtomicFormula atomic formulas that are not composed of other formulas

case class
FuncOf(func: Function, child: Term) extends CompositeTerm with ApplicationOf with Product with Serializable
Function symbol applied to argument child
func(child)
. 
case class
Function(name: String, index: Option[Int] = None, domain: Sort, sort: Sort, interp: Option[Formula] = None) extends NamedSymbol with Product with Serializable
Function symbol or predicate symbol or predicational symbol
name_index:domain>sort
Function symbol or predicate symbol or predicational symbol
name_index:domain>sort
 domain
the sort of expected arguments.
 sort
the sort resulting when this function/predicate/predicational symbol has been applied to an argument.
 interp
if present, this function symbol
f
has a fixed interpretation defined byy = f(x) <> P(y,x)
where P is the interp formula, substituting (y,x) for the dot terms. That is
._0 = f(._1) <> P(._0,._1)

case class
Greater(left: Term, right: Term) extends RComparisonFormula with Product with Serializable
> greater than comparison left > right of reals.

case class
GreaterEqual(left: Term, right: Term) extends RComparisonFormula with Product with Serializable
>= greater or equal comparison left >= right of reals.

case class
HideLeft(pos: AntePos) extends LeftRule with Product with Serializable
Hide left.
Hide left.
G  D  (Weaken left) p, G  D

case class
HideRight(pos: SuccPos) extends RightRule with Product with Serializable
Hide right.
Hide right.
G  D  (Weaken right) G  p, D

case class
Imply(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable
> logical implication: implies.

case class
ImplyLeft(pos: AntePos) extends LeftRule with Product with Serializable
>L Imply left.
>L Imply left.
G  D, p q, G  D  (> Imply left) p>q, G  D

case class
ImplyRight(pos: SuccPos) extends RightRule with Product with Serializable
>R Imply right.
>R Imply right.
G, p  D, q  (>R Imply right) G  p>q, D

case class
InapplicableRuleException(msg: String, r: Rule, s: Sequent = null) extends NoncriticalCoreException with Product with Serializable
Rule is not applicable as indicated.
Rule is not applicable as indicated. For example, InapplicableRuleException can be raised when trying to apply AndRight at the correct position 2 in bounds on the righthand side where it turns out there is an Or formula not an And formula. For readability and code performance reasons, the prover kernel may also raise scala.MatchError if the shape of a formula is not as expected, but core tactics will then convert MatchError to InapplicableRuleException.

sealed
trait
Kind extends AnyRef
Kinds of expressions (term, formula, program, differential program).
Kinds of expressions (term, formula, program, differential program).
 See also

trait
LeftRule extends PositionRule
A rule applied to a position in the antecedent on the left of a sequent.
A rule applied to a position in the antecedent on the left of a sequent. LeftRules can only be applied to antecedent positions.
 See also

case class
Less(left: Term, right: Term) extends RComparisonFormula with Product with Serializable
<= less than comparison left < right of reals.

case class
LessEqual(left: Term, right: Term) extends RComparisonFormula with Product with Serializable
< less or equal comparison left <= right of reals.

case class
Loop(child: Program) extends UnaryCompositeProgram with Product with Serializable
child* nondeterministic repetition running child arbitrarily often.

case class
Minus(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable
 binary subtraction of reals.

trait
Modal extends CompositeFormula
Modal formulas.

trait
NamedSymbol extends Expression with Ordered[NamedSymbol]
A named symbol such as a variable or function symbol or predicate symbol or program constant symbol.
A named symbol such as a variable or function symbol or predicate symbol or program constant symbol.
 Note
Userlevel symbols should not use underscores, which are reserved for the core.

case class
Neg(child: Term) extends RUnaryCompositeTerm with Product with Serializable
 unary negation of reals: minus.

class
NoncriticalCoreException extends CoreException
Noncritical reasoning exceptions directly from the KeYmaera X Prover Core that indicate a proof step was perfectly plausible to try, just did not fit the expected pattern, and consequently turned out impossible.

case class
Not(child: Formula) extends UnaryCompositeFormula with Product with Serializable
! logical negation: not.

case class
NotEqual(left: Term, right: Term) extends ComparisonFormula with Product with Serializable
!= disequality left != right.

case class
NotLeft(pos: AntePos) extends LeftRule with Product with Serializable
!L Not left.
!L Not left.
G  D, p  (!L Not left) !p, G  D

case class
NotRight(pos: SuccPos) extends RightRule with Product with Serializable
!R Not right.
!R Not right.
G, p  D  (!R Not right) G  !p, D

case class
Number(value: BigDecimal) extends AtomicTerm with RTerm with Product with Serializable
Number literal such as 0.5 or 42 etc.

case class
ODESystem(ode: DifferentialProgram, constraint: Formula = True) extends Program with Product with Serializable
Differential equation system
ode
with given evolution domain constraint. 
case class
ObjectSort(name: String) extends Sort with Product with Serializable
Userdefined object sort.

case class
Or(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable
 logical disjunction: or.

case class
OrLeft(pos: AntePos) extends LeftRule with Product with Serializable
L Or left.
L Or left.
p, G  D q, G  D  (L Or left) pq, G  D

case class
OrRight(pos: SuccPos) extends RightRule with Product with Serializable
R Or right.
R Or right.
G  D, p,q  (R Or right) G  pq, D

case class
Pair(left: Term, right: Term) extends BinaryCompositeTerm with Product with Serializable
Pairs (left,right) for binary Function and FuncOf and PredOf.
Pairs (left,right) for binary Function and FuncOf and PredOf.
 Note
By convention, pairs are usually used in rightassociative ways. That is, nary argument terms (t1,t2,t3,...tn) are represented as (t1,(t2,(t3,...tn))). This is not a strict requirement, but the default parse and suggested use.

case class
Plus(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable
+ binary addition of reals.

trait
PositionRule extends Rule
A rule applied to a position in a sequent.
A rule applied to a position in a sequent.
 See also

case class
Power(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable
real exponentiation or power: left^{right}.
real exponentiation or power: left^{right}.
 Note
By mathematical conventions, powers are parsed in rightassociative ways. That is, x^{4}2 is parsed as x^{(4}2).

case class
PredOf(func: Function, child: Term) extends AtomicFormula with ApplicationOf with Product with Serializable
Predicate symbol applied to argument child
func(child)
wherefunc
is Booleanvalued . 
case class
PredicationalOf(func: Function, child: Formula) extends AtomicFormula with ApplicationOf with StateDependent with Product with Serializable
Predicational or quantifier symbol applied to argument formula child, written
C{child}
.Predicational or quantifier symbol applied to argument formula child, written
C{child}
. Predicationals are similar to predicate symbol applications, except that they accept a formula as an argument rather than a term. Also, their truthvalue may depend on the entire truth table ofchild
at any state. Note
In theory,
C{child}
is writtenC(child)
.

sealed
trait
Program extends Expression
Hybrid programs of differential dynamic logic.
Hybrid programs of differential dynamic logic. Also includes hybrid games of differential game logic, which only differ in the permitted mention of Dual.
Hybrid Programs are of the form
 AtomicProgram atomic programs that are not composed of other programs
x:=e
assignment as Assign(Variable,Term) and likewise differential assignmentx':=e
as Assign(DifferentialSymbol,Term)x:=*
nondeterministic assignment as AssignAny(Variable) and likewise nondeterministic differential assignmentx':=*
as AssignAny(DifferentialSymbol)a
program constant as ProgramConst writtena{^x}
if x taboo.
a
system constant as SystemConst without games, writtena{^@}
in internal syntax.
?P
test as Test(Formula)
 BinaryCompositeProgram binary composite programs composed of a left and right program
 UnaryCompositeProgram unary composite programs composed of a child program
 Special
{c&Q}
differential equation system as ODESystem(DifferentialProgram, Formula)
 AtomicProgram atomic programs that are not composed of other programs

case class
ProgramConst(name: String, space: Space = AnyArg) extends NamedSymbol with AtomicProgram with SpaceDependent with Product with Serializable
Uninterpreted program constant symbol / game symbol, possibly limited to the given state space.
Uninterpreted program constant symbol / game symbol, possibly limited to the given state space. The semantics of ProgramConst symbol is looked up by the state, with the additional promise that taboos are neither free nor bound, so the run does not depend on the value of taboos nor does the value of taboos change when space=Except(taboos).
 space
The part of the state space that the interpretation/replacement of this symbol is limited to have free or bound.
AnyArg
is the default allowing full read/write access to the state.Taboo(x)
meansx
can neither be free nor bound. Writtena{x}
in internal syntax.
 Note
In theory,
a;
is writtena
. By analogy,a{x}
has read/write access to the entire state except the taboo x.

final
case class
Provable extends Product with Serializable
Provable(conclusion, subgoals) is the proof certificate representing certified provability of
conclusion
from the premises insubgoals
.Provable(conclusion, subgoals) is the proof certificate representing certified provability of
conclusion
from the premises insubgoals
. Ifsubgoals
is an empty list, thenconclusion
is provable. Otherwiseconclusion
is provable from the set of all assumptions insubgoals
.G1  D1 ... Gn  Dn (subgoals)  G  D (conclusion)
Invariant: All Provables ever produced are locally sound, because only the prover kernel can create Provable objects and chooses not to use the globally sound uniform substitution rule.
Provables are stateless and do not themselves remember other provables that they resulted from. The ProofTree data structure outside the kernel provides such proof tree navigation information.
Proofs can be constructed in (backward/tableaux) sequent order using Provables:
import scala.collection.immutable._ val verum = new Sequent(IndexedSeq(), IndexedSeq(True)) // conjecture val provable = Provable.startProof(verum) // construct a proof val proof = provable(CloseTrue(SuccPos(0)), 0) // check if proof successful if (proof.isProved) println("Successfully proved " + proof.proved)
, Multiple Provable objects for subderivations obtained from different sources can also be merged
// ... continuing other example val more = new Sequent(IndexedSeq(), IndexedSeq(Imply(Greater(Variable("x"), Number(5)), True))) // another conjecture val moreProvable = Provable.startProof(more) // construct another (partial) proof val moreProof = moreProvable(ImplyRight(SuccPos(0)), 0)(HideLeft(AntePos(0)), 0) // merge proofs by gluing their Provables together val mergedProof = moreProof(proof, 0) // check if proof successful if (mergedProof.isProved) println("Successfully proved " + mergedProof.proved)
, Proofs in backward tableaux sequent order are straightforward
import scala.collection.immutable._ val fm = Greater(Variable("x"), Number(5)) //  x>5 > x>5 & true val finGoal = new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True)))) // conjecture val finProvable = Provable.startProof(finGoal) // construct a proof val proof = finProvable( ImplyRight(SuccPos(0)), 0)( AndRight(SuccPos(0)), 0)( HideLeft(AntePos(0)), 1)( CloseTrue(SuccPos(0)), 1)( Close(AntePos(0), SuccPos(0)), 0) // proof of finGoal println(proof.proved)
, Proofs in forward Hilbert order are straightforward with merging of branches
import scala.collection.immutable._ val fm = Greater(Variable("x"), Number(5)) // proof of x>5  x>5 & true merges left and right branch by AndRight val proof = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(And(fm, True))))( AndRight(SuccPos(0)), 0) ( // left branch: x>5  x>5 Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(fm)))( Close(AntePos(0), SuccPos(0)), 0), 0) ( //right branch:  true Provable.startProof(Sequent(IndexedSeq(), IndexedSeq(True)))( CloseTrue(SuccPos(0)), 0)( // x>5  true Sequent(IndexedSeq(fm), IndexedSeq(True)), HideLeft(AntePos(0))), 0) ( //  x>5 > x>5 & true new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True)))), ImplyRight(SuccPos(0)) ) // proof of finGoal:  x>5 > x>5 & true println(proof.proved)
, Proofs in Hilbertcalculus style order can also be based exclusively on subsequent merging
import scala.collection.immutable._ val fm = Greater(Variable("x"), Number(5)) // x>0  x>0 val left = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(fm)))( Close(AntePos(0), SuccPos(0)), 0) //  true val right = Provable.startProof(Sequent(IndexedSeq(), IndexedSeq(True)))( CloseTrue(SuccPos(0)), 0) val right2 = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(True)))( HideLeft(AntePos(0)), 0) (right, 0) // gluing order for subgoals is irrelevant. Could use: (right2, 1)(left, 0)) val merged = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(And(fm, True))))( AndRight(SuccPos(0)), 0) ( left, 0)( right2, 0) //  x>5 > x>5 & true val finGoal = new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True)))) val proof = Provable.startProof(finGoal)( ImplyRight(SuccPos(0)), 0) (merged, 0) // proof of finGoal println(proof.proved)
, Branching proofs in backward tableaux sequent order are straightforward, yet might become more readable when closing branches righttoleft to keep explicit subgoals:
// explicit proof certificate construction of  !!p() <> p() val proof = (Provable.startProof( "!!p() <> p()".asFormula) (EquivRight(SuccPos(0)), 0) // right branch (NotRight(SuccPos(0)), 1) (NotLeft(AntePos(1)), 1) (Close(AntePos(0),SuccPos(0)), 1) // left branch (NotLeft(AntePos(0)), 0) (NotRight(SuccPos(1)), 0) (Close(AntePos(0),SuccPos(0)), 0) )
 Note
soundnesscritical logical framework.
,Only private constructor calls for soundness
,For soundness: No reflection should bypass constructor call privacy, nor reflection to bypass immutable val algebraic data types.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Examples: 
class
ProvableStorageException extends CoreException
Exception indicating that a Provable Storage representation as a String cannot be read, because it has been tampered with.
Exception indicating that a Provable Storage representation as a String cannot be read, because it has been tampered with.
 See also

case class
ProverAssertionError(msg: String) extends ProverException with Product with Serializable
Internal core assertions that fail in the prover

class
ProverException extends RuntimeException
KeYmaera X Prover Exceptions.

trait
QETool extends AnyRef
Interface to quantifier elimination tools.

trait
Quantified extends CompositeFormula
Quantified formulas.

case class
RenamingClashException(msg: String, ren: String, e: String, info: String = "") extends CriticalCoreException with Product with Serializable
Uniform or bound renaming clashes are unsound renaming reasoning attempts.
Uniform or bound renaming clashes are unsound renaming reasoning attempts.

trait
RightRule extends PositionRule
A rule applied to a position in the succedent on the right of a sequent.
A rule applied to a position in the succedent on the right of a sequent. RightRules can only be applied to succedent positions.
 See also

sealed
trait
Rule extends (Sequent) ⇒ List[Sequent]
Subclasses represent all builtin proof rules.
Subclasses represent all builtin proof rules. A proof rule is ultimately a named mapping from sequents to lists of sequents. The resulting list of sequents represent the subgoals/premises all of which need to be proved to prove the current sequent (desired conclusion).
 Note
soundnesscritical This class is sealed, so no rules can be added outside Proof.scala
 See also

sealed
trait
SeqPos extends AnyRef
Position of a formula in a sequent, i.e.
Position of a formula in a sequent, i.e. antecedent or succedent positions.

final
case class
Sequent(ante: IndexedSeq[Formula], succ: IndexedSeq[Formula]) extends Product with Serializable
Sequent
ante  succ
with antecedent ante and succedent succ.Sequent
ante  succ
with antecedent ante and succedent succ.ante(0),ante(1),...,ante(n)  succ(0),succ(1),...,succ(m)
This sequent is often prettyprinted with signed line numbers:
1: ante(0) 2: ante(1) ... (n+1): ante(n) ==> 1: succ(0) 2: succ(1) ... (m+1): succ(m)
The semantics of sequent
ante  succ
is the conjunction of the formulas inante
implying the disjunction of the formulas insucc
. ante
The ordered list of antecedents of this sequent whose conjunction is assumed.
 succ
The orderd list of succedents of this sequent whose disjunction needs to be shown.
 See also
Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143189, 2008.

sealed
trait
SetLattice[A] extends AnyRef
Lattice of sets, i.e.
Lattice of sets, i.e. the lattice of sets that also includes bottom, top and neartop elements.
 A
Type of elements in the set

case class
SkolemClashException(msg: String, clashedNames: SetLattice[Variable], vars: String, s: String) extends CriticalCoreException with Product with Serializable
Skolem symbol clashes are unsound Skolemization reasoning attempts.
Skolem symbol clashes are unsound Skolemization reasoning attempts.
 See also

case class
Skolemize(pos: SeqPos) extends PositionRule with Product with Serializable
Skolemization assumes that the names of the quantified variables to be skolemized are unique within the sequent.
Skolemization assumes that the names of the quantified variables to be skolemized are unique within the sequent. This can be ensured by finding a unique name and renaming the bound variable through alpha conversion.
G  p(x), D  (Skolemize) provided x not in G,D G  \forall x p(x), D
Skolemization also handles existential quantifiers on the left:
p(x), G  D  (Skolemize) provided x not in G,D \exists x p(x), G  D
 Note
Could in principle replace by uniform substitution rule application mechanism for rule "all generalization" along with tactics expanding scope of quantifier with axiom "all quantifier scope" at the cost of propositional repacking and unpacking. p(x) all generalize \forall x. p(x) Kept because of the incurred cost.
 See also
SkolemClashException

sealed
trait
Sort extends AnyRef
Sorts of expressions (real, bool, etc).
Sorts of expressions (real, bool, etc).
 See also

sealed
trait
Space extends AnyRef
Sorts of state spaces for statedependent operators.
Sorts of state spaces for statedependent operators.
 See also

trait
SpaceDependent extends StateDependent
Expressions limited to a given sub statespace of only some variables and differential variables.
Expressions limited to a given sub statespace of only some variables and differential variables.
 Since
4.2

trait
StateDependent extends Expression
Expressions whose semantic interpretations have access to the state.
Expressions whose semantic interpretations have access to the state.
 Note
Not soundnesscritical, merely speeds up matching in SubstitutionPair.freeVars.

case class
SubderivationSubstitutionException(subderivation: String, conclusion: String, subgoal: String, subgoalid: Int, provable: String) extends CriticalCoreException with Product with Serializable
Exceptions that arise from trying to substitute a subderivation in for a subgoal that does not equal the conclusion of the subderivation.
Exceptions that arise from trying to substitute a subderivation in for a subgoal that does not equal the conclusion of the subderivation.
 See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(rule:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable,subgoal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable\.Subgoal):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

case class
SubstitutionClashException(subst: String, U: String, e: String, context: String, clashes: String, info: String = "") extends CriticalCoreException with Product with Serializable
Substitution clashes are raised for unsound substitution reasoning attempts.
Substitution clashes are raised for unsound substitution reasoning attempts.
 See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubstChurch):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

final
case class
SubstitutionPair(what: Expression, repl: Expression) extends Product with Serializable
Representation of a substitution replacing
what
withrepl
uniformly, everywhere.Representation of a substitution replacing
what
withrepl
uniformly, everywhere. Data structure invariant: Only substitutable expressions will be accepted forwhat
with compatiblerepl
. what
the expression to be replaced.
what
can have one of the following forms: PredOf(p:Function, DotTerm/Nothing/Nested Pair of DotTerm)
 FuncOf(f:Function, DotTerm/Nothing/Nested Pair of DotTerm)
 ProgramConst or DifferentialProgramConst or SystemConst
 UnitPredicational
 UnitFunctional
 PredicationalOf(p:Function, DotFormula)
 DotTerm
 DotFormula
 repl
the expression to be used in place of
what
.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425441. Springer, 2019.

case class
SuccPos extends SeqPos with Product with Serializable
Antecedent Positions of formulas in a sequent, i.e.
Antecedent Positions of formulas in a sequent, i.e. on the right of the sequent arrow.

case class
SystemConst(name: String, space: Space = AnyArg) extends NamedSymbol with AtomicProgram with SpaceDependent with Product with Serializable
Uninterpreted hybrid system program constant symbols that are NOT hybrid games, limited to the given state space.
Uninterpreted hybrid system program constant symbols that are NOT hybrid games, limited to the given state space. Written
a{^@}
in internal syntax.
 space
The part of the state space that the interpretation/replacement of this symbol is limited to have free or bound.
AnyArg
is the default allowing full read/write access to the state.Taboo(x)
meansx
can neither be free nor bound. Writtena{^@x}
in internal syntax.
 Since
4.7.4 also SpaceDependent with
space
parameter.

sealed
trait
Term extends Expression
Terms of differential dynamic logic.
Terms of differential dynamic logic. Also terms of differential game logic, which only differ in the permitted mention of Dual.
Terms are of the form
 AtomicTerm atomic terms are not composed of other terms
x
variable as Variable, including differential symbolx'
as DifferentialSymbol5
number literals as NumberF
nullary functional as UnitFunctional writtenF()
in internal syntax..
dot as reserved nullary function symbol DotTerm for term argument placeholders Nothing for empty arguments Nothing for nullary functions
 ApplicationOf terms that are function applications
 UnaryCompositeTerm unary composite terms composed of one child term
e
negation as Neg(Term)(e)'
differential as Differential(Term)
 BinaryCompositeTerm binary composite terms composed of two children terms
 AtomicTerm atomic terms are not composed of other terms

case class
Test(cond: Formula) extends AtomicProgram with Product with Serializable
?cond test a formula as a condition on the current state.

case class
Times(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable
* binary multiplication of reals.

case class
Tuple(left: Sort, right: Sort) extends Sort with Product with Serializable
Tuple sort for Pair.

final
case class
URename(what: Variable, repl: Variable, semantic: Boolean = false) extends (Expression) ⇒ Expression with Product with Serializable
Uniformly rename all occurrences of
what
andwhat'
torepl
andrepl'
and vice versa, but clash for program constants etc.Uniformly rename all occurrences of
what
andwhat'
torepl
andrepl'
and vice versa, but clash for program constants etc. Uniformly rename all occurrences of variablewhat
(and its associated DifferentialSymbolwhat'
) torepl
(and its associated DifferentialSymbolrepl'
) everywhere and vice versa uniformly rename all occurrences of variablerepl
(and its associated DifferentialSymbol) towhat
(andwhat'
). Uniform renaming, thus, is a transposition. what
What variable to replace (along with its associated DifferentialSymbol).
 repl
The target variable to replace
what
with and vice versa. semantic
true
to allow semantic renaming of SpaceDependent symbols, which preserves local soundness when applied to inferences.

type
USubst = USubstOne
The uniform substitution type to use

final
case class
USubstOne(subsDefsInput: Seq[SubstitutionPair]) extends (Expression) ⇒ Expression with Product with Serializable
A Uniform Substitution with its onepass application mechanism.
A Uniform Substitution with its onepass application mechanism. A Uniform Substitution uniformly replaces all occurrences of a given predicate p(.) by a formula in (.). It can also replace all occurrences of a function symbol f(.) by a term in (.) and all occurrences of a predicational / quantifier symbols C() by a formula in () and all occurrences of program constant symbol b by a hybrid program.
This type implements the application of uniform substitutions to terms, formulas, programs, and sequents.
 Since
4.7
 Note
Implements the onepass version that checks admissibility on the fly and checking upon occurrence. Faster than the alternative USubstChurch. Main ingredient of prover core.
,soundnesscritical
 See also
Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425441. Springer, 2019.
edu.cmu.cs.ls.keymaerax.core.Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubstOne):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

trait
UnaryComposite extends Composite
Unary composite expressions that are composed of one subexpression.

trait
UnaryCompositeFormula extends UnaryComposite with CompositeFormula
Unary Composite Formulas, i.e.
Unary Composite Formulas, i.e. formulas composed of one subformula.

trait
UnaryCompositeProgram extends UnaryComposite with CompositeProgram
Unary Composite Programs, i.e.
Unary Composite Programs, i.e. programs composed of one subprogram.

trait
UnaryCompositeTerm extends UnaryComposite with CompositeTerm
Unary Composite Terms, i.e.
Unary Composite Terms, i.e. terms composed of one real subterm.

final
case class
UniformRenaming(what: Variable, repl: Variable) extends Rule with Product with Serializable
Uniformly rename all occurrences of what and what' to repl and repl' and vice versa.
Uniformly rename all occurrences of what and what' to repl and repl' and vice versa. Uniformly rename all occurrences of variable what (and its associated DifferentialSymbol) to repl. Uniform renaming, thus, is a transposition.
r(G)  r(D)  UR G  D
 what
What variable to replace (along with its associated DifferentialSymbol).
 repl
The target variable to replace
what
with (and vice versa).
 Note
soundnesscritical: For uniform renaming purposes the semantic renaming proof rule would be sound but not locally sound. The kernel is easier when keeping everything locally sound.
 See also

case class
UnitFunctional(name: String, space: Space, sort: Sort) extends AtomicTerm with SpaceDependent with NamedSymbol with Product with Serializable
Arity 0 functional symbol
name:sort
, writtenf()
, or limited to the given state spacef(x)
.Arity 0 functional symbol
name:sort
, writtenf()
, or limited to the given state spacef(x)
. The semantics of arity 0 functional symbol is given by the state, with the additional promise that the taboos are not free so the value does not depend on taboos whenspace=Except(taboos)
. Note
In theory,
f()
is writtenf(\bar{x})
where\bar{x}
is the vector of all variables. By analogy,f(x)
is like having all variables other than taboo x as argument.

case class
UnitPredicational(name: String, space: Space) extends AtomicFormula with SpaceDependent with NamedSymbol with Product with Serializable
Arity 0 predicational symbol
name:bool
, writtenP()
, or limited to the given state spaceP(x)
.Arity 0 predicational symbol
name:bool
, writtenP()
, or limited to the given state spaceP(x)
. The semantics of arity 0 predicational symbol is looked up by the state, with the additional promise that taboos are not free so the value does not depend on taboos whenspace=Except(taboos)
. Note
In theory,
P()
is writtenP(\bar{x})
where\bar{x}
is the vector of all variables. By analogy,P(x)
is like having all variables other than taboo x as argument.

case class
UnknownOperatorException(msg: String, e: Expression) extends ProverException with Product with Serializable
Thrown to indicate when an unknown operator occurs

class
UnprovedException extends CoreException
Exception indicating an attempt to steal a proved sequent from a Provable that was not proved.
Exception indicating an attempt to steal a proved sequent from a Provable that was not proved.
 See also

trait
Variable extends NamedSymbol with AtomicTerm
Variables have a name and index and sort.
Variables have a name and index and sort. They are either BaseVariable or DifferentialSymbol.

final
case class
USubstChurch(subsDefsInput: Seq[SubstitutionPair]) extends (Expression) ⇒ Expression with Product with Serializable
A Uniform Substitution with its application mechanism (original version).
A Uniform Substitution with its application mechanism (original version). A Uniform Substitution uniformly replaces all occurrences of a given predicate p(.) by a formula in (.). It can also replace all occurrences of a function symbol f(.) by a term in (.) and all occurrences of a quantifier symbols C() by a formula in () and all occurrences of program constant b by a hybrid program.
This type implements the application of uniform substitutions to terms, formulas, programs, and sequents.
 Annotations
 @deprecated
 Deprecated
Use faster USubstOne instead
Uniform substitution can be applied to a formula
val p = Function("p", None, Real, Bool) val x = Variable("x", None, Real) // p(x) <> ! ! p(  x) val prem = Equiv(PredOf(p, x), Not(Not(PredOf(p, Neg(Neg(x)))))) val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm), GreaterEqual(Power(DotTerm, Number(5)), Number(0))))) // x^5>=0 <> !(!(((x))^5>=0)) println(s(prem))
, Uniform substitutions can be applied via the uniform substitution proof rule to a sequent:
val p = Function("p", None, Real, Bool) val x = Variable("x", None, Real) // p(x) <> ! ! p(  x) val prem = Equiv(PredOf(p, x), Not(Not(PredOf(p, Neg(Neg(x)))))) val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm), GreaterEqual(Power(DotTerm, Number(5)), Number(0))))) val conc = "x^5>=0 <> !(!(((x))^5>=0))".asFormula val next = UniformSubstitutionRule(s, Sequent(IndexedSeq(), IndexedSeq(prem)))( Sequent(IndexedSeq(), IndexedSeq(conc))) // results in: p(x) <> ! ! p(  x) println(next)
, Uniform substitutions also work for substituting hybrid programs
val p = Function("p", None, Real, Bool) val x = Variable("x", None, Real) val a = ProgramConst("a") // [a]p(x) <> [a](p(x)&true) val prem = Equiv(Box(a, PredOf(p, x)), Box(a, And(PredOf(p, x), True))) val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm), GreaterEqual(DotTerm, Number(2))), SubstitutionPair(a, ODESystem(AtomicODE(DifferentialSymbol(x), Number(5)), True)))) // "[x'=5;]x>=2 <> [x'=5;](x>=2&true)".asFormula println(s(prem))
, Uniform substitution rule also works when substitution hybrid programs
val p = Function("p", None, Real, Bool) val x = Variable("x", None, Real) val a = ProgramConst("a") // [a]p(x) <> [a](p(x)&true) val prem = Equiv(Box(a, PredOf(p, x)), Box(a, And(PredOf(p, x), True))) val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm), GreaterEqual(DotTerm, Number(2))), SubstitutionPair(a, ODESystem(AtomicODE(DifferentialSymbol(x), Number(5)), True)))) val conc = "[x'=5;]x>=2 <> [x'=5;](x>=2&true)".asFormula val next = UniformSubstitutionRule(s, Sequent(IndexedSeq(), IndexedSeq(prem)))( Sequent(IndexedSeq(), IndexedSeq(conc))) // results in: [x'=5;]x>=2 <> [x'=5;](x>=2&true) println(next)
 Note
Implements the "global" version that checks admissibility eagerly at bound variables rather than computing bounds on the fly and checking upon occurrence. Main ingredient of prover core.
,Superseded by faster alternative USubstOne.
,soundnesscritical
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
Andre Platzer. Uniform substitution for differential game logic. In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Automated Reasoning, 9th International Joint Conference, IJCAR 2018, volume 10900 of LNCS, pp. 211227. Springer 2018.
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
edu.cmu.cs.ls.keymaerax.core.Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubstChurch):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*
Examples:
Value Members

val
ENCODING: String
The encoding used for storing lemmas and other artifacts.

def
USubst(subsDefsInput: Seq[SubstitutionPair]): USubst
USubst factory method, forwards to constructor.

val
VERSION: String
KeYmaera X core kernel version number

def
assertion(condition: ⇒ Boolean, message: ⇒ Any): scala.Unit
see assertion
see assertion
 Annotations
 @elidable( elidable.ASSERTION ) @inline()

def
assertion(condition: ⇒ Boolean): scala.Unit
see assertion
see assertion
 Annotations
 @elidable( elidable.ASSERTION ) @inline()

def
assertion[A](condition: (A) ⇒ Boolean, argument: A): A
see assertion
see assertion
 Annotations
 @elidable( elidable.ASSERTION ) @inline()

def
assertion[A](condition: (A) ⇒ Boolean, argument: A, message: ⇒ Any): A
Javastyle assertions, disabled by default, enabled with
java ea
, disable withjava da
.Javastyle assertions, disabled by default, enabled with
java ea
, disable withjava da
. Scalastyle elidable at compiletime withXdisableassertions
Lazy evaluation of
condition
onargument
, lazy evaluation of message. Annotations
 @elidable( elidable.ASSERTION ) @inline()

final
def
insist(requirement: Boolean, message: ⇒ Any): scala.Unit
Insist on
requirement
being true, throwing a CoreException if false.Insist on
requirement
being true, throwing a CoreException if false. This method is arequire
coming from the prover core that cannot be disabled. Blame is on the caller of the method for violating the contract. requirement
the expression to test for being true
 message
a String explaining what is expected.
 Annotations
 @inline()
 See also
scala.Predef.require()

final
def
noException[T](e: ⇒ T): Boolean
Check that the given expression
e
does not throw an exception.Check that the given expression
e
does not throw an exception. returns
true
ife
completed without raising any exceptions or errors.false
ife
raised an exception or error.
 Annotations
 @inline()
insist(noExeption(complicatedComputation), "The complicated computation should complete without throwing exceptions")
Example: 
object
AnyArg extends Space with Product with Serializable
The sort denoting the whole state space alias list of all variables as arguments \bar{x} (axioms that allow any variable dependency)
 object Bool extends Sort with Product with Serializable
 object DifferentialProduct

object
DifferentialProgramKind extends Kind with Product with Serializable
All differential programs are of kind DifferentialProgramKind.
All differential programs are of kind DifferentialProgramKind.
 See also

object
DotFormula extends NamedSymbol with AtomicFormula with StateDependent with Product with Serializable
⎵: Placeholder for formulas in uniform substitutions.
⎵: Placeholder for formulas in uniform substitutions. Reserved nullary predicational symbol _ for substitutions is unlike ordinary predicational symbols by convention.

object
ExpressionKind extends Kind with Product with Serializable
Expressions that are neither terms nor formulas nor programs nor functions would be of kind ExpressionKind

object
False extends AtomicFormula with Product with Serializable
Falsum formula false.

object
FormulaKind extends Kind with Product with Serializable
All formulas are of kind FormulaKind.
All formulas are of kind FormulaKind.
 See also

object
FunctionKind extends Kind with Product with Serializable
Function/predicate symbols that are not themselves terms or formulas are of kind FunctionKind, so degenerate.
Function/predicate symbols that are not themselves terms or formulas are of kind FunctionKind, so degenerate.
 See also

object
NoProverException extends ProverException
Nil case for exceptions, which is almost useless except when an exception type is needed to indicate that there really was none.

object
Nothing extends NamedSymbol with AtomicTerm with Product with Serializable
The empty argument of Unit sort (as argument for arity 0 function/predicate symbols).

object
PrettyPrinter extends (Expression) ⇒ String
A pretty printer for differential dynamic logic is an injective function from Expressions to Strings.
A pretty printer for differential dynamic logic is an injective function from Expressions to Strings. This object manages the default pretty printer that KeYmaera X uses in Expression.prettyString.

object
ProgramKind extends Kind with Product with Serializable
All programs are of kind ProgramKind.
All programs are of kind ProgramKind.
 See also

object
Provable extends Serializable
Starting new Provables to begin a proof, either with unproved conjectures or with proved axioms or axiomatic proof rules.
Starting new Provables to begin a proof, either with unproved conjectures or with proved axioms or axiomatic proof rules.

object
Real extends Sort with Product with Serializable
Sort of real numbers: 0, 1, 2.5, 42.
 object SeqPos
 object SetLattice

object
StaticSemantics
The static semantics of differential dynamic logic.
The static semantics of differential dynamic logic. This object defines the static semantics of differential dynamic logic in terms of the free variables and bound variables that expressions have as well as their signatures.
val fml = Imply(Greater(Variable("x",None,Real), Number(5)), Forall(Seq(Variable("y",None,Real)), GreaterEqual(Variable("x",None,Real), FuncOf(Function("f",None,Real,Real), Variable("y",None,Real))))) // determine the static semantics of the above formula val stat = StaticSemantics(fml) println("Free variables " + stat.fv) println("Bound variables " + stat.bv) // determine all function, predicate and program constants occurring in the above formula println("Signature " + StaticSemantics.signature(fml)) // determine all symbols occurring in the above formula println("Symbols " + StaticSemantics.symbols(fml))
 Note
soundnesscritical
 See also
Section 2.3 in Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
Example: 
object
SubstitutionAdmissibility
Admissibility conditions.

object
TermKind extends Kind with Product with Serializable
All terms are of kind TermKind.
All terms are of kind TermKind.
 See also

object
Trafo extends Sort with Product with Serializable
Sort of state transformations (i.e.
Sort of state transformations (i.e. programs and games).

object
True extends AtomicFormula with Product with Serializable
Verum formula true.

object
UniformRenaming extends Serializable
Convenience for uniform renaming.

object
Unit extends Sort with Product with Serializable
Unit type of Nothing used as no argument.
 object Variable

object
Version
KeYmaera X versions.
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