case class TermProvable(provable: ProvableSig, pt: ProofTerm, defs: Declaration) extends ProvableSig with Logging with Product with Serializable
TermProvable has the same signature as Provable, but constructs proof terms alongside Provables. The ProofTerms remember how the provable was proved.
- Alphabetic
- By Inheritance
- TermProvable
- Serializable
- Serializable
- Product
- Equals
- Logging
- LazyLogging
- LoggerHolder
- ProvableSig
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new TermProvable(provable: ProvableSig, pt: ProofTerm, defs: Declaration)
Type Members
- class DebugMeException extends Exception
-
type
Subgoal = Int
Position types for the subgoals of a Provable.
Position types for the subgoals of a Provable.
- Definition Classes
- ProvableSig
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
apply(prolongation: ProvableSig): ProvableSig
Substitute Subderivation Forward: Prolong this Provable with the given prolongation.
Substitute Subderivation Forward: Prolong this Provable with the given prolongation. This Provable with conclusion
G |- Dtransforms as followsG1 |- D1 ... Gn |- Dn G1 |- D1 ... Gn |- Dn ------------------------- => ------------------------- G |- D G0 |- D0provided
G |- D ------------------------- prolongation G0 |- D0- prolongation
the subderivation used to prolong this Provable. Where subderivation has a subgoal equaling our conclusion.
- returns
A Provable derivation that proves prolongation's conclusion from our subgoals.
- Definition Classes
- TermProvable → ProvableSig
-
def
apply(newConsequence: Sequent, rule: Rule): ProvableSig
Apply Rule Forward: Apply given proof rule forward in Hilbert style to prolong this Provable to a Provable for concludes.
Apply Rule Forward: Apply given proof rule forward in Hilbert style to prolong this Provable to a Provable for concludes. This Provable with conclusion
G |- Dtransforms as followsG1 |- D1 ... Gn |- Dn G1 |- D1 ... Gn |- Dn ------------------------- => ------------------------- G |- D newConsequenceprovided
G |- D ------------------------- rule newConsequence- newConsequence
the new conclusion that the rule shows to follow from this.conclusion
- rule
the proof rule to apply to concludes to reduce it to this.conclusion.
- returns
A Provable derivation that proves concludes from the same subgoals by using the given proof rule. Will return a Provable with the same subgoals but an updated conclusion.
- Definition Classes
- TermProvable → ProvableSig
-
def
apply(ren: URename): ProvableSig
<invalid inheritdoc annotation>
<invalid inheritdoc annotation>
- Definition Classes
- TermProvable → ProvableSig
-
def
apply(subst: USubst): ProvableSig
Apply a uniform substitution to a (locally sound!) Provable.
Apply a uniform substitution to a (locally sound!) Provable. Substitutes both subgoals and conclusion with the same uniform substitution
subst.G1 |- D1 ... Gn |- Dn s(G1) |- s(D1) ... s(Gn) |- s(Dn) ----------------------- => ----------------------------------- (USR) G |- D s(G) |- s(D)- subst
The uniform substitution (of no free variables) to be used on the premises and conclusion of this Provable.
- returns
The Provable resulting from applying
substto our subgoals and conclusion.
- Definition Classes
- TermProvable → ProvableSig
-
def
apply(subderivation: ProvableSig, subgoal: Subgoal): ProvableSig
Substitute subderivation as a proof of subgoal.
Substitute subderivation as a proof of subgoal. Merge: Replace premise subgoal by the given subderivation. Use the given provable derivation in place of the indicated subgoal of this Provable, returning the resulting concatenated Provable.
In particular, if subderivation.isProved, then the given subgoal will disappear, otherwise it will be replaced by the subgoals of subderivation (with the first subgoal of subderivation in place of subgoal and all other subgoals at the end).
This function implements the substitution principle for hypotheses.
G1 |- D1 ... Gi |- Di ... Gn |- Dn G1 |- D1 ... Gr1 |- Dr1 ... Gn |- Dn Gr2 |- Dr2 ... Grk | Drk ------------------------------------ => --------------------------------------------------------------- G |- D G |- Dusing the given subderivation
Gr1 |- Dr1 Gr2 |- Dr2 ... Grk |- Drk ------------------------------------ (subderivation) Gi |- Di- subderivation
the Provable derivation that proves premise subgoal.
- subgoal
the index of our subgoal that the given subderivation concludes.
- returns
A Provable derivation that joins our derivation and subderivation to a joint derivation of our conclusion using subderivation to show our subgoal. Will return a Provable with the same conclusion but an updated set of premises.
- Definition Classes
- TermProvable → ProvableSig
-
def
apply(rule: Rule, subgoal: Subgoal): ProvableSig
Apply Rule: Apply given proof rule to the indicated subgoal of this Provable, returning the resulting Provable
Apply Rule: Apply given proof rule to the indicated subgoal of this Provable, returning the resulting Provable
G1 |- D1 ... Gi |- Di ... Gn |- Dn G1 |- D1 ... Gr1 |- Dr1 ... Gn |- Dn Gr2 |- Dr2 ... Grk | Drk ------------------------------------ => --------------------------------------------------------------- G |- D G |- Dusing the rule instance
Gr1 |- Dr1 Gr2 |- Dr2 ... Grk |- Drk ------------------------------------ (rule) Gi |- Di- rule
the proof rule to apply to the indicated subgoal of this Provable derivation.
- subgoal
which of our subgoals to apply the given proof rule to.
- returns
A Provable derivation that proves the premise subgoal by using the given proof rule. Will return a Provable with the same conclusion but an updated set of premises.
- Definition Classes
- TermProvable → ProvableSig
-
def
apply(fw: (ProvableSig) ⇒ ProvableSig): ProvableSig
Apply forward tactic on all subgoals.
Apply forward tactic on all subgoals.
- Definition Classes
- ProvableSig
-
def
apply(fw: (ProvableSig) ⇒ ProvableSig, subgoal: Subgoal): ProvableSig
Apply forward tactic
fwatsubgoal.Apply forward tactic
fwatsubgoal.- Definition Classes
- ProvableSig
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
val
axiom: Map[String, Formula]
immutable list of sound axioms, i.e., valid formulas of differential dynamic logic.
immutable list of sound axioms, i.e., valid formulas of differential dynamic logic. (convenience method)
- Definition Classes
- ProvableSig
-
lazy val
axioms: Map[String, ProvableSig]
immutable list of Provables of sound axioms, i.e., valid formulas of differential dynamic logic.
immutable list of Provables of sound axioms, i.e., valid formulas of differential dynamic logic.
* ---------- (axiom) |- axiom
- Definition Classes
- TermProvable → ProvableSig
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
val
conclusion: Sequent
the conclusion
G |- Dthat follows if all subgoals are valid.the conclusion
G |- Dthat follows if all subgoals are valid.- Definition Classes
- TermProvable → ProvableSig
-
val
defs: Declaration
- Definition Classes
- TermProvable → ProvableSig
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
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()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
isProved: Boolean
Checks whether this Provable proves its conclusion.
Checks whether this Provable proves its conclusion.
- returns
true if conclusion is proved by this Provable, false if subgoals are missing that need to be proved first.
- Definition Classes
- ProvableSig
- See also
Provable.isProved
-
lazy val
logger: Logger
- Attributes
- protected
- Definition Classes
- LazyLogging → LoggerHolder
-
final
val
loggerName: String
- Attributes
- protected
- Definition Classes
- LoggerHolder
-
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
prettyString: String
<invalid inheritdoc annotation>
<invalid inheritdoc annotation>
- Definition Classes
- TermProvable → ProvableSig
- val provable: ProvableSig
-
def
proveArithmetic(t: QETool, f: Formula): ProvableSig
<invalid inheritdoc annotation>
<invalid inheritdoc annotation>
- Definition Classes
- TermProvable → ProvableSig
-
def
proveArithmeticLemma(t: QETool, f: Formula): Lemma
Proves a formula f in real arithmetic using an external tool for quantifier elimination.
Proves a formula f in real arithmetic using an external tool for quantifier elimination.
- t
The quantifier-elimination tool.
- f
The formula.
- returns
a Lemma with a quantifier-free formula equivalent to f and evidence as provided by the tool.
- Definition Classes
- TermProvable → ProvableSig
-
def
proved: Sequent
What conclusion this Provable proves if isProved.
What conclusion this Provable proves if isProved.
- Definition Classes
- TermProvable → ProvableSig
- val pt: ProofTerm
-
def
reapply(defs: Declaration): ProvableSig
Returns a copy of this provable with the definitions replaced by
defs.Returns a copy of this provable with the definitions replaced by
defs.- Definition Classes
- ProvableSig
-
def
reapply(underlying: Provable): ProvableSig
Returns a copy of this provable with the underlying provable replaced by
underlying.Returns a copy of this provable with the underlying provable replaced by
underlying.- Definition Classes
- ProvableSig
-
lazy val
rules: Map[String, ProvableSig]
immutable list of Provables of locally sound axiomatic proof rules.
immutable list of Provables of locally sound axiomatic proof rules.
Gi |- Di ---------- (axiomatic rule) G |- D
- Definition Classes
- TermProvable → ProvableSig
-
def
startProof(goal: Formula): ProvableSig
Begin a new proof for the desired conclusion formula from no antecedent.
Begin a new proof for the desired conclusion formula from no antecedent.
|- goal --------- |- goal
- goal
the desired conclusion formula for the succedent.
- returns
a Provable whose subgoals need to be all proved in order to prove goal.
- Definition Classes
- TermProvable → ProvableSig
-
def
startProof(goal: Sequent): ProvableSig
Begin a new proof for the desired conclusion goal
Begin a new proof for the desired conclusion goal
goal ------ goal
- goal
the desired conclusion.
- returns
a Provable whose subgoals need to be all proved in order to prove goal.
- Definition Classes
- TermProvable → ProvableSig
-
val
steps: Int
<invalid inheritdoc annotation>
<invalid inheritdoc annotation>
- Definition Classes
- TermProvable → ProvableSig
-
def
sub(subgoal: Subgoal): ProvableSig
Sub-Provable: Get a sub-Provable corresponding to a Provable with the given subgoal as conclusion.
Sub-Provable: Get a sub-Provable corresponding to a Provable with the given subgoal as conclusion. Provables resulting from the returned subgoal can be merged into this Provable to prove said subgoal.
- subgoal
the index of our subgoal for which to return a new open Provable.
- returns
an initial unfinished open Provable for the subgoal
i:Gi |- Di ---------- Gi |- Di
which is suitable for being merged back into this Provable for subgoal
isubsequently.
- Definition Classes
- TermProvable → ProvableSig
-
val
subgoals: IndexedSeq[Sequent]
the premises
Gi |- Dithat, if they are all valid, imply the conclusion.the premises
Gi |- Dithat, if they are all valid, imply the conclusion.- Definition Classes
- TermProvable → ProvableSig
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
<invalid inheritdoc annotation>
<invalid inheritdoc annotation>
- Definition Classes
- TermProvable → AnyRef → Any
-
val
underlyingProvable: Provable
The core's Provable that this object really represents.
The core's Provable that this object really represents.
- Definition Classes
- ProvableSig
-
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( ... )
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