package scaladsl
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- scaladsl
- Predef
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Type Members
- type AMonomial[E <: poly.multivar.AMonomial[E]] = poly.multivar.AMonomial[E]
- type AMultivariatePolynomial[T <: poly.multivar.AMonomial[T], P <: poly.multivar.AMultivariatePolynomial[T, P]] = poly.multivar.AMultivariatePolynomial[T, P]
- type Coder[E] = io.Coder[E, _, _]
- type DegreeVector = poly.multivar.DegreeVector
- type IPolynomial[P <: poly.IPolynomial[P]] = poly.IPolynomial[P]
- type IUnivariatePolynomial[P <: poly.univar.IUnivariatePolynomial[P]] = poly.univar.IUnivariatePolynomial[P]
- type IntZ = BigInteger
- type Monomial[E] = poly.multivar.Monomial[E]
- type MonomialZp64 = poly.multivar.MonomialZp64
- type MultivariatePolynomial[E] = poly.multivar.MultivariatePolynomial[E]
- type MultivariatePolynomialZp64 = poly.multivar.MultivariatePolynomialZp64
- type Ordering = Comparator[DegreeVector]
- type PolynomialFactorDecomposition[P <: IPolynomial[P]] = poly.PolynomialFactorDecomposition[P]
- type PrecomputedInverse[Poly <: IUnivariatePolynomial[Poly]] = InverseModMonomial[Poly]
- type Rational[E] = rings.Rational[E]
-
final
class
RichArrayTuple[Poly] extends AnyRef
- Definition Classes
- Predef
- type UnivariatePolynomial[E] = poly.univar.UnivariatePolynomial[E]
- type UnivariatePolynomialZp64 = poly.univar.UnivariatePolynomialZp64
Value Members
-
def
GaussianIntegers(imaginaryUnit: String): AlgebraicNumberField[IntZ]
- Definition Classes
- Predef
-
lazy val
GaussianIntegers: AlgebraicNumberField[IntZ]
- Definition Classes
- Predef
-
def
GaussianNumbers[E](ring: Ring[E], imaginaryUnit: String): AlgebraicNumberField[E]
- Definition Classes
- Predef
-
def
GaussianRationals(imaginaryUnit: String): AlgebraicNumberField[Rational[IntZ]]
- Definition Classes
- Predef
-
lazy val
GaussianRationals: AlgebraicNumberField[Rational[IntZ]]
- Definition Classes
- Predef
-
val
Q: Ring[rings.Rational[BigInteger]]
- Definition Classes
- Predef
-
def
SplittingField[E](poly: UnivariatePolynomial[E], variables: Array[String]): MultipleFieldExtension[Monomial[E], MultivariatePolynomial[E], UnivariatePolynomial[E], E]
- Definition Classes
- Predef
-
def
SplittingField[Term <: AMonomial[Term], mPoly <: AMultivariatePolynomial[Term, mPoly], sPoly <: IUnivariatePolynomial[sPoly], E](poly: sPoly, variables: Array[String]): MultipleFieldExtension[Term, mPoly, sPoly, E]
- Definition Classes
- Predef
-
def
SplittingFieldZp64(poly: UnivariatePolynomialZp64, variables: Array[String]): MultipleFieldExtension[MonomialZp64, MultivariatePolynomialZp64, UnivariatePolynomialZp64, Long]
- Definition Classes
- Predef
-
val
Z: Ring[BigInteger]
- Definition Classes
- Predef
-
def
Zp(modulus: BigInt): Ring[BigInteger]
- Definition Classes
- Predef
-
def
Zp(modulus: BigInteger): Ring[BigInteger]
- Definition Classes
- Predef
-
def
Zp(modulus: Long): Ring[BigInteger]
- Definition Classes
- Predef
-
def
Zp64(modulus: Long): IntegersZp64
- Definition Classes
- Predef
-
implicit
def
arrayToTuple[Poly](arr: Array[Poly]): RichArrayTuple[Poly]
- Definition Classes
- Predef
-
implicit
def
asBigInteger(v: Long): IntZ
- Definition Classes
- Predef
-
implicit
def
asBigInteger(v: Int): IntZ
- Definition Classes
- Predef
-
implicit
def
asBigInteger(v: BigInteger): IntZ
- Definition Classes
- Predef
-
implicit
def
asBigInteger(v: BigInt): IntZ
- Definition Classes
- Predef
-
implicit
def
asIdeal[Term <: AMonomial[Term], Poly <: AMultivariatePolynomial[Term, Poly], E](ideal: poly.multivar.Ideal[Term, Poly]): Ideal[Term, Poly, E]
- Definition Classes
- Predef
-
implicit
def
asRandomGenerator(rnd: Random): RandomGenerator
- Definition Classes
- Predef
-
implicit
def
asRing(ring: IntegersZp64): Ring[Long]
- Definition Classes
- Predef
-
implicit
def
asRing[E](ring: rings.Ring[E]): Ring[E]
- Definition Classes
- Predef
-
implicit
def
asRingElement[E](v: Long)(implicit ring: Ring[E]): E
- Definition Classes
- Predef
-
implicit
def
asRingElement[E](v: Int)(implicit ring: Ring[E]): E
- Definition Classes
- Predef
-
implicit
def
factors2Seq[E](factors: FactorDecomposition[E]): Seq[(E, Int)]
- Definition Classes
- Predef
-
implicit
def
idealMethods[Term <: AMonomial[Term], Poly <: AMultivariatePolynomial[Term, Poly], E](ideal: Ideal[Term, Poly, E]): poly.multivar.Ideal[Term, Poly]
- Definition Classes
- Predef
-
implicit
def
ringMethods[E](ring: Ring[E]): rings.Ring[E]
- Definition Classes
- Predef
-
implicit
def
ringMethods[E](ring: GaloisField[E]): FiniteField[UnivariatePolynomial[E]]
- Definition Classes
- Predef
-
implicit
def
ringMethods(ring: GaloisField64): FiniteField[UnivariatePolynomialZp64]
- Definition Classes
- Predef
-
implicit
def
ringMethods(ring: MultivariateRingZp64): poly.MultivariateRing[MultivariatePolynomialZp64]
- Definition Classes
- Predef
-
implicit
def
ringMethods[E](ring: MultivariateRing[E]): poly.MultivariateRing[MultivariatePolynomial[E]]
- Definition Classes
- Predef
-
implicit
def
ringMethods(ring: UnivariateRingZp64): poly.UnivariateRing[UnivariatePolynomialZp64]
- Definition Classes
- Predef
-
implicit
def
ringMethods[E](ring: UnivariateRing[E]): poly.UnivariateRing[UnivariatePolynomial[E]]
- Definition Classes
- Predef
-
implicit
def
ringMethods[Poly <: IPolynomial[Poly], E](ring: IPolynomialRing[Poly, E]): poly.IPolynomialRing[Poly]
- Definition Classes
- Predef
-
object
Rational
- Definition Classes
- Predef
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,ProgramSequent- Sequents of formulasProvable- Proof certificates transformed by rules/axiomsRule- Proof rules as well asUSubstOnefor (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.kyxfilesDLParser- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser- Combinator parser reading KeYmaera X model and proof archive.kyxfilesedu.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-helpto 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