trait LeftTactic extends BelleExpr with PositionalTactic
Tactics that can only be applied in the antecedent on the left.
- See also
LeftRule
- Alphabetic
- By Inheritance
- LeftTactic
- PositionalTactic
- AtPosition
- Logging
- LazyLogging
- LoggerHolder
- Function1
- BelleExpr
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Abstract Value Members
-
abstract
def
computeResult(provable: ProvableSig, position: AntePosition): ProvableSig
- Note
this should be called from within interpreters, but not by end-users
-
abstract
def
prettyString: String
pretty-printed form of this Bellerophon tactic expression
pretty-printed form of this Bellerophon tactic expression
- Definition Classes
- BelleExpr
Concrete Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
def
&(other: BelleExpr): BelleExpr
this & other: sequential composition this ; other executes other on the output of this, failing if either fail.
this & other: sequential composition this ; other executes other on the output of this, failing if either fail.
- Definition Classes
- BelleExpr
-
def
*(n: Int): BelleExpr
this*n: bounded repetition executes this tactic to
timesnumber of times, failing if any of those repetitions fail.this*n: bounded repetition executes this tactic to
timesnumber of times, failing if any of those repetitions fail.- Definition Classes
- BelleExpr
-
def
<(children: BelleExpr*): BelleExpr
<(e1,...,en): branching to run tactic
eion branchi, failing if any of them fail or if there are not exactlynbranches.<(e1,...,en): branching to run tactic
eion branchi, failing if any of them fail or if there are not exactlynbranches.- Definition Classes
- BelleExpr
- Note
Equivalent to
a & Idioms.<(b,c)
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
U(p: (SequentType, (RenUSubst) ⇒ BelleExpr)*): BelleExpr
case _ of {fi => ei} uniform substitution case pattern applies the first ei such that fi uniformly substitutes to current provable for which ei does not fail, fails if the ei of all matching fi fail.
case _ of {fi => ei} uniform substitution case pattern applies the first ei such that fi uniformly substitutes to current provable for which ei does not fail, fails if the ei of all matching fi fail.
- Definition Classes
- BelleExpr
-
def
andThen[A](g: (AppliedPositionTactic) ⇒ A): (PositionLocator) ⇒ A
- Definition Classes
- Function1
- Annotations
- @unspecialized()
-
final
def
apply(locator: PositionLocator): AppliedPositionTactic
Returns the tactic that can be applied at the position identified by
locator.Returns the tactic that can be applied at the position identified by
locator.- locator
The locator: Fixed, Find, LastAnte, or LastSucc
- returns
The tactic of type
Tthat can be readily applied at the position identified bylocatorto any given BelleExpr.
- Definition Classes
- PositionalTactic → AtPosition → Function1
- See also
-
final
def
apply(locator: Symbol, expected: Expression): AppliedPositionTactic
- Definition Classes
- AtPosition
-
final
def
apply(locator: Symbol, expected: Expression, defs: Declaration): AppliedPositionTactic
Returns the tactic at the position identified by
locator, ensuring thatlocatorwill yield the formulaexpectedverbatim.Returns the tactic at the position identified by
locator, ensuring thatlocatorwill yield the formulaexpectedverbatim.- locator
The locator symbol at which to apply this AtPosition: 'L (find left), 'R (find right), '_ (find left/right appropriately for tactic), 'Llast (at last position in antecedent), or 'Rlast (at last position in succedent).
- expected
the formula expected at the position that
locatoridentifies. Contract fails if that expectation is not met.
- Definition Classes
- AtPosition
- Note
Convenience wrapper
- See also
apply()
-
final
def
apply(locator: Symbol): AppliedPositionTactic
- Definition Classes
- AtPosition
-
final
def
apply(locator: Symbol, inExpr: PosInExpr): AppliedPositionTactic
Returns the tactic at the position identified by
locator.Returns the tactic at the position identified by
locator.- locator
The locator symbol at which to apply this AtPosition: 'L (find left), 'R (find right), '_ (find left/right appropriately for tactic), 'Llast (at last position in antecedent), or 'Rlast (at last position in succedent).
- Definition Classes
- AtPosition
- Note
Convenience wrapper
- See also
PositionLocator)
-
final
def
apply(seqIdx: Int, inExpr: PosInExpr): AppliedPositionTactic
- Definition Classes
- AtPosition
-
final
def
apply(seqIdx: Int, inExpr: List[Int] = Nil): AppliedPositionTactic
Applied at a fixed position in (signed) sequent position
seqIdxat subexpressioninExpr.Applied at a fixed position in (signed) sequent position
seqIdxat subexpressioninExpr.- seqIdx
The signed index in the sequent (strictly negative index for antecedent, strictly positive for succedent).
- inExpr
Where to apply inside the formula at index seqIdx interpreted as a PosInExpr.
- returns
The tactic of type
Tthat can be readily applied at the specified position to any given BelleExpr.
- Definition Classes
- AtPosition
- Note
Convenience wrapper
- See also
PosInExpr
Position)
-
final
def
apply(seqIdx: Int, inExpr: PosInExpr, expected: Formula): AppliedPositionTactic
- Definition Classes
- AtPosition
-
final
def
apply(seqIdx: Int, inExpr: List[Int], expected: Formula): AppliedPositionTactic
Applied at a fixed position, ensuring that the formula
expectedwill be found at that position, verbatim.Applied at a fixed position, ensuring that the formula
expectedwill be found at that position, verbatim.- seqIdx
The position where this tactic will be applied at (-1 based for antecedent, 1 based for succedent).
- expected
the formula expected at
position. Contract fails if that expectation is not met.- returns
The tactic of type
Tthat can be readily applied at the specified position to any given BelleExpr.
- Definition Classes
- AtPosition
- Note
Convenience wrapper
- See also
PositionLocator)
-
final
def
apply(seqIdx: Int, expected: Formula): AppliedPositionTactic
Applied at a fixed position, ensuring that the formula
expectedwill be found at that position, verbatim.Applied at a fixed position, ensuring that the formula
expectedwill be found at that position, verbatim.- seqIdx
The position where this tactic will be applied at (-1 based for antecedent, 1 based for succedent).
- expected
the formula expected at
position. Contract fails if that expectation is not met.- returns
The tactic of type
Tthat can be readily applied at the specified position to any given BelleExpr.
- Definition Classes
- AtPosition
- Note
Convenience wrapper
- See also
PositionLocator)
-
final
def
apply(position: Position, expected: Formula): AppliedPositionTactic
Applied at a fixed position, ensuring that the formula
expectedwill be found at that position, verbatim.Applied at a fixed position, ensuring that the formula
expectedwill be found at that position, verbatim.- position
The position where this tactic will be applied at.
- expected
the formula expected at
position. Contract fails if that expectation is not met.- returns
The tactic of type
Tthat can be readily applied at the specified position to any given BelleExpr.
- Definition Classes
- AtPosition
- Note
Convenience wrapper
- See also
PositionLocator)
-
final
def
apply(position: Position): AppliedPositionTactic
Applied at a fixed position.
Applied at a fixed position.
- position
The position where this tactic will be applied at.
- returns
The tactic of type
Tthat can be readily applied at the specified position to any given BelleExpr.
- Definition Classes
- AtPosition
- Note
Convenience wrapper
- See also
PositionLocator)
-
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) ⇒ PositionLocator): (A) ⇒ AppliedPositionTactic
- Definition Classes
- Function1
- Annotations
- @unspecialized()
-
final
def
computeResult(provable: ProvableSig, position: Position): ProvableSig
- Definition Classes
- LeftTactic → PositionalTactic
- Annotations
- @throws( ... )
- Note
this should be called from within interpreters, but not by end-users
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- 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
getLocation: Location
Get the location where this tactic stems from.
Get the location where this tactic stems from.
- Definition Classes
- BelleExpr
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
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
setLocation(newLocation: Location): Unit
- Definition Classes
- BelleExpr
- Note
location is private so that it's not something that effects case class quality, and mutable so that it can be ignored when building up custom tactics.
-
def
switch(children: (BelleLabel, BelleExpr)*): BelleExpr
- Definition Classes
- BelleExpr
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- Function1 → AnyRef → Any
-
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( ... )
-
def
|(other: BelleExpr): BelleExpr
this | other: alternative composition executes other if applying this fails, failing if both fail.
this | other: alternative composition executes other if applying this fails, failing if both fail.
- Definition Classes
- BelleExpr
-
def
|!(other: BelleExpr): BelleExpr
this |! other: alternative composition executes other if applying this fails (even critically), failing if both fail.
this |! other: alternative composition executes other if applying this fails (even critically), failing if both fail.
- Definition Classes
- BelleExpr
-
def
||(other: BelleExpr): BelleExpr
- Definition Classes
- BelleExpr
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