case class DbPlainExecStepProofTreeNode(db: DBAbstraction, id: ProofTreeNodeId, proof: ProofTree, stepLoader: () ⇒ ExecutionStepPOJO) extends DbProofTreeNode with Logging with Product with Serializable
A proof tree node backed by a database of recorded execution steps. An ID Some(step),None points to the source node where step was executed, an ID Some(step),Some(branch) represents a proxy for the branch subgoal created by step and searches the actual successor step on demand.
- Alphabetic
- By Inheritance
- DbPlainExecStepProofTreeNode
- Serializable
- Serializable
- Product
- Equals
- Logging
- LazyLogging
- LoggerHolder
- DbProofTreeNode
- ProofTreeNode
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new DbPlainExecStepProofTreeNode(db: DBAbstraction, id: ProofTreeNodeId, proof: ProofTree, stepLoader: () ⇒ ExecutionStepPOJO)
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
allAncestors: List[ProofTreeNode]
All direct and indirect ancestors of this node.
All direct and indirect ancestors of this node.
- Definition Classes
- ProofTreeNode
-
def
allDescendants: List[ProofTreeNode]
All direct and indirect descendants of this node.
All direct and indirect descendants of this node.
- Definition Classes
- ProofTreeNode
-
def
applicableTacticsAt(pos: Position, pos2: Option[Position] = None): List[(DerivationInfo, Option[DerivationInfo])]
Returns a list of tactics that are applicable at the specified position in this node's goal.
Returns a list of tactics that are applicable at the specified position in this node's goal. Each entry is the typical form of the tactic and an optional more convenient variant of the tactic.
- Definition Classes
- ProofTreeNode
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
children: List[ProofTreeNode]
The node's children.
The node's children.
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
final
def
conclusion: Sequent
The tree node's conclusion (might be subject to other nodes being proved).
The tree node's conclusion (might be subject to other nodes being proved).
- Definition Classes
- ProofTreeNode
- val db: DBAbstraction
-
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()
-
def
goal: Option[Sequent]
The node's goal
The node's goal
- Definition Classes
- DbProofTreeNode → ProofTreeNode
-
def
goalIdx: Int
The index of the goal (subgoal in local provable) that this node targets.
The index of the goal (subgoal in local provable) that this node targets.
- Definition Classes
- DbProofTreeNode → ProofTreeNode
-
val
id: ProofTreeNodeId
The node ID.
The node ID.
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
isProved: Boolean
Indicates whether or not the proof from this node downwards is done (potentially expensive).
Indicates whether or not the proof from this node downwards is done (potentially expensive).
- Definition Classes
- ProofTreeNode
- See also
ProvableSig.isProved
-
def
label: Option[BelleLabel]
The node label.
The node label.
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
def
localProvable: ProvableSig
A local provable, whose subgoals are filled in by the node's children.
A local provable, whose subgoals are filled in by the node's children.
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
lazy val
logger: Logger
- Attributes
- protected
- Definition Classes
- LazyLogging → LoggerHolder
-
final
val
loggerName: String
- Attributes
- protected
- Definition Classes
- LoggerHolder
-
def
maker: Option[String]
The tactic that produced this node from its parent.
The tactic that produced this node from its parent.
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
def
makerShortName: Option[String]
The tactic short name.
The tactic short name.
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
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
numSubgoals: Int
The number of subgoals in the local provable (fast, doesn't actually load the provable).
The number of subgoals in the local provable (fast, doesn't actually load the provable).
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
def
parent: Option[ProofTreeNode]
The node's parent, None if root.
The node's parent, None if root.
- Definition Classes
- DbPlainExecStepProofTreeNode → ProofTreeNode
-
val
proof: ProofTree
The proof that this proof node is a part of.
The proof that this proof node is a part of.
- Definition Classes
- DbPlainExecStepProofTreeNode → DbProofTreeNode → ProofTreeNode
-
final
def
provable: ProvableSig
Compute the overall provable with the sub-proofs already filled in for the local subgoals (potentially expensive) from children.
Compute the overall provable with the sub-proofs already filled in for the local subgoals (potentially expensive) from children.
- Definition Classes
- ProofTreeNode
- See also
-
def
pruneBelow(): Unit
Deletes this node with the entire subtree underneath.
Deletes this node with the entire subtree underneath.
- Definition Classes
- DbProofTreeNode → ProofTreeNode
-
def
runTactic(userId: String, interpreter: (List[IOListener]) ⇒ Interpreter, tactic: BelleExpr, shortName: String, executor: BellerophonTacticExecutor = ..., wait: Boolean = false): String
Runs a tactic on this node.
Runs a tactic on this node.
- Definition Classes
- DbProofTreeNode → ProofTreeNode
-
def
stepId: Option[Int]
Execution step recording: predecessor step ID (=this, when executing a tactic on this).
Execution step recording: predecessor step ID (=this, when executing a tactic on this).
- Attributes
- protected
- Definition Classes
- DbPlainExecStepProofTreeNode → DbProofTreeNode
- val stepLoader: () ⇒ ExecutionStepPOJO
-
def
stepTactic(userId: String, interpreter: Interpreter, tactic: BelleExpr, executor: BellerophonTacticExecutor = ..., wait: Boolean = false): String
Runs a tactic step-by-step, starting on this node.
Runs a tactic step-by-step, starting on this node.
- Definition Classes
- DbProofTreeNode → ProofTreeNode
-
def
substs: List[SubstitutionPair]
Uniform substitutions applied at this node.
Uniform substitutions applied at this node.
- Definition Classes
- ProofTreeNode
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
tacticInputSuggestions(pos: Position): Map[ArgInfo, Expression]
Returns suggestions for tactic argument inputs, argument info according to UIIndex and DerivationInfo.
Returns suggestions for tactic argument inputs, argument info according to UIIndex and DerivationInfo.
- Definition Classes
- DbProofTreeNode → ProofTreeNode
-
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