package core
KeYmaera X Kernel: Soundnesscritical core of the Axiomatic Tactical Theorem Prover KeYmaera X
The KeYmaera X Kernel implements Differential Dynamic Logic and defines
 Syntax of differential dynamic logic:
 Proof Construction of proof certificates from
 Provides basic lemma data storage, 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 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 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.DerivedAxioms.
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
Uniform substitutions can be used on proof certificates with the edu.cmu.cs.ls.keymaerax.core.Provable.apply(edu.cmu.cs.ls.keymaerax.core.USubst), 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
Lemma Mechanism
A lemma storage mechanism and an interface to real arithmetic decision procedures are defined in edu.cmu.cs.ls.keymaerax.core.Lemma 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.
 Note
Code Review 20160817
 See also
Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143189, 2008.
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. 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. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
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. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
 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.

sealed
trait
ApplicationOf extends Composite
Function/predicate/predicational application

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':=*

sealed
trait
Atomic extends Expression
Atomic expressions

sealed
trait
AtomicDifferentialProgram extends AtomicProgram with DifferentialProgram
Atomic differential programs

sealed
trait
AtomicFormula extends Formula with Atomic
Atomic formulas

case class
AtomicODE(xp: DifferentialSymbol, e: Term) extends AtomicDifferentialProgram with Product with Serializable
x'=e atomic differential equation

sealed
trait
AtomicProgram extends Program with Atomic
Atomic programs

sealed
trait
AtomicTerm extends Term with Atomic
Atomic terms

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 
sealed
trait
BinaryComposite extends Composite
Binary composite expressions that are composed of two subexpressions

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

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

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

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

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

case class
Close(assume: AntePos, pos: SuccPos) extends Rule with Product with Serializable
Close / Identity rule
Close / Identity rule
*  (Id) p, G  p, D

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

case class
CloseTrue(pos: SuccPos) extends RightRule with Product with Serializable
Close by true
Close by true
*  (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
Not used, just contained for symmetry reasons
,Rarely useful (except for contradictory
p
)

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

sealed
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

sealed
trait
Composite extends Expression
Composite expressions that are composed of subexpressions

sealed
trait
CompositeFormula extends Formula with Composite
Composite formulas

sealed
trait
CompositeProgram extends Program with Composite
composite programs

sealed
trait
CompositeTerm extends Term with Composite
Composite terms

class
CoreException extends ProverException
Critical exceptions from the KeYmaera X Prover Core.

case class
Cut(c: Formula) extends Rule with Product with Serializable
Cut in the given formula c.
Cut in the given formula c.
G, c  D G  D, c  (cut) G  D
 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
' differential of a term

case class
DifferentialFormula(child: Formula) extends UnaryCompositeFormula with Product with Serializable
Differential formula are differentials of formulas in analogy to differential terms (child)'

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 reassociates to list form DifferentialProduct(AtomicDifferentialProgram, DifferentialProduct(AtomicDifferentialProgram, ....))
 Note
Private constructor so only DifferentialProduct.apply can ever create this, which will reassociate et al.
,This is a case class except for an override of the apply function.

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

sealed
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 taboo is neither free nor bound, so the run does not depend on the value of taboo nor does the value of taboo change when space=Except(taboo).

case class
DifferentialSymbol(x: Variable) extends Variable with RTerm with Product with Serializable
Differential symbol x' for variable x

case class
Divide(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable
/ real division

sealed
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 symbol \\cdot for uniform substitutions are unlike ordinary function symbols

case class
Dual(child: Program) extends UnaryCompositeProgram with Product with Serializable
child^d
dual program

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

trait
Evidence extends AnyRef
"Weak" Correctness evidence for lemmas

case class
Except(taboo: Variable) extends Space with Product with Serializable
The sort denoting a slice of the state space that does not include/depend on/affect variable
taboo
. 
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

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
See Section 2.1
 See also
Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.

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

sealed
trait
Formula extends Expression
Formulas of differential dynamic logic.
Formulas of differential dynamic logic.
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_
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)

sealed
case class
Function(name: String, index: Option[Int] = None, domain: Sort, sort: Sort, interpreted: Boolean = false) extends Expression with 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
 interpreted
when
true
this function symbol has a fixed interpretation/definition.

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

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

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 CoreException with Product with Serializable
Rule is not applicable as indicated

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

trait
LeftRule extends PositionRule
A rule applied to a position in the antecedent on the left

final
case class
Lemma(fact: ProvableSig, evidence: List[Evidence], name: Option[String] = None) extends Product with Serializable
Lemmas are named Provables, supported by some evidence of how they came about.
Lemmas are named Provables, supported by some evidence of how they came about. The soundnesscritical part in a lemma is its provable fact, which can only be obtained from the prover core.
// prove a lemma val proved = TactixLibrary.proveBy( Sequent(IndexedSeq(), IndexedSeq("true  x>5".asFormula)), orR(1) & close ) // store a lemma val lemmaDB = LemmaDBFactory.lemmaDB val evidence = ToolEvidence(immutable.Map("input" > proved.toString, "output" > "true")) :: Nil)) val lemmaID = lemmaDB.add( Lemma(proved, evidence, Some("Lemma test")) ) // retrieve a lemma val lemmaFact = lemmaDB.get(lemmaID).get.fact // use a lemma literally TactixLibrary.by(lemmaFact) // use a uniform substitution instance of a lemma TactixLibrary.byUS(lemmaFact)
 Note
Construction is not soundnesscritical so constructor is not private, because Provables can only be constructed by prover core.
 See also
ProvableSig.proveArithmetic
Example: 
case class
Less(left: Term, right: Term) extends RComparisonFormula with Product with Serializable
<= less than comparison left < right

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

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

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

sealed
trait
Modal extends CompositeFormula
Modal formulas

sealed
trait
NamedSymbol extends Expression with Ordered[NamedSymbol]
A named symbol such as a variable or function symbol or predicate symbol.
A named symbol such as a variable or function symbol or predicate 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: minus

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

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.

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

trait
PositionRule extends Rule
A rule applied to a position

case class
Power(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable
real exponentiation or power: left^{right}

case class
PredOf(func: Function, child: Term) extends AtomicFormula with ApplicationOf with Product with Serializable
Predicate symbol applied to argument child func(child)

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.

sealed
trait
Program extends Expression
Hybrid programs of differential dynamic logic.
Hybrid programs of differential dynamic logic.
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?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

sealed
case class
ProgramConst(name: String, space: Space = AnyArg) extends NamedSymbol with AtomicProgram with SpaceDependent with Product with Serializable
Uninterpreted program constant / game symbol, limited to the given state space.
Uninterpreted program constant / game symbol, limited to the given state space. The semantics of ProgramConst symbol is looked up by the state, with the additional promise that taboo is neither free nor bound, so the run does not depend on the value of taboo nor does the value of taboo change when space=Except(taboo).

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.
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) )
, 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)
, 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 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)
, 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 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)
 Note
For soundness: No reflection should bypass constructor call privacy, nor reflection to bypass immutable val algebraic data types.
,Only private constructor calls for soundness
,soundnesscritical logical framework.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Examples: 
case class
ProverAssertionError(msg: String) extends ProverException with Product with Serializable
Assertions that fail in the prover

class
ProverException extends RuntimeException
KeYmaera X Prover Exceptions.

trait
QETool extends AnyRef
Quantifier elimination tool.
Quantifier elimination tool.

sealed
trait
Quantified extends CompositeFormula
Quantified formulas

case class
RenamingClashException(msg: String, ren: String, e: String, info: String = "") extends CoreException with Product with Serializable
Uniform or bound renaming clash exception

trait
RightRule extends PositionRule
A rule applied to a position in the succedent on the right

sealed
trait
Rule extends (Sequent) ⇒ List[Sequent]
Subclasses represent all proof rules.
Subclasses represent all proof rules. A proof rule is ultimately a named mapping from sequents to lists of sequents. The resulting list of sequents represent the subgoal/premise andbranches 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

sealed
trait
SeqPos extends AnyRef
Position of a formula in a sequent, i.e.

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 top and toplike elements.
 A
Type of elements in the set

case class
SkolemClashException(msg: String, clashedNames: SetLattice[Variable], vars: String, s: String) extends CoreException with Product with Serializable
Skolem symbol clash

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

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

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

sealed
trait
SpaceDependent extends StateDependent
Expressions limited to a given sub statespace.
Expressions limited to a given sub statespace.
 Since
4.2

sealed
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
SubstitutionClashException(subst: String, U: String, e: String, context: String, clashes: String, info: String = "") extends CoreException with Product with Serializable
Substitution clash

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. what
the expression to be replaced.
what
can have one of the following forms: 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.

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.

sealed
case class
SystemConst(name: String) extends NamedSymbol with AtomicProgram with StateDependent with Product with Serializable
Uninterpreted hybrid system program constant that are NOT hybrid games.

sealed
trait
Term extends Expression
Terms of differential dynamic logic.
Terms of differential dynamic logic.
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.
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

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) 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'
). what
What variable to replace (along with its associated DifferentialSymbol).
 repl
The target variable to replace
what
with and vice versa.
 Note
soundnesscritical
 See also

final
case class
USubst(subsDefsInput: Seq[SubstitutionPair]) extends (Expression) ⇒ Expression with Product with Serializable
A Uniform Substitution with its application mechanism.
A Uniform Substitution with its 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 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.
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)
, 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 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 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))
 Note
soundnesscritical
,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.
 See also
edu.cmu.cs.ls.keymaerax.core.Provable.apply(edu.cmu.cs.ls.keymaerax.core.UniformSubstitution)
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.
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.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Examples: 
sealed
trait
UnaryComposite extends Composite
Unary composite expressions that are composed of one subexpression

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

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

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

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.
 what
What variable to replace (along with its associated DifferentialSymbol).
 repl
The target variable to replace what with.
 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
, limited to the given state space.Arity 0 functional symbol
name:sort
, limited to the given state space. The semantics of arity 0 functional symbol is given by the state, with the additional promise that taboo is not free so the value does not depend on taboo when space=Except(taboo). 
case class
UnitPredicational(name: String, space: Space) extends AtomicFormula with SpaceDependent with NamedSymbol with Product with Serializable
Arity 0 predicational symbol
name:bool
, limited to the given state space.Arity 0 predicational symbol
name:bool
, limited to the given state space. The semantics of arity 0 predicational symbol is looked up by the state, with the additional promise that taboo is not free so the value does not depend on taboo when space=Except(taboo). 
case class
UnknownOperatorException(msg: String, e: Expression) extends ProverException with Product with Serializable
Thrown to indicate when an unknown operator occurs

sealed
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.
Value Members

val
VERSION: String
KeYmaera X core kernel version number

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

object
DifferentialProgramKind extends Kind
All differential programs are of kind DifferentialProgramKind

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

object
ExpressionKind extends Kind
All expressions that are neither terms nor formulas nor programs nor functions are of kind ExpressionKind

object
False extends AtomicFormula
Falsum formula false

object
FormulaKind extends Kind
All formulas are of kind FormulaKind

object
FunctionKind extends Kind
Function/predicate symbols that are not themselves terms or formulas are of kind FunctionKind

object
Lemma extends Serializable
Facility for reading lemmas back in from their string representation.

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
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 a function from Expressions to Strings.
A pretty printer for differential dynamic logic is a function from Expressions to Strings. This object manages the default pretty printer that KeYmaera X uses in Expression.prettyString.

object
ProgramKind extends Kind
All programs are of kind ProgramKind

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

object
Real extends Sort
Sort of real numbers: 0, 1, 2.5
 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. See Section 2.3
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
Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.
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.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Example: 
object
SubstitutionAdmissibility
Admissibility conditions.

object
TermKind extends Kind
All terms are of kind TermKind

object
Trafo extends Sort
Sort of state transformations (i.e.
Sort of state transformations (i.e. programs)

object
True extends AtomicFormula
Verum formula true

object
UniformRenaming extends Serializable
Convenience for uniform renaming.

object
Unit extends Sort
Unit type of Nothing
 object Variable
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 structuresedu.cmu.cs.ls.keymaerax.core.Expression
 Differential dynamic logic expressionsedu.cmu.cs.ls.keymaerax.core.Sequent
 Sequents of formulasedu.cmu.cs.ls.keymaerax.core.Rule
 Proof rulesedu.cmu.cs.ls.keymaerax.core.Provable
 Proof certificateedu.cmu.cs.ls.keymaerax.btactics
 Tactic language libraryedu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
 Main tactic libraryedu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicedu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
 Sequent Calculus for propositional and firstorder logicedu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus
 Unificationbased Uniform Substitution Calculusedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreteredu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr
 Tactic language expressionsedu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
 Sequential tactic interpreteredu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
 Parser for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter
 Pretty printer for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser
 Parser for KeYmaera X problem files.kyx
edu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismedu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB
 Lemma database stored in filesedu.cmu.cs.ls.keymaerax.tools
 Arithmetic backendsedu.cmu.cs.ls.keymaerax.tools.Mathematica
 Mathematica interface for real arithmetic and ODE solver etc.edu.cmu.cs.ls.keymaerax.tools.Z3
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.Polya
 Polya interface for real arithmetic.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.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.References
Full references are provided elsewhere 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, LNCS. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.