package bellerophon
 Alphabetic
 Public
 All
Type Members

case class
AppliedBuiltinTwoPositionTactic(positionTactic: BuiltInTwoPositionTactic, posOne: Position, posTwo: Position) extends BelleExpr with (ProvableSig) ⇒ ProvableSig 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 (ProvableSig) ⇒ ProvableSig 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).

class
BelleAbort extends BelleProofSearchControl
Raised when a tactic decides that all further tactical work on a goal is useless and bellerophon should immediately stop

abstract
class
BelleBaseInterpreter extends Interpreter with Logging
Sequential interpreter for Bellerophon tactic expressions.

case class
BelleCEX(message: String, cex: Map[NamedSymbol, Expression], s: Sequent) extends BelleProofSearchControl with Product with Serializable
Raised when counterexamples are found in sequent
s
;cex
contains counterexample values per named symbol.  sealed trait BelleContext extends (Map[BelleDot, BelleExpr]) ⇒ BelleExpr

abstract
class
BelleCriticalException extends BelleThrowable
Reported bug: Major syntactic and semantic errors in bellerophon tactics that indicate a tactic is broken.
Reported bug: Major syntactic and semantic errors in bellerophon tactics that indicate a tactic is broken. For example, forgetting to provide an expected position or applying a left tactic on the right. BelleInterpreter will raise the error to the user's attention but it needs an internal fix to KeYmaera X.

class
BelleDelayedSubstProvable extends BelleProvable
A Provable that was produced with a delayed substitution
subst
. 
class
BelleDot extends BelleExpr
⎵: Placeholder for tactics in tactic contexts.
⎵: Placeholder for tactics in tactic contexts. Reserved tactic expression that cannot be executed.

sealed 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. All Bellerophon tactic expressions are of type edu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr, which provides the following tactic combinators
s ; t
aliass & t
sequential composition executes ton the output of
s, 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.
 To do
Consolidate the members of BelleExpr and finalize an abstract syntax.
 See also
Table 1 of Bellerophon: A Typed Language for Automated Deduction in a Uniform Substitution Calculus. In Mauricio AyalaRincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207224. Springer, 2017.

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

case class
BelleLabelTx(r: BelleLabel, c: Option[BelleLabel], label: String = "") extends BelleLabel with Product with Serializable
Label transaction with rollback point
r
and collected labelsc
since rollback point. 
class
BelleNoProgress extends BelleProofSearchControl
Raised when a tactic wants to indicate that it is/was not able to make progress on the goal.

abstract
class
BelleProofSearchControl extends BelleThrowable
Search control: Silently raises issues to control proof search, indicating that one proof attempt did not succeed so other proof options should be tried.
Search control: Silently raises issues to control proof search, indicating that one proof attempt did not succeed so other proof options should be tried. They will be swallowed by any outer proof search tactics that will try something else instead. For example, trying to apply an implyR tactic at a succedent position that contains an Or will be inapplicable but does not indicate a bug in the tactic, merely that a different branch needs to be taken in proof search.

case class
BelleProvable(p: ProvableSig, label: Option[List[BelleLabel]]) 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

abstract
class
BelleTacticFailure extends BelleProofSearchControl
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.

abstract
class
BelleThrowable extends ProverException
Common exception type for all Bellerophon tactic problems and exceptions.
Common exception type for all Bellerophon tactic problems and exceptions. Tactic exceptions come on three different kinds:
 BelleCriticalException indicates an internal bug in a tactic implementation, such as applying left rules on the right. They will be reported but need a KeYmaera X implementation change to fix. 2. BelleUserCorrectableException indicates that the user has provided an unsuitable input problem or made a correctable error in a proof step. They will be reported back to the user along with a legible message describing what needs to be changed in the problem or proof. 3. BelleProofSearchControl indicates that one proof attempt did not succeed so other proof options should be tried. They will be swallowed by any outer proof search tactics that will try something else instead. Some advanced proof search tactics may "convert" between these exception types or swallow more of them when they deliberately try steps they know may fail spectacularly but have a backup plan.

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

class
BelleUnexpectedProofStateError extends BelleCriticalException
Signals an unexpected proof state (e.g., an open goal that should have been closed).

case class
BelleUnfinished(message: String, p: Provable) extends BelleProofSearchControl with Product with Serializable
Raised when provable
p
is not yet proved. 
abstract
class
BelleUserCorrectableException extends BelleThrowable
User feedback: Indicates that the user has provided an unsuitable input problem or made a correctable error in a proof step.
User feedback: Indicates that the user has provided an unsuitable input problem or made a correctable error in a proof step. They will be reported back to the user along with a legible message describing what needs to be changed in the problem or proof.

trait
BelleValue extends AnyRef
Bellerophon expressions that are values, so should not be evaluated any further since irreducible.

case class
BranchTactic(children: Seq[BelleExpr]) extends BelleExpr with Product with Serializable
<(e1,...,en)
branching to run tacticei
on branchi
, failing if any of them fail or if there are not exactlyn
branches. 
abstract
case class
BuiltInLeftTactic(name: String) extends BelleExpr with LeftTactic 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 RightTactic 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 (ProvableSig) ⇒ ProvableSig with Product with Serializable
 abstract case class BuiltInTwoPositionTactic(name: String) extends BelleExpr with NamedBelleExpr with Product with Serializable

class
Cancellable[T] extends AnyRef
Cancellable future, @see https://stackoverflow.com/questions/16009837/howtocancelfutureinscala

case class
CaseTactic(children: Seq[(BelleLabel, BelleExpr)]) extends BelleExpr with Product with Serializable
<("l1":e1,...,"ln":en)
branching to run tacticei
on labelli
, failing if any of them fail, if there are not exactlyn
branches, or if any of the labels does not exist. 
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
CompoundCriticalException extends BelleCriticalException
A Bellerophon critical exception that consists of two reasons why it is being raised, for example, if two things went wrong out of which it would have sufficed if only one succeeds.

class
CompoundProofSearchException extends BelleProofSearchControl
A Bellerophon proof search exception that consists of two reasons why it is being raised, for example, if two things went wrong out of which it would have sufficed if only one succeeds.

case class
ConcurrentInterpreter(listeners: Seq[IOListener] = Nil, throwWithDebugInfo: Boolean = false) extends BelleBaseInterpreter with Logging with Product with Serializable
Concurrent interpreter that runs parallel tactics concurrently.

abstract
case class
CoreLeftTactic(name: String) extends BelleExpr with LeftTactic with NamedBelleExpr with Product with Serializable
Builtin position tactics coming from the core that are to be applied on the left.
Builtin position tactics coming from the core that are to be applied on the left. Unlike BuiltInLeftTactic, wraps MatchError from the core in readable errors.
 See also

abstract
case class
CoreRightTactic(name: String) extends BelleExpr with RightTactic with NamedBelleExpr with Product with Serializable
Builtin position tactics coming from the core that are to be applied on the right Unlike BuiltInRightTactic, wraps MatchError from the core in readable errors.
Builtin position tactics coming from the core that are to be applied on the right Unlike BuiltInRightTactic, wraps MatchError from the core in readable errors.
 See also

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
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 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.
 case class EitherTactic(alts: Seq[BelleExpr]) extends BelleExpr with Product with Serializable
 trait ExecutionContext extends AnyRef

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

case class
Find(goal: Int, shape: Option[Expression], start: Position, exact: Boolean, defs: Declaration) 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.

trait
IOListener extends AnyRef
Listeners for input/output results during the interpretation of Bellerophon tactic expressions.

class
IllFormedTacticApplicationException extends BelleCriticalException
Illformed ways of applying tactics, such as missing position for a position tactic or supplying a term when a formula was expected.
Illformed ways of applying tactics, such as missing position for a position tactic or supplying a term when a formula was expected. Or applying a tactic at 1 that can only applied in the succedent or vice versa. This indicates a catastrophic logical error in the whole tactic implementation.

class
InapplicableUnificationKeyFailure extends BelleTacticFailure
Tactic was unable to unify with the given key and is, thus, inapplicable as indicated in the present sequent.
Tactic was unable to unify with the given key and is, thus, inapplicable as indicated in the present sequent. Besides indicating genuine unifiable situations, this may indicate that the wrong key was chosen for the (derived) axiom in its edu.cmu.cs.ls.keymaerax.btactics.macros.AxiomInfo.

class
InfiniteTacticLoopError extends BelleCriticalException
Error indicates that a (critical) infinite tactic loop is detected indicating an implementation error.

class
InputFormatFailure extends BelleTacticFailure
Signaling that a tactic input was not as expected.
 abstract case class InputTactic(name: String, inputs: Seq[Any]) extends BelleExpr with NamedBelleExpr with Product with Serializable

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 NoOpTactic with Product with Serializable
Assign the given label
label
to the present BelleProvable. 
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(), throwWithDebugInfo: Boolean = false) extends SequentialInterpreter with Product with Serializable
Sequential interpreter that stops exploring branching on the first failing branch.

trait
LeftTactic extends BelleExpr with PositionalTactic
Tactics that can only be applied in the antecedent on the left.
Tactics that can only be applied in the antecedent on the left.
 See also
LeftRule

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)
 class MissingLyapunovFunction extends BelleUserCorrectableException

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. 
trait
NoOpTactic extends AnyRef
Marker for noop tactics.

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

case class
ParallelTactic(expr: List[BelleExpr]) extends BelleExpr with Product with Serializable
left  right
alternative composition executes bothleft
andright
simultaneously and succeeds with the first success, failing if both fail. 
case class
PartialTactic(child: BelleExpr, label: Option[BelleLabel] = None) extends BelleExpr with Product with Serializable
A partial tactic marks an unclosed proof (mainly for testing purposes to not insist on a closed proof).
A partial tactic marks an unclosed proof (mainly for testing purposes to not insist on a closed proof). To check for closed subgoals, use TactixLibrary.done.

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
ProofSearchFailure extends BelleTacticFailure
Signals a proof search failure.
Signals a proof search failure. Also thrown by calls that are not "tactics" per se but might, e.g., be called internally by a tactic May be caught internally by tactics to direct searches.

class
ProverSetupException extends BelleCriticalException
Incorrect prover setup, such as insufficient stack size or missing tools.

case class
RepeatTactic(child: BelleExpr, times: Int) extends BelleExpr with Product with Serializable
child*times
bounded repetition executeschild
tactictimes
number of times, failing if any of those repetitions fail.  case class ReplacementBelleContext(t: BelleExpr) extends BelleContext with Product with Serializable

trait
RightTactic extends BelleExpr with PositionalTactic
Tactics that can only be applied in the succedent on the right.
Tactics that can only be applied in the succedent on the right.
 See also
RightRule

case class
SaturateTactic(child: BelleExpr) extends BelleExpr with Product with Serializable
child*
saturating repetition executes tacticchild
repeatedly to a fixpoint, casting result to type annotation, diverging if no fixpoint. 
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
ProvableSig.apply(USubst)
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017. Example 32.
NoProverException
 case class SeqTactic(seq: Seq[BelleExpr]) extends BelleExpr with Product with Serializable

abstract
class
SequentialInterpreter extends BelleBaseInterpreter with Logging
Sequential interpreter that runs parallel tactics as alternatives sequentially.
 abstract class SingleGoalDependentTactic extends DependentTactic

case class
SpoonFeedingInterpreter(rootProofId: Int, startStepIndex: Int, idProvider: (ProvableSig) ⇒ Int, defs: Declaration, listenerFactory: (Int) ⇒ (String, Int, Int) ⇒ Seq[IOListener], inner: (Seq[IOListener]) ⇒ Interpreter, descend: Int, strict: Boolean, convertPending: Boolean, recordInternal: Boolean) 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

class
TacticAssertionError extends BelleCriticalException
Tactic assertions.
 class TacticComparator[T <: BelleExpr] extends AnyRef

class
TacticInapplicableFailure extends BelleTacticFailure
Tactic happens to not be applicable as indicated in the present sequent.
Tactic happens to not be applicable as indicated in the present sequent. For example, InapplicableTactic can be raised when trying to apply edu.cmu.cs.ls.keymaerax.btactics.SequentCalculus.andR at the correct position 2 in bounds on the righthand side where it turns out there is an Or formula not an And formula. This does not indicate a catastrophic failure in the tactic implementation, merely a promising but unsuccessful attempt of applying a tactic.

class
TacticRequirementError extends BelleCriticalException
Tactic requirements that failed and indicate a critical logical error in using it.

case class
TryCatch[T <: Throwable](t: BelleExpr, cCatch: Class[T], c: (T) ⇒ BelleExpr, f: Option[BelleExpr] = None) extends BelleExpr with Product with Serializable
Tries tactic
t
and executes c
(catch) on exceptions of typeT
that occur when executingt
f
(finally) on the result oft
(ift
is successful), on the result ofc
(ifc
is successful), or on the initial problem if neithert
norc
are successful (throwing the exceptions oft
orc
even iff
is successful).Tries tactic
t
and executes c
(catch) on exceptions of typeT
that occur when executingt
f
(finally) on the result oft
(ift
is successful), on the result ofc
(ifc
is successful), or on the initial problem if neithert
norc
are successful (throwing the exceptions oft
orc
even iff
is successful). Pattern: TryCatch should usually be used together with
. In that case,c
should throw a proof search control exception instead of supplying a tactic, since it is usually intended to also execute the alternative tactic on success oft
or ift
throws other unrelated proof search control exceptions.TryCatch(useAt("[:=] assign")(1), classOf[SubstitutionClashException], (ex: SubstitutionClashException) => throw new TacticInapplicableFailure("Inapplicable", ex))  alternativeTactic
If indeed an alternative tactic should only be executed on exception, use
TryCatch(useAt("[:=] assign")(1), classOf[SubstitutionClashException], (ex: SubstitutionClashException) => alternativeTactic)

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.In other words:
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.  class UnexpandedDefinitionsFailure extends BelleUserCorrectableException

class
UnificationException extends BelleCriticalException
Raised to indicate that two expressions are not unifiable in the singlesided matching sense.

class
UnprovableAnnotatedInvariant extends BelleUserCorrectableException
Signals that an annotated invariant is not provable and needs fixing.

class
UnsupportedTacticFeature extends BelleTacticFailure
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
Using(es: List[Expression], t: BelleExpr) extends BelleExpr with Product with Serializable
Positive mention of expressions
es
to use when executing tactict
. 
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
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
BelleCommitTxLabel extends BelleLabel
Commits a label transaction.
 object BelleDot extends BelleDot
 object BelleExpr

object
BelleInterpreter extends Interpreter
Provides the interpreter for running tactics.

object
BelleLabel
Conversion functions for labels from/to strings.
 object BelleProvable extends Serializable

object
BelleRollbackTxLabel extends BelleLabel
Rollback a label transaction.
 object BelleStartTxLabel extends BelleLabel
 object Cancellable

object
EitherTactic extends Serializable
left  right
alternative composition executesright
if applyingleft
fails, failing if both fail.  object Find extends Serializable
 object Fixed extends Serializable

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

object
NoOpTactic
Mixing in NoOpTactic with existing tactic instances (e.g., obtained through TacticFactory methods)
Mixing in NoOpTactic with existing tactic instances (e.g., obtained through TacticFactory methods)
 See also
https://stackoverflow.com/a/3896244
 object PositionLocator

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

object
SeqTactic extends Serializable
left ; right
sequential composition executesright
on the output ofleft
, failing if either fail.  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.
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