package bellerophon
Bellerophon tactics language framework. This package includes
All Bellerophon tactic expressions are of type edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr, which provides the following tactic combinators
s & t
sequential composition executest
on the output ofs
, failing if either fail.s  t
alternative composition executest
if applyings
fails, failing if both fail.t*
saturating repetition executes tactict
repeatedly to a fixpoint, casting result to type annotation, diverging if no fixpoint.t*n
bounded repetition executest
tacticn
number of times, failing if any of those repetitions fail.t+
saturating repetition executes tactict
to a fixpoint, requires at least one successful application.<(e1,...,en)
branching to run tacticei
on branchi
, failing if any of them fail or if there are not exactlyn
branches.case _ of {fi => ei}
uniform substitution case pattern applies the firstei
such thatfi
uniformly substitutes to current provable for whichei
does not fail, fails if theei
of all matchingfi
fail.t partial
partial tactic marker marks that tactict
is allowed to not close all its goals.
Positional tactics support flexible modes of identifying what position to apply them to via
edu.cmu.cs.ls.keymaerax.bellerophon.AtPosition.
Applying a positional tactic t
at a position supports many different ways of specifying the position:
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).
 See also
Nathan Fulton, Stefan Mitsch, Brandon Bohrer and Andre Platzer. Bellerophon: Tactical theorem proving for hybrid systems. In Mauricio AyalaRincon and Cesar Munoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS. Springer, 2017.
 Alphabetic
 By Inheritance
 bellerophon
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members
 case class AfterTactic(left: BelleExpr, right: BelleExpr) extends BelleExpr with Product with Serializable

trait
AntePosition extends Position
A position guaranteed to identify an antecedent position
A position guaranteed to identify an antecedent position
 See also
AntePos

case class
AppliedBuiltinTwoPositionTactic(positionTactic: BuiltInTwoPositionTactic, posOne: Position, posTwo: Position) extends BelleExpr with Product with Serializable
Motivation is similar to AppliedPositionTactic, but for BuiltInTwoPositionTactic
 class AppliedDependentPositionTactic extends DependentTactic
 class AppliedDependentPositionTacticWithAppliedInput extends AppliedDependentPositionTactic

case class
AppliedPositionTactic(positionTactic: PositionalTactic, locator: PositionLocator) extends BelleExpr with Product with Serializable
Stores the position tactic and position at which the tactic was applied.
Stores the position tactic and position at which the tactic was applied. Useful for storing execution traces.

case class
ApplyDefTactic(t: DefTactic) extends BelleExpr with Product with Serializable
Applies the tactic definition
t
. 
trait
AtPosition[T <: BelleExpr] extends BelleExpr with (PositionLocator) ⇒ T with Logging
Applied at a position, AtPosition turns into a tactic of type T.
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).

trait
BaseMatcher extends Matcher
A matcher that forwards all unification functionality to BaseMatcher.unify().

class
BelleAbort extends BelleThrowable
Raised when a tactic decides that all further tactical work on a goal is useless and bellerophon should immediately stop
 sealed trait BelleContext extends (Map[BelleDot, BelleExpr]) ⇒ BelleExpr

class
BelleDot extends BelleExpr
⎵: Placeholder for tactics in tactic contexts.
⎵: Placeholder for tactics in tactic contexts. Reserved tactic expression that cannot be executed.

abstract
class
BelleExpr extends AnyRef
Algebraic Data Type whose elements are wellformed Bellephoron tactic expressions.
Algebraic Data Type whose elements are wellformed Bellephoron tactic expressions. See Table 1 of "Bellerophon: A Typed Language for Automated Deduction in a Uniform Substitution Calculus"
 To do
Consolidate the members of BelleExpr and finalize an abstract syntax.
 See also

class
BelleFriendlyUserMessage extends Exception
These exceptions have wellunderstood causes and the given explanation should be propagated all the way to the user.
These exceptions have wellunderstood causes and the given explanation should be propagated all the way to the user.
 To do
give proper formatting and inContext and such.

case class
BelleIllFormedError(message: String, cause: Throwable = null) extends BelleThrowable with Product with Serializable
Syntactic and semantic errors in bellerophon tactics, such as forgetting to provide an expected position.
Syntactic and semantic errors in bellerophon tactics, such as forgetting to provide an expected position. BelleInterpreter will raise the error to the user's attention.

trait
BelleLabel extends AnyRef
Bellerophon labels for proof branches.
Bellerophon labels for proof branches.
 See also
edu.cmu.cs.ls.keymaerax.btactics.Idioms.<()
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.label()

case class
BelleProvable(p: ProvableSig, label: Option[List[BelleLabel]] = None) extends BelleExpr with BelleValue with Product with Serializable
A Provable during a Bellerophon interpreter run, readily paired with an optional list of BelleLabels

case class
BelleSubLabel(parent: BelleLabel, label: String) extends BelleLabel with Product with Serializable
A sublabel for a BelleProvable

case class
BelleSubProof(id: Int) extends BelleValue with Product with Serializable
Internal: To communicate proof IDs of subproofs opened in the spoonfeeding interpreter in Let between requests.
Internal: To communicate proof IDs of subproofs opened in the spoonfeeding interpreter in Let between requests. NOT TO BE USED FOR ANYTHING ELSE

case class
BelleTacticFailure(message: String, cause: Throwable = null) extends BelleThrowable with Product with Serializable
Signaling that a tactic was not applicable or did not work at the current goal.
Signaling that a tactic was not applicable or did not work at the current goal. BelleTacticFailures will be consumed by the BelleInterpreter which will try something else instead.

class
BelleThrowable extends ProverException
Common exception type for all Bellerophon tactic exceptions.

case class
BelleTopLevelLabel(label: String) extends BelleLabel with Product with Serializable
A toplevel label for a BelleProvable

case class
BelleUnsupportedFailure(message: String, cause: Throwable = null) extends BelleThrowable with Product with Serializable
Signaling that a tactic's implementation was incomplete and did not work out as planned, so tactic execution might continue, but it is indicating a potential problem in the tactic's implementation.
 case class BelleUserGeneratedError(msg: String) extends BelleThrowable with Product with Serializable

trait
BelleValue extends AnyRef
Bellerophon expressions that are values.
 case class BranchTactic(children: Seq[BelleExpr]) extends BelleExpr with Product with Serializable

abstract
case class
BuiltInLeftTactic(name: String) extends BelleExpr with PositionalTactic with NamedBelleExpr with Product with Serializable
Builtin position tactics that are to be applied on the left

abstract
case class
BuiltInPositionTactic(name: String) extends BelleExpr with PositionalTactic with NamedBelleExpr with Product with Serializable
Builtin position tactics such as assertAt

abstract
case class
BuiltInRightTactic(name: String) extends BelleExpr with PositionalTactic with NamedBelleExpr with Product with Serializable
Builtin position tactics that are to be applied on the right
 abstract case class BuiltInTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable
 abstract case class BuiltInTwoPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable

case class
ChooseSome[A](options: () ⇒ Iterator[A], e: (A) ⇒ BelleExpr) extends BelleExpr with Product with Serializable
ChooseSome(options, e)(pr) proves
e(o)(pr)
after choosing some optiono
fromoptions
whose proof with tactice
succeeds after supplying argumento
toe
.ChooseSome(options, e)(pr) proves
e(o)(pr)
after choosing some optiono
fromoptions
whose proof with tactice
succeeds after supplying argumento
toe
. It's usually one of the first optionso
for whiche(o)(pr)
does not fail. Fails if no choice fromoptions
madee(o)(pr)
succeed. options
The (lazy) iterator or stream from which subsequent options
o
will be tried. e
The tactic generator
e
that will be tried with inputo
on the Provable subsequently for each of the optionso
inoptions
until one is found for whiche(o)
does not fail.
 See also
 class CompoundException extends BelleThrowable

case class
DbAtomPointer(id: Int) extends ExecutionContext with Product with Serializable
Computes IDs for atomic steps stored in the database.
Computes IDs for atomic steps stored in the database. Anticipates how the DB issues IDs.

case class
DbBranchPointer(parent: Int, branch: Int, predStep: Int, openBranchesAfterExec: List[Int] = Nil) extends ExecutionContext with Product with Serializable
Computes IDs for branching steps stored in the database.
Computes IDs for branching steps stored in the database. Anticipates how the DB issues IDs.

case class
DefExpression(exprDef: Formula) extends BelleExpr with Product with Serializable
Defines an expression (function or predicate) for later expansion.

case class
DefTactic(name: String, t: BelleExpr) extends BelleExpr with Product with Serializable
Defines a tactic for later execution.

abstract
case class
DependentPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with AtPosition[DependentTactic] with Product with Serializable
DependentPositionTactics are tactics that can be applied at positions giving dependent tactics.
DependentPositionTactics are tactics that can be applied at positions giving dependent tactics.
 See also
 abstract class DependentPositionWithAppliedInputTactic extends DependentPositionTactic

abstract
case class
DependentTactic(name: String) extends BelleExpr with NamedBelleExpr with Logging with Product with Serializable
Dependent tactics compute a tactic to apply based on their input.
Dependent tactics compute a tactic to apply based on their input. These tactics are probably not necessary very often, but are useful for idiomatic shortcuts. See e.g., AtSubgoal.
 name
The name of the tactic.
 To do
is there a short lambda abstraction notation as syntactic sugar?
 Note
similar to the ConstructionTactics in the old framework, except they should not be necessary nearly as often because BuiltIns have direct access to a Provable.

final
class
DirectUSubstAboveURen extends RenUSubst
Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
Direct implementation of: Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
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 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.
 case class EitherTactic(left: BelleExpr, right: BelleExpr) extends BelleExpr with Product with Serializable
 trait ExecutionContext extends AnyRef

case class
ExhaustiveSequentialInterpreter(listeners: Seq[IOListener] = scala.collection.immutable.Seq()) extends SequentialInterpreter with Product with Serializable
Sequential interpreter that explores branching tactics exhaustively, regardless of failure of some.

case class
ExpandDef(expr: DefExpression) extends BelleExpr with Product with Serializable
Expands a function or predicate.

case class
Find(goal: Int, shape: Option[Expression], start: Position, exact: Boolean = true) extends PositionLocator with Product with Serializable
Locates the first applicable toplevel position that matches shape (exactly or unifiably) at or after position
start
(remaining in antecedent/succedent asstart
says). 
case class
Fixed extends PositionLocator with Product with Serializable
Locates the formula at the specified fixed position.
Locates the formula at the specified fixed position. Can optionally specify the expected formula or expected shape of formula at that position as contract.

class
FreshPostUnificationMatch extends SchematicUnificationMatch
Unification/matching algorithm for fresh shapes (with builtin names such as those in axioms).
Unification/matching algorithm for fresh shapes (with builtin names such as those in axioms). Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast 1.5pass matcher gathering uncomposed unifiers with a subsequent postprocessing pass preparing for the after renaming. Note
Expects shape to have fresh names that do not occur in the input. Usually shape has all builtin names ending in underscore _ and no input is like that.

class
FreshUnificationMatch extends SchematicUnificationMatch
Unification/matching algorithm for fresh shapes (with builtin names such as those in axioms).
Unification/matching algorithm for fresh shapes (with builtin names such as those in axioms). Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast singlepass matcher. Note
Expects shape to have fresh names that do not occur in the input. Usually shape has all builtin names ending in underscore _ and no input is like that.

trait
IOListener extends AnyRef
Listeners for input/output results during the interpretation of Bellerophon tactic expressions.
 abstract case class InputTactic(name: String, inputs: Seq[Any]) extends BelleExpr with NamedBelleExpr with Product with Serializable

trait
InsistentMatcher extends Matcher
A matcher that insists on always matching as if there were arbitrary expressions as opposed to specializing to Term versus Formula etc.

trait
Interpreter extends AnyRef
Interpreter for Bellerophon tactic expressions that transforms Bellerophon values using Bellerophon tactic language expressions to ultimately produce ProvableSig.
Interpreter for Bellerophon tactic expressions that transforms Bellerophon values using Bellerophon tactic language expressions to ultimately produce ProvableSig.
Interpreter : BelleExpr * BelleValue => BelleValue
 See also
 case class LabelBranch(label: BelleLabel) extends BelleExpr with Product with Serializable
 abstract class LabelledGoalsDependentTactic extends DependentTactic with Logging

case class
LastAnte(goal: Int, inExpr: PosInExpr = PosInExpr.HereP) extends PositionLocator with Product with Serializable
'Llast Locates the last position in the antecedent.

case class
LastSucc(goal: Int, inExpr: PosInExpr = PosInExpr.HereP) extends PositionLocator with Product with Serializable
'Rlast Locates the last position in the succedent.

case class
LazySequentialInterpreter(listeners: Seq[IOListener] = scala.collection.immutable.Seq()) extends SequentialInterpreter with Product with Serializable
Sequential interpreter that stops exploring branching on the first failing branch.

case class
Let(abbr: Expression, value: Expression, inner: BelleExpr) extends BelleExpr with Product with Serializable
Let(abbr, value, inner) alias
let abbr=value in inner
abbreviatesvalue
byabbr
in the provable and proceeds with an internal proof by tacticinner
, resuming to the outer proof by a uniform substitution ofvalue
forabbr
of the resulting provable.Let(abbr, value, inner) alias
let abbr=value in inner
abbreviatesvalue
byabbr
in the provable and proceeds with an internal proof by tacticinner
, resuming to the outer proof by a uniform substitution ofvalue
forabbr
of the resulting provable. To do
generalize inner to also AtPosition[E]
 See also
ProvableSig.apply(USubst)

case class
LetInspect(abbr: Expression, instantiator: (ProvableSig) ⇒ Expression, inner: BelleExpr) extends BelleExpr with Product with Serializable
LetInspect(abbr, instantiator, inner) alias
let abbr := inspect instantiator in inner
postpones the choice for the definition ofabbr
until tacticinner
finished on the Provable, and asksinstantiator
to choose a value forabbr
based on that Provable at the end ofinner
.LetInspect(abbr, instantiator, inner) alias
let abbr := inspect instantiator in inner
postpones the choice for the definition ofabbr
until tacticinner
finished on the Provable, and asksinstantiator
to choose a value forabbr
based on that Provable at the end ofinner
. Resumes to the outer proof by a uniform substitution ofinstantiator(result)
forabbr
of the resulting provable. To do
generalize inner to also AtPosition[E]
 Note
abbr should be fresh in the Provable
 See also
ProvableSig.apply(USubst)

trait
Matcher extends (Expression, Expression) ⇒ RenUSubst with Logging
Matcher(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa.Matcher(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. 
final
case class
MultiRename(rens: Seq[(Variable, Variable)]) extends (Expression) ⇒ Expression with Product with Serializable
Uniformly rename multiple variables at once.
Uniformly rename multiple variables at once. Uniformly all occurrences of
what
andwhat'
torepl
andrepl'
and vice versa, for all (what,repl) in renames.Performs semantic renaming, i.e. leaves program constants etc. unmodified.

trait
NamedBelleExpr extends BelleExpr
A BelleExpr that has a proper code name, so is not just used internally during application.

case class
NamedTactic(name: String, tactic: BelleExpr) extends BelleExpr with NamedBelleExpr with Product with Serializable
Give a code name to the given tactic
tactic
for serialization purposes. 
case class
OnAll(e: BelleExpr) extends BelleExpr with Product with Serializable
OnAll(e)(BelleProvable(p)) == <(e, ..., e) does the same tactic on all branches where e occurs the appropriate number of times, which is
p.subgoals.length
times.OnAll(e)(BelleProvable(p)) == <(e, ..., e) does the same tactic on all branches where e occurs the appropriate number of times, which is
p.subgoals.length
times. To do
eisegesis

sealed
case class
PosInExpr(pos: List[Int] = Nil) extends Product with Serializable
Positions identify subexpressions of an expression.
Positions identify subexpressions of an expression. A position is a finite sequence of binary numbers where 0 identifies the left or only subexpression of an expression and 1 identifies the right subexpression of an expression.
import StringConverter._ val fml = "(x>2 & x+1<9) > [x:=2*x+1; y:=0;] x^2>=2".asFormula // explicitly use FormulaAugmentor print(FormulaAugmentor(fml).sub(PosInExpr(0::0::Nil))) // x>2 // implicitly use FormulaAugmentor functions on formulas import Augmentors._ print(fml.sub(PosInExpr(0::0::Nil))) // x>2; print(fml.sub(PosInExpr(0::1::Nil))) // x+1<9 print(fml.sub(PosInExpr(0::1::0::Nil))) // x+1 print(fml.sub(PosInExpr(0::1::0::0::Nil))) // x print(fml.sub(PosInExpr(0::1::0::1::Nil))) // 1 print(fml.sub(PosInExpr(0::1::1::Nil))) // 9 print(fml.sub(PosInExpr(1::1::Nil))) // x^2>=2 print(fml.sub(PosInExpr(1::0::Nil))) // x:=2*x+1; y:=0; print(fml.sub(PosInExpr(1::0::0::Nil))) // x:=2*x+1; print(fml.sub(PosInExpr(1::0::1::Nil))) // y:=0; print(fml.sub(PosInExpr(1::0::0::1::Nil))) // 2*x+1
 See also
edu.cmu.cs.ls.keymaerax.btactics.Context.splitPos()
edu.cmu.cs.ls.keymaerax.btactics.Context.replaceAt()
edu.cmu.cs.ls.keymaerax.btactics.Context.at()
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.positionOf()
Example: 
sealed
trait
Position extends AnyRef
Position at which formula and subexpresion ofa a sequent to apply a tactic.
Position at which formula and subexpresion ofa a sequent to apply a tactic.
 To do
Position should essentially become a nice typepreserving name for a pair of a SeqPos and a PosInExpr.
use AntePos and SuccPos directly instead of index etc.
 See also

sealed
trait
PositionLocator extends AnyRef
Position locators identify a position directly or indirectly in a sequent.
Position locators identify a position directly or indirectly in a sequent.
 See also
AtPosition.apply()

trait
PositionalTactic extends BelleExpr with AtPosition[AppliedPositionTactic]
PositionTactics are tactics that can be applied at positions giving ordinary tactics.
PositionTactics are tactics that can be applied at positions giving ordinary tactics.
 See also

class
ReflectiveExpressionBuilderExn extends Exception
Exceptions raised by the reflective expression builder on unexpected tactics/arguments.

sealed abstract
class
RenUSubst extends (Expression) ⇒ Expression
Renaming Uniform Substitution, combining URename and USubst.
Renaming Uniform Substitution, combining URename and USubst. Liberal list of SubstitutionPair represented as merely a list of Pair, where the
Variable~>Variable
replacements are by uniform renaming, and the other replacements are by uniform substitution. See also
edu.cmu.cs.ls.keymaerax.btactics.Augmentors.ProgramAugmentor.~>()
edu.cmu.cs.ls.keymaerax.btactics.Augmentors.FormulaAugmentor.~>()
edu.cmu.cs.ls.keymaerax.btactics.Augmentors.TermAugmentor.~>()
 case class RepeatTactic(child: BelleExpr, times: Int) extends BelleExpr with Product with Serializable
 case class ReplacementBelleContext(t: BelleExpr) extends BelleContext with Product with Serializable
 case class SaturateTactic(child: BelleExpr) extends BelleExpr with Product with Serializable

abstract
class
SchematicUnificationMatch extends BaseMatcher
Generic schematic unification/matching algorithm for tactics.
Generic schematic unification/matching algorithm for tactics. Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast singlepass matcher. Defined by recursive unification from compositions. 
case class
SearchAndRescueAgain(abbr: Seq[Expression], common: BelleExpr, instantiator: (ProvableSig, ProverException) ⇒ Seq[Expression], continuation: BelleExpr) extends BelleExpr with Product with Serializable
SearchAndRescue(abbr, common, instantiator, continuation) alias
search abbr := after common among instantiator in continuation
postpones the choice for the definition ofabbr
until tacticcommon
finished on the Provable, but then searches for the definition ofabbr
by trying to runcontinuation
from the outcome ofcommon
untilcontinuation
is successful.SearchAndRescue(abbr, common, instantiator, continuation) alias
search abbr := after common among instantiator in continuation
postpones the choice for the definition ofabbr
until tacticcommon
finished on the Provable, but then searches for the definition ofabbr
by trying to runcontinuation
from the outcome ofcommon
untilcontinuation
is successful. Each time it asksinstantiator
to choose a value forabbr
based on the same Provable at the end ofcommon
in addition to the present ProverException obtained after the current attempt of runningcontinuation
with the last choice forabbr
. Resumes to the outer proof by a uniform substitution of instantiator(result)for
abbrof the resulting provable which corresponds to having run
USubst(abbr,inst){ common } ; continuation. Thus, the logical effect is identical to directly running
instUSubst(abbr,inst){ common } ; continuation
but the operational effect differs by the above search to find the instantiationin the first place.
 abbr
the abbreviation to instantie, which should be fresh in the Provable
 See also
NoProverException
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017. Example 32.
ProvableSig.apply(USubst)
 case class SeqTactic(left: BelleExpr, right: BelleExpr) extends BelleExpr with Product with Serializable

abstract
class
SequentialInterpreter extends Interpreter with Logging
Sequential interpreter for Bellerophon tactic expressions.
 abstract class SingleGoalDependentTactic extends DependentTactic

case class
SpoonFeedingInterpreter(rootProofId: Int, startStepIndex: Int, idProvider: (ProvableSig) ⇒ Int, listenerFactory: (Int) ⇒ (String, Int, Int) ⇒ Seq[IOListener], inner: (Seq[IOListener]) ⇒ Interpreter, descend: Int = 0, strict: Boolean = true) extends Interpreter with Logging with Product with Serializable
Sequential interpreter for Bellerophon tactic expressions: breaks apart combinators and spoonfeeds "atomic" tactics to another interpreter.
Sequential interpreter for Bellerophon tactic expressions: breaks apart combinators and spoonfeeds "atomic" tactics to another interpreter.
 rootProofId
The ID of the proof this interpreter is working on.
 startStepIndex
The index in the proof trace where the interpreter starts appending steps (1 for none, e.g., in a fresh proof).
 idProvider
Provides IDs for child provables created in this interpreter.
 listenerFactory
Creates listener that are notified from the inner interpreter, takes (tactic name, parent step index in trace, branch).
 inner
Processes atomic tactics.
 descend
How far to descend into depending tactics (default: do not descend)
 strict
If true, follow tactic strictly; otherwise perform some optimizations (e.g., do not execute nil).
 abstract class StringInputTactic extends BuiltInTactic

trait
SuccPosition extends Position
A position guaranteed to identify a succedent position
A position guaranteed to identify a succedent position
 See also
SuccPos
 class TacticComparator[T <: BelleExpr] extends AnyRef

trait
TopAntePosition extends AntePosition with TopPosition
A toplevel anteedent position

trait
TopPosition extends Position
A position guaranteed to identify a toplevel position

trait
TopSuccPosition extends SuccPosition with TopPosition
A toplevel succedent position

final
class
USubstAboveURen extends RenUSubst
Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
Renaming Uniform Substitution that, in Sequent direction, first runs a uniform renaming and on the result subsequently the uniform substituion.
s(RG)  s(RD)  USubst RG  RD  URen G  D
 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.

case class
USubstPatternTactic(options: Seq[(BelleType, (RenUSubst) ⇒ BelleExpr)]) extends BelleExpr with Product with Serializable
USubstPatternTactic((form1, us=>t1) :: ...
USubstPatternTactic((form1, us=>t1) :: ... (form2, us=>t2) :: Nil) runs the first tactic
ti
for the unificationus
with the first patternformi
that matches the current goal. 
final
case class
USubstRen(subsDefsInput: Seq[(Expression, Expression)]) extends (Expression) ⇒ Expression with Product with Serializable
Renaming Uniform Substitution, simultaneously combining URename and USubst.
Renaming Uniform Substitution, simultaneously combining URename and USubst. Liberal list of SubstitutionPair represented as merely a list of Pair, where the Variable~>Variable replacements are by uniform renaming, and the other replacements are by uniform substitution, simultaneously.
 Note
This implementation performs semantic renaming.
 See also
 case class UnificationException(e1: String, e2: String, info: String = "") extends BelleThrowable with Product with Serializable

class
UnificationMatchBase extends SchematicUnificationMatch
Generic base for unification/matching algorithm for tactics.
Generic base for unification/matching algorithm for tactics. Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape. Reasonably fast singlepass matcher. 
class
UnificationMatchURenAboveUSubst extends Matcher
Unification/matching algorithm for tactics for URenAboveUSubst.
Unification/matching algorithm for tactics for URenAboveUSubst. Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape.  class UnificationMatchUSubstAboveURen extends Matcher

case class
AppliedDependentTwoPositionTactic(t: DependentTwoPositionTactic, p1: Position, p2: Position) extends BelleExpr with Product with Serializable
 Annotations
 @deprecated
 Deprecated

trait
BelleType extends AnyRef
 Annotations
 @deprecated
 Deprecated
remove
 To do
eisegesis  simple types

abstract
case class
DependentTwoPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable
 Annotations
 @deprecated
 Deprecated

case class
PartialTactic(child: BelleExpr, label: Option[BelleLabel] = None) extends BelleExpr with Product with Serializable
A partial tactic is allowed to leave its subgoals around as unproved
A partial tactic is allowed to leave its subgoals around as unproved
 Annotations
 @deprecated
 Deprecated
(Since version 4.2) Replace with something else  either assertProved or some sort of branch indicator?

case class
ProveAs(lemmaName: String, f: Formula, e: BelleExpr) extends BelleExpr with Product with Serializable
 Annotations
 @deprecated
 Deprecated
(Since version 4.2) Does not work with useAt, which was the only point. There's also no way to print/parse ProveAs correctly, and scoping is global. So ProveAs should be replaced with something more systematic.

case class
SequentType(s: Sequent) extends BelleType with Product with Serializable
 Annotations
 @deprecated
 Deprecated
remove
 To do
Added because SequentTypes are needed for unification tactics.

case class
TheType() extends BelleType with Product with Serializable
 Annotations
 @deprecated
 Deprecated
remove
Value Members
 object AntePosition
 object BelleDot extends BelleDot
 object BelleExpr

object
BelleInterpreter extends Interpreter
Provides the interpreter for running tactics.
 object Find extends Serializable
 object Fixed extends Serializable

object
IOListeners
Some tactic listeners.
Some tactic listeners. Created by smitsch on 9/3/17.

object
NonSubstUnificationMatch extends FreshUnificationMatch
Unify any term for variables in ODEs.
 object PosInExpr extends Serializable
 object Position

object
ReflectiveExpressionBuilder extends Logging
Constructs a edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr from a tactic name
 object RenUSubst
 object SuccPosition
 object TacticComparator

object
TacticDiff
Computes a diff.
Computes a diff. (C,d1,d2) of two tactics t1 and t2 such that C(d1)=t1 and C(d2)=t2.

object
TacticStatistics
Computes tactic statistics (e.g., size).

object
UIIndex
UserInterface Axiom/Tactic Index: Indexing data structure for all canonically applicable (derived) axioms/rules/tactics in UserInterface.
UserInterface Axiom/Tactic Index: Indexing data structure for all canonically applicable (derived) axioms/rules/tactics in UserInterface.
 object USubstRen extends Serializable

object
UnificationMatch extends FreshUnificationMatch
Unification/matching algorithm for tactics.
Unification/matching algorithm for tactics. Unify(shape, input) matches second argument
input
against the patternshape
of the first argument but not vice versa. Matcher leaves input alone and only substitutes into shape.
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 structuresedu.cmu.cs.ls.keymaerax.core.Expression
 Differential dynamic logic expressionsedu.cmu.cs.ls.keymaerax.core.Sequent
 Sequents of formulasedu.cmu.cs.ls.keymaerax.core.Rule
 Proof rulesedu.cmu.cs.ls.keymaerax.core.Provable
 Proof certificateedu.cmu.cs.ls.keymaerax.btactics
 Tactic language libraryedu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
 Main tactic libraryedu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicedu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
 Sequent Calculus for propositional and firstorder logicedu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus
 Unificationbased Uniform Substitution Calculusedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreteredu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr
 Tactic language expressionsedu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
 Sequential tactic interpreteredu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
 Parser for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter
 Pretty printer for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser
 Parser for KeYmaera X problem files.kyx
edu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismedu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB
 Lemma database stored in filesedu.cmu.cs.ls.keymaerax.tools
 Arithmetic backendsedu.cmu.cs.ls.keymaerax.tools.Mathematica
 Mathematica interface for real arithmetic and ODE solver etc.edu.cmu.cs.ls.keymaerax.tools.Z3
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.Polya
 Polya interface for real arithmetic.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.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.References
Full references are provided elsewhere 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, LNCS. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.