object Kaisar
Created by bbohrer on 12/2/16.
- Alphabetic
- By Inheritance
- Kaisar
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- case class Auto() extends Method with Product with Serializable
- case class BRule(r: RuleSpec, tails: List[SP]) extends SP with Product with Serializable
- case class BadBranchingFactorException(had: Int, wanted: Int) extends Exception with Product with Serializable
- case class CloseId() extends Method with Product with Serializable
- case class Context(gmap: Map[Variable, Position], defmap: Map[VBase, Expression], fundefmap: Map[VBase, (VBase, Expression)]) extends Product with Serializable
- case class DiffCutInfo(proofVar: Variable, bcFml: Formula, indFml: Formula, bcProof: SP, indProof: SP) extends OdeInvInfo with Product with Serializable
- case class DiffGhostInfo(dgVar: Variable, dgPrime: Term, dg0: Term) extends OdeInvInfo with Product with Serializable
- case class FInst(fp: FP, t: Term) extends FP with Product with Serializable
- case class FLet(x: VBase, arg: VBase, e: Expression, tail: SP) extends SP with Product with Serializable
- case class FMP(fp1: FP, fp2: FP) extends FP with Product with Serializable
- abstract class FP extends AnyRef
- case class FPat(e: Expression) extends FP with Product with Serializable
- case class FactVariable(p: Variable) extends Resource with Product with Serializable
- case class Finally(tail: SP) extends IP with Product with Serializable
- case class Ghost(gvar: Variable, gterm: Term, ginv: Formula, x0: Term, pre: SP, inv: SP, tail: IP) extends IP with Product with Serializable
- case class HCAssign(hp: Assign) extends HistChange with Product with Serializable
- case class HCRename(baseName: BaseVariable, permName: BaseVariable, defn: Option[AntePos] = None) extends HistChange with Product with Serializable
- case class HCTimeStep(ts: TimeName) extends HistChange with Product with Serializable
- case class Have(x: Variable, fml: Formula, sp: SP, tail: SP) extends SP with Product with Serializable
- abstract class HistChange extends AnyRef
- case class History(steps: List[HistChange]) extends Product with Serializable
- abstract class IP extends AnyRef
- case class Inv(x: Variable, fml: Formula, pre: SP, inv: SP, tail: IP) extends IP with Product with Serializable
- abstract class Method extends AnyRef
- case class Note(x: Variable, fp: FP, tail: SP) extends SP with Product with Serializable
- abstract class OdeInvInfo extends AnyRef
- case class PatternMatchError(msg: String) extends Exception with Product with Serializable
- case class PrintGoal(msg: String, sp: SP) extends SP with Product with Serializable
- case class ProgramVariable(a: Variable) extends Resource with Product with Serializable
- type Proof = (Formula, SP)
- type ProofStep = (List[Resource], BelleExpr)
- case class RBAbbrev(xphi: Variable, x: Variable, theta: Term) extends RuleSpec with Product with Serializable
- case class RBAssign(hp: Assign) extends RuleSpec with Product with Serializable
- case class RBAssignAny(x: Variable) extends RuleSpec with Product with Serializable
- case class RBAssume(x: Variable, fml: Formula) extends RuleSpec with Product with Serializable
- case class RBCase(pats: List[Expression]) extends RuleSpec with Product with Serializable
- case class RBCaseImplyL(p: Variable, patp: Formula, q: Variable, patq: Formula) extends RuleSpec with Product with Serializable
- case class RBCaseOrL(x1: Variable, pat1: Expression, x2: Variable, pat2: Expression) extends RuleSpec with Product with Serializable
- case class RBCaseOrR(x1: Variable, x2: Variable) extends RuleSpec with Product with Serializable
- case class RBInv(ip: IP) extends RuleSpec with Product with Serializable
- case class RBMid(x: Variable, fml: Formula) extends RuleSpec with Product with Serializable
- case class RBSolve(t: Variable, fmlT: Formula, dc: Variable, fmlDC: Formula, sols: List[(Variable, Formula)]) extends RuleSpec with Product with Serializable
- case class RCF() extends Method with Product with Serializable
- case class RDAssert(x: Variable, fml: Formula) extends RuleSpec with Product with Serializable
- case class RDAssign(hp: Assign) extends RuleSpec with Product with Serializable
- case class RDAssignAny(x: Variable, xVal: Term) extends RuleSpec with Product with Serializable
- case class RDCase(a: Program) extends RuleSpec with Product with Serializable
- case class RDMid(fml: Formula) extends RuleSpec with Product with Serializable
- case class RDSolve(t: Variable, fmlT: Formula, dc: Variable, fmlDC: Formula, sols: List[(Variable, Formula)]) extends RuleSpec with Product with Serializable
- case class RIdent(x: String) extends RuleSpec with Product with Serializable
- abstract class Resource extends AnyRef
- abstract class RuleSpec extends AnyRef
- case class Run(a: VBase, hp: Program, tail: SP) extends SP with Product with Serializable
- case class SLet(pat: Expression, e: Expression, tail: SP) extends SP with Product with Serializable
- abstract class SP extends AnyRef
- case class Show(phi: Formula, proof: UP) extends SP with Product with Serializable
- case class Simp() extends Method with Product with Serializable
- case class SmartQE() extends Method with Product with Serializable
- case class State(st: TimeName, tail: SP) extends SP with Product with Serializable
- type TimeName = String
- case class UP(use: List[Either[Expression, FP]], method: Method) extends Product with Serializable
- type VBase = String
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
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
- def assertBranches(had: Int, wanted: Int): Unit
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
- def collectLoopInvs(ip: IP, h: History, hh: History, c: Context): (List[Variable], List[Formula], List[Formula], List[SP], List[SP], IP)
- def collectNegVarPat(t: Term): Option[List[BaseVariable]]
- def collectODEInvs(ip: IP, h: History, hh: History, c: Context): (List[OdeInvInfo], IP)
- def collectVarPat(t: Term): Option[List[BaseVariable]]
- def doesMatch(pat: Expression, e: Expression, c: Context, ante: IndexedSeq[Formula]): Boolean
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def eval(sp: SP, h: History, c: Context, g: Provable): Provable
- def eval(brule: RuleSpec, sp: List[SP], h: History, c: Context, g: Provable): Provable
- def eval(ip: IP, h: History, c: Context, g: Provable, nInvs: Int = 0): Provable
- def eval(fp: FP, h: History, c: Context, ante: IndexedSeq[Formula]): Provable
- def eval(up: UP, h: History, c: Context, g: Provable): Provable
- def eval(method: Method, pr: Provable): Provable
- def expand(e: Expression, h: History, c: Context, at: Option[TimeName]): Expression
- def expand(e: Program, h: History, c: Context, at: Option[TimeName]): Program
- def expand(e: Formula, h: History, c: Context, at: Option[TimeName]): Formula
- def expand(e: Term, h: History, c: Context, at: Option[TimeName]): Term
-
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()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def interpret(e: BelleExpr, pr: Provable): Provable
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
- def patChild(e: Expression): Option[Expression]
- def patIdent(e: Expression): Option[String]
- def pmatch(pat: Expression, e: Expression, c: Context, ante: IndexedSeq[Formula]): Context
- def polyK(pr: Provable, facts: List[Provable], onSecond: Boolean = false, impAtEnd: Boolean = false): Provable
- val propAxioms: Map[String, Formula]
- def rotAnte(pr: Provable): Provable
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
- def uniqueMatch(pat: Expression, c: Context, ante: IndexedSeq[Formula]): Int
-
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( ... )
- object Context extends Serializable
- object History extends Serializable
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