trait AtPosition[T <: BelleExpr] extends BelleExpr with (PositionLocator) ⇒ T with Logging
Applied at a position, AtPosition turns into a tactic of type T. Turns a position or position locator into a tactic. That is, an AtPosition[T] tactic is essentially a function of type
Position => T
but one that also supports indirect positioning via position locators that merely identify positions
PositionLocator => T
An AtPosition tactic t
supports direct positions and indirect position locators.
t(1)
applied at the first succedent formula.t(1)
applied at the first antecedent formula.t(4, 0::1::1::Nil)
applied at subexpression positioned at.0.1.1
of the fourth antecedent formula, that is at the second child of the second child of the first child of the fourth antecedent formula in the sequent.t('L)
applied at the first applicable position in the antecedent (left side of the sequent).t('R)
applied at the first applicable position in the succedent (right side of the sequent).t('_)
applied at the first applicable position in the side of the sequent to which tactict
applies. The side of the sequent is uniquely determined by type of tactic.t('Llast)
applied at the last antecedent position (left side of the sequent).t('Rlast)
applied at the last succedent position (right side of the sequent).
In addition, the formulas expected or sought for at the respective positions identified by the locators can be provided, which is useful for tactic contract and tactic documentation purposes. It is also useful for finding a corresponding formula by pattern matching.
t(2, fml)
applied at the second succedent formula, ensuring that the formulafml
is at that position.t(2, fml)
applied at the second antecedent formula, ensuring that the formulafml
is at that position.t(5, 0::1::1::Nil, ex)
applied at subexpression positioned at.0.1.1
of the fifth succedent formula, that is at the second child of the second child of the first child of the fifth succcedent formula in the sequent, ensuring that the expressionex
is at that position.t('L, fml)
applied at the antecedent position (left side of the sequent) where the expected formulafml
can be found (on the top level).t('R, fml)
applied at the succedent position (right side of the sequent) where the expected formulafml
can be found (on the top level).t('_, fml)
applied at the suitable position (uniquely determined by type of tactic) where the expected formulafml
can be found (on the top level).
 Alphabetic
 By Inheritance
 AtPosition
 Logging
 LazyLogging
 LoggerHolder
 Function1
 BelleExpr
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Abstract Value Members

abstract
def
apply(locator: PositionLocator): T
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
T
that can be readily applied at the position identified bylocator
to any given BelleExpr.
 Definition Classes
 AtPosition → Function1
 See also

abstract
def
prettyString: String
prettyprinted form of this Bellerophon tactic expression
prettyprinted 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
times
number of times, failing if any of those repetitions fail.this*n: bounded repetition executes this tactic to
times
number of times, failing if any of those repetitions fail. Definition Classes
 BelleExpr

def
<(children: BelleExpr*): BelleExpr
<(e1,...,en): branching to run tactic
ei
on branchi
, failing if any of them fail or if there are not exactlyn
branches.<(e1,...,en): branching to run tactic
ei
on branchi
, failing if any of them fail or if there are not exactlyn
branches. 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: (T) ⇒ A): (PositionLocator) ⇒ A
 Definition Classes
 Function1
 Annotations
 @unspecialized()
 final def apply(locator: Symbol, expected: Expression): T

final
def
apply(locator: Symbol, expected: Expression, defs: Declaration): T
Returns the tactic at the position identified by
locator
, ensuring thatlocator
will yield the formulaexpected
verbatim.Returns the tactic at the position identified by
locator
, ensuring thatlocator
will yield the formulaexpected
verbatim. 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
locator
identifies. Contract fails if that expectation is not met.
 Note
Convenience wrapper
 See also
apply()
 final def apply(locator: Symbol): T

final
def
apply(locator: Symbol, inExpr: PosInExpr): T
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).
 Note
Convenience wrapper
 See also
PositionLocator)
 final def apply(seqIdx: Int, inExpr: PosInExpr): T

final
def
apply(seqIdx: Int, inExpr: List[Int] = Nil): T
Applied at a fixed position in (signed) sequent position
seqIdx
at subexpressioninExpr
.Applied at a fixed position in (signed) sequent position
seqIdx
at 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
T
that can be readily applied at the specified position to any given BelleExpr.
 Note
Convenience wrapper
 See also
PosInExpr
Position)
 final def apply(seqIdx: Int, inExpr: PosInExpr, expected: Formula): T

final
def
apply(seqIdx: Int, inExpr: List[Int], expected: Formula): T
Applied at a fixed position, ensuring that the formula
expected
will be found at that position, verbatim.Applied at a fixed position, ensuring that the formula
expected
will 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
T
that can be readily applied at the specified position to any given BelleExpr.
 Note
Convenience wrapper
 See also
PositionLocator)

final
def
apply(seqIdx: Int, expected: Formula): T
Applied at a fixed position, ensuring that the formula
expected
will be found at that position, verbatim.Applied at a fixed position, ensuring that the formula
expected
will 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
T
that can be readily applied at the specified position to any given BelleExpr.
 Note
Convenience wrapper
 See also
PositionLocator)

final
def
apply(position: Position, expected: Formula): T
Applied at a fixed position, ensuring that the formula
expected
will be found at that position, verbatim.Applied at a fixed position, ensuring that the formula
expected
will 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
T
that can be readily applied at the specified position to any given BelleExpr.
 Note
Convenience wrapper
 See also
PositionLocator)

final
def
apply(position: Position): T
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
T
that can be readily applied at the specified position to any given BelleExpr.
 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) ⇒ T
 Definition Classes
 Function1
 Annotations
 @unspecialized()

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
,Program
Sequent
 Sequents of formulasProvable
 Proof certificates transformed by rules/axiomsRule
 Proof rules as well asUSubstOne
for (onepass) 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 firstorder logicHybridProgramCalculus
 Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
 Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
 Unificationbased 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 backend solversMathematicaQETool
 Mathematica interface for real arithmetic.Z3QETool
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
 Extended backends 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
 Commandline launcher for KeYmaera X supports commandline argumenthelp
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
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface 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. 219265, 2017.
2. Nathan Fulton, Stefan Mitsch, JanDavid 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. 527538. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018. Videos