final class DirectUSubstAboveURen extends RenUSubstBase
Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substitution.
s(RG) |- s(RD) -------------- USubst RG |- RD -------------- URen G |- D
Semantic renaming may be supported if need be.
DirectUSubstAboveURen is a direct implementation in tactics land of a joint renaming and substitution algorithm. It uses a single direct fast USubstRen for direct internal applications via DirectUSubstAboveURen.apply() but schedules separate uniform substitutions and uniform renamings to the core when asked. The first fast pass supports semantic renaming, which is useful during unification to "apply" renamings already to predicationals without clash. The final core pass does not support semantic renaming, but is only needed for the final unifier.
- Note
reading in Hilbert direction from top to bottom, the uniform substitution comes first to ensure the subsequent uniform renaming no longer has nonrenamable program constants since no semantic renaming.
- See also
- Alphabetic
- By Inheritance
- DirectUSubstAboveURen
- RenUSubstBase
- RenUSubst
- Function1
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new DirectUSubstAboveURen(subsDefsInput: Seq[(Expression, Expression)])
Type Members
-
type
RenUSubstRepl = (Expression, Expression)
A renaming substitution pair for a renaming uniform substitution.
A renaming substitution pair for a renaming uniform substitution.
- Definition Classes
- RenUSubst
- See also
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.TermAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.infrastruct.Augmentors.ProgramAugmentor.~>()
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
def
++(other: RenUSubst): RenUSubst
Union of renaming uniform substitutions, i.e., both replacement lists merged.
Union of renaming uniform substitutions, i.e., both replacement lists merged.
- Definition Classes
- RenUSubst
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A
- Definition Classes
- Function1
- Annotations
- @unspecialized()
-
def
apply(p: DifferentialProgram): DifferentialProgram
- Definition Classes
- DirectUSubstAboveURen → RenUSubst
-
def
apply(p: Program): Program
- Definition Classes
- DirectUSubstAboveURen → RenUSubst
-
def
apply(f: Formula): Formula
- Definition Classes
- DirectUSubstAboveURen → RenUSubst
-
def
apply(t: Term): Term
- Definition Classes
- DirectUSubstAboveURen → RenUSubst
-
def
apply(s: Sequent): Sequent
Apply everywhere in the sequent.
Apply everywhere in the sequent.
- Definition Classes
- RenUSubst
-
def
apply(e: Expression): Expression
- Definition Classes
- RenUSubst → Function1
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression
- Definition Classes
- Function1
- Annotations
- @unspecialized()
-
val
effective: USubstRen
The effective USubstRen consisting of the renaming and the renamed substitution, since the core substitution will be above the core renaming in the end.
The effective USubstRen consisting of the renaming and the renamed substitution, since the core substitution will be above the core renaming in the end.
- Attributes
- protected
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(e: Any): Boolean
- Definition Classes
- DirectUSubstAboveURen → AnyRef → Any
-
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
getRenamingTactic: BelleExpr
Get the renaming tactic part
Get the renaming tactic part
- Definition Classes
- RenUSubstBase → RenUSubst
-
def
hashCode(): Int
- Definition Classes
- DirectUSubstAboveURen → AnyRef → Any
-
def
isEmpty: Boolean
Returns true if there is no replacement.
Returns true if there is no replacement.
- Definition Classes
- RenUSubst
-
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
reapply(subs: Seq[(Expression, Expression)]): DirectUSubstAboveURen
Create a similar RenUSubst of the same class with the alternative list of replacements
Create a similar RenUSubst of the same class with the alternative list of replacements
- Definition Classes
- DirectUSubstAboveURen → RenUSubstBase → RenUSubst
-
def
renaming: RenUSubst
The uniform renaming part of this renaming uniform substitution
The uniform renaming part of this renaming uniform substitution
- Definition Classes
- RenUSubstBase → RenUSubst
-
final
val
rens: Seq[(Variable, Variable)]
Renaming part, with identity renaming no-ops filtered out.
Renaming part, with identity renaming no-ops filtered out.
- Attributes
- protected
- Definition Classes
- RenUSubstBase
-
final
val
subsDefs: Seq[SubstitutionPair]
Substitution part, with identity substitution no-ops filtered out.
Substitution part, with identity substitution no-ops filtered out.
- Attributes
- protected
- Definition Classes
- RenUSubstBase
-
def
substitution: RenUSubst
The uniform substitution part of this renaming uniform substitution
The uniform substitution part of this renaming uniform substitution
- Definition Classes
- RenUSubstBase → RenUSubst
- See also
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
val
toCore: (Expression) ⇒ Expression
This RenUSubst implemented strictly from the core.
This RenUSubst implemented strictly from the core.
- Definition Classes
- DirectUSubstAboveURen → RenUSubst
- Note
For contract purposes
-
val
toForward: (ProvableSig) ⇒ ProvableSig
Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.
Central operation to convert to forward tactic using the core's respective uniform renaming and uniform substitution rules.
- Definition Classes
- DirectUSubstAboveURen → RenUSubst
-
def
toString(): String
- Definition Classes
- DirectUSubstAboveURen → RenUSubstBase → Function1 → AnyRef → Any
-
def
toTactic(form: Sequent): BelleExpr
Convert to tactic to reduce to
formby successively using the respective uniform renaming and uniform substitution rulesConvert to tactic to reduce to
formby successively using the respective uniform renaming and uniform substitution rules- Definition Classes
- DirectUSubstAboveURen → RenUSubstBase
-
final
lazy val
usubst: USubst
The uniform substitution part of this renaming uniform substitution
The uniform substitution part of this renaming uniform substitution
- Definition Classes
- RenUSubstBase → RenUSubst
- Note
lazy val and postponing applicable() until actual use case would make it possible for useAt(inst) to modify before exception. Not sure that's worth it though.
- See also
-
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