object PolynomialArithV2 extends TwoThreeTreePolynomialRing
Polynomial Arithmetic.
Computations are carried out fairly efficiently in a distributive representation. Computations are certifying:
- the internal data structures maintain a proof that the constructed term equals the distributive representation
The main interface is that of a PolynomialRing
- Alphabetic
- By Inheritance
- PolynomialArithV2
- TwoThreeTreePolynomialRing
- Serializable
- Serializable
- Product
- Equals
- PolynomialRing
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- final case class NonPolynomialArithmeticException(message: String) extends IllegalArgumentException with NonSupportedOperationException with Product with Serializable
- final case class NonSupportedDivisorException(message: String) extends IllegalArgumentException with NonSupportedOperationException with Product with Serializable
- final case class NonSupportedExponentException(message: String) extends IllegalArgumentException with NonSupportedOperationException with Product with Serializable
-
trait
NonSupportedOperationException extends IllegalArgumentException
report operations not supported by polynomial arithmetic in computations
-
final
case class
NonSupportedOperationInapplicability(cause: NonSupportedOperationException) extends TacticInapplicableFailure with Product with Serializable
report operations not supported by polynomial arithmetic in tactics
-
trait
Polynomial extends AnyRef
Interface to Polynomials: - a term that keeps track of how the polynomial was constructed - a proof for the internal representation of the polynomial - arithmetic - test for zero
Interface to Polynomials: - a term that keeps track of how the polynomial was constructed - a proof for the internal representation of the polynomial - arithmetic - test for zero
- Definition Classes
- PolynomialRing
-
trait
PowerProduct extends AnyRef
- Definition Classes
- PolynomialRing
-
case class
Branch2(left: TreePolynomial, value: Monomial, right: TreePolynomial, prvO: Option[ProvableSig]) extends TreePolynomial with Product with Serializable
- Definition Classes
- TwoThreeTreePolynomialRing
-
case class
Branch3(left: TreePolynomial, value1: Monomial, mid: TreePolynomial, value2: Monomial, right: TreePolynomial, prvO: Option[ProvableSig]) extends TreePolynomial with Product with Serializable
- Definition Classes
- TwoThreeTreePolynomialRing
-
case class
Coefficient(num: BigDecimal, denom: BigDecimal, prvO: Option[ProvableSig] = None) extends Product with Serializable
prv: lhs = rhs lhs: input term (arbitrary, trace of construction) rhs: Divide(Number(num), Number(denom))
prv: lhs = rhs lhs: input term (arbitrary, trace of construction) rhs: Divide(Number(num), Number(denom))
- Definition Classes
- TwoThreeTreePolynomialRing
-
case class
Empty(prvO: Option[ProvableSig]) extends TreePolynomial with Product with Serializable
- Definition Classes
- TwoThreeTreePolynomialRing
-
sealed
trait
Growth extends AnyRef
2-3 Tree for monomials, keeping track of proofs.
2-3 Tree for monomials, keeping track of proofs.
- Definition Classes
- TwoThreeTreePolynomialRing
-
case class
Monomial(coeff: Coefficient, powerProduct: SparsePowerProduct, prvO: Option[ProvableSig] = None) extends Product with Serializable
prv: lhs = rhs lhs: input term (arbitrary, trace of construction) rhs: representation of
coeff*powers.map(^)
prv: lhs = rhs lhs: input term (arbitrary, trace of construction) rhs: representation of
coeff*powers.map(^)
- Definition Classes
- TwoThreeTreePolynomialRing
-
case class
SparsePowerProduct(sparse: Seq[(Term, Int)]) extends PowerProduct with Product with Serializable
- Definition Classes
- TwoThreeTreePolynomialRing
-
case class
Sprout(sprout: Branch2) extends Growth with Product with Serializable
- Definition Classes
- TwoThreeTreePolynomialRing
-
case class
Stay(p: TreePolynomial) extends Growth with Product with Serializable
- Definition Classes
- TwoThreeTreePolynomialRing
-
sealed
trait
TreePolynomial extends Polynomial
- Definition Classes
- TwoThreeTreePolynomialRing
-
final
case class
UnknownPolynomialImplementationException(other: TwoThreeTreePolynomialRing.Polynomial) extends RuntimeException with Product with Serializable
- Definition Classes
- TwoThreeTreePolynomialRing
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
Const(num: BigDecimal): TreePolynomial
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
def
Const(num: BigDecimal, denom: BigDecimal): TreePolynomial
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
lazy val
One: TreePolynomial
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
PolynomialRing(variableOrdering: Ordering[Term], monomialOrdering: Ordering[IndexedSeq[(Term, Int)]]): PolynomialRing
constructor for given variable and monomial orderings
-
def
Var(term: Term, power: Int): TreePolynomial
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
def
Var(term: Term): TreePolynomial
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
lazy val
branch2GrowLeft: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
- Note
for the Left case, could actually just use branch2Left
-
lazy val
branch2GrowRight: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch2Left: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch2Right: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch2Value: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3GrowLeft: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3GrowMid: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3GrowRight: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3Left: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3Mid: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3Right: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3Value1: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
branch3Value2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
lazy val
coefficientBigDecimalPrv: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
coefficientNegPrv: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
coefficientPlusPrv: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
coefficientTimesPrv: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constC: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constCl: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constCr: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constF: UnitFunctional
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constL: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constLd: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
constLemma: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constLn: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constR_: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constRd: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constRn: FuncOf
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
constX: UnitFunctional
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
divideIdentity: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
divideNeg: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
divideNumber: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
divideRat: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
emptySprout: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
lazy val
equalReflexive: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
equalityBySubtraction: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
equate(t1: Term, t2: Term): Option[ProvableSig]
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
val
equate: DependentPositionTactic
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
lazy val
identityTimes: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
lazy val
minusBranch2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
minusBranch3: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
minusEmpty: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
monTimesBranch2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
monTimesBranch3: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
monTimesZero: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
monomialOrdering: Ordering[IndexedSeq[(Term, Int)]]
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
monomialTimesLemma: ProvableSig
l = cl * xls r = cr * xrs c = cl*cr xs = xls ** xrs -> l*r=c*xs
l = cl * xls r = cr * xrs c = cl*cr xs = xls ** xrs -> l*r=c*xs
- Definition Classes
- TwoThreeTreePolynomialRing
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
lazy val
negTimes: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
negateBranch2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
negateBranch3: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
negateEmpty: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
normalize(term: Term): ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
val
normalizeAt: DependentPositionTactic
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
lazy val
normalizeBranch2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizeBranch3: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizeCoeff0: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizeCoeff1: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizeMonom0: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizeMonomCS: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizeMonomNCS: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizePowers1R: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizePowers1V: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizePowersC1: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizePowersCP: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizePowersCV: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizePowersRP: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
normalizePowersRV: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
implicit
def
ofInt(i: Int): Polynomial
- Definition Classes
- PolynomialRing
-
def
ofSparse(powers: (Term, Int)*): SparsePowerProduct
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
def
ofSparse(seq: Seq[(Term, Int)]): SparsePowerProduct
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
def
ofTerm(t: Term): Polynomial
- Definition Classes
- PolynomialRing
-
lazy val
partition2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
plusBranch2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
plusBranch3: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
plusEmpty: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
plusMinus: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
plusTimes: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
powerDivideLemma(i: Int): ProvableSig
lookup or prove lemma of the form "(x_(||) / y_(||))i = x_(||)i / y_(||)^i "
lookup or prove lemma of the form "(x_(||) / y_(||))i = x_(||)i / y_(||)^i "
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
powerEven: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
powerLemma: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
powerOdd: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
powerOne: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
powerPoly: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
powerZero: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
ratForm(term: Term): (Polynomial, Polynomial, ProvableSig)
- Definition Classes
- TwoThreeTreePolynomialRing → PolynomialRing
-
lazy val
rationalLemma: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
reassoc(prv: ProvableSig): ProvableSig
drop parentheses of a sum of terms on the rhs of prv to the left, e.g., t = a + (b + c) ~~> t = a + b + c
drop parentheses of a sum of terms on the rhs of prv to the left, e.g., t = a + (b + c) ~~> t = a + b + c
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
reassocLeft0RightConst: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
reassocRight0: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
reassocRightConst: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
reassocRightPlus: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
- def reportBelleThrowables[R](block: ⇒ R): R
-
lazy val
splitBranch2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
splitBranch3: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
splitCoefficient: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
splitCoefficientNumericCondition(n: Term, d: Term, n1: Term, d1: Term, n2: Term, d2: Term): And
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
splitEmpty: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
splitMonomial: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
def
symbols(t: Term): Seq[Term]
- Definition Classes
- PolynomialRing
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
lazy val
timesBranch2: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesBranch3: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesEmpty: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesIdentity: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesPowers1Left: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesPowers1Right: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesPowersBoth: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesPowersLeft: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
timesPowersRight: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
varLemma: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
lazy val
varPowerLemma: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
-
val
variableOrdering: Ordering[Term]
- Definition Classes
- TwoThreeTreePolynomialRing
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
lazy val
zez: ProvableSig
- Definition Classes
- TwoThreeTreePolynomialRing
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core
- KeYmaera X kernel, proof certificates, main data structuresExpression
- Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
- Sequents of formulasProvable
- Proof certificates transformed by rules/axiomsRule
- Proof rules as well asUSubstOne
for (one-pass) uniform substitutions and renaming.StaticSemantics
- Static semantics with free and bound variable analysisKeYmaeraXParser
.edu.cmu.cs.ls.keymaerax.parser
- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter
- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser
- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser
- Parser reading KeYmaera X model and proof archive.kyx
filesDLParser
- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
- Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.cmu.cs.ls.keymaerax.infrastruct
- Prover infrastructure outside the kernelUnificationMatch
- Unification algorithmRenUSubst
- Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context
- Representation for contexts of formulas in which they occur.Augmentors
- Augmenting formula and expression data structures with additional functionalityExpressionTraversal
- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon
- Bellerophon tactic language and tactic interpreterBelleExpr
- Tactic language expressionsSequentialInterpreter
- Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics
- Bellerophon tactic library for conducting proofs.TactixLibrary
- Main KeYmaera X tactic library including many proof tactics.HilbertCalculus
- Hilbert Calculus for differential dynamic logicSequentCalculus
- Sequent Calculus for propositional and first-order logicHybridProgramCalculus
- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
- Unification-based uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]
- Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma
- Lemma mechanismLemma
- Lemmas are Provables stored under a name, e.g., in files.LemmaDB
- Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe
- Real arithmetic back-end solversMathematicaQETool
- Mathematica interface for real arithmetic.Z3QETool
- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
- Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica
- Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3
- Z3 interface for real arithmetic including simplifiers.Entry Points
Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX
- Command-line launcher for KeYmaera X supports command-line argument-help
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.AxIndex
- Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex
- Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax
- Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos