package btactics
Tactic library in the Bellerophon tactic language.
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
Main tactic library consisting of: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
 Tactic tools
 AxiomIndex]: Axiom Indexing data structures for canonical proof strategies.
 DerivationInfo: Metainformation for derivation steps such as axioms for user interface etc.
All tactics are implemented in the Bellerophon tactic language, including its dependent tactics, which ultimately produce edu.cmu.cs.ls.keymaerax.core.Provable proof certificates by the Bellerophon interpreter. The Provables that tactics produce can be extracted, for example, with edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.proveBy().
Proof Styles
KeYmaera X supports many different proof styles, including flexible combinations of the following styles:
 Explicit proof certificates directly program the proof rules from the core.
2. Explicit proofs use tactics to describe a proof directly mentioning all or most proof steps.
3. Proof by search relies mainly on proof search with occasional additional guidance.
4. Proof by pointing points out facts and where to use them.
5. Proof by congruence is based on equivalence or equality or implicational rewriting within a context.
6. Proof by chase is based on chasing away operators at an indicated position.
Explicit Proof Certificates
The most explicit types of proofs can be constructed directly using the edu.cmu.cs.ls.keymaerax.core.Provable certificates in KeYmaera X's kernel without using any tactics. Also see edu.cmu.cs.ls.keymaerax.core.
import edu.cmu.cs.ls.keymaerax.core._ // explicit proof certificate construction of  !!p() <> p() val proof = (Provable.startProof( Sequent(IndexedSeq(), IndexedSeq("!!p() <> p()".asFormula))) (EquivRight(SuccPos(0)), 0) // right branch (NotRight(SuccPos(0)), 1) (NotLeft(AntePos(1)), 1) (Close(AntePos(0),SuccPos(0)), 1) // left branch (NotLeft(AntePos(0)), 0) (NotRight(SuccPos(1)), 0) (Close(AntePos(0),SuccPos(0)), 0) )
Explicit Proofs
Explicit proofs construct similarly explicit proof steps, just with explicit tactics from TactixLibrary: The only actual difference is the order of the branches, which is fixed to be from left to right in tactic branching. Tactics also use more elegant signed integers to refer to antecedent positions (negative) or succedent positions (positive).
import TactixLibrary._ // Explicit proof tactic for  !!p() <> p() val proof = TactixLibrary.proveBy("!!p() <> p()".asFormula, equivR(1) & <( (notL(1) & notR(2) & closeId) , (notR(1) & notL(2) & closeId) ) )
Proof by Search
Proof by search primarily relies on proof search procedures to conduct a proof. That gives very short proofs but, of course, they are not always entirely informative about how the proof worked. It is easiest to see in simple situations where propositional logic proof search will find a proof but works well in more general situations, too.
import TactixLibrary._ // Proof by search of  (p() & q()) & r() <> p() & (q() & r()) val proof = TactixLibrary.proveBy("(p() & q()) & r() <> p() & (q() & r())".asFormula, prop )
Common tactics for proof by search include edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.prop(), edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.master() and the like.
Proof by Pointing
Proof by pointing emphasizes the facts to use and is implicit about the details on how to use them exactly. Proof by pointing works by pointing to a position in the sequent and using a given fact at that position. For example, for proving
⟨v:=2*v+1;⟩v!=0 <> 2*v+1!=0
it is enough to point to the highlighted position
using the "<> diamond" axiom fact
![a;]!p() <> ⟨a;⟩p()
at the highlighted position to reduce the proof to a proof of
![v:=2*v+1;]!(v!=0) <> 2*v+1!=0
which is, in turn, easy to prove by pointing to the highlighted position using the "[:=] assign" axiom
[x:=t();]p(x) <> p(t())
at the highlighted position to reduce the proof to
!!(2*v+1!=0) <> 2*v+1!=0
Finally, using double negation !!p() <> p()
at the highlighted position yields the following
2*v+1!=0 <> 2*v+1!=0
which easily proves by reflexivity p() <> p()
.
Proof by pointing matches the highlighted position against the highlighted position in the fact and does what it takes to use that knowledge. There are multiple variations of proof by pointing in edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.useAt and edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.byUS, which are also imported into edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary. The above proof by pointing implements directly in KeYmaera X:
import TactixLibrary._ // Proof by pointing of  <v:=2*v+1;>v!=0 <> 2*v+1!=0 val proof = TactixLibrary.proveBy("<v:=2*v+1;>q(v) <> q(2*v+1)".asFormula, // use "<> diamond" axiom backwards at the indicated position on //  __<v:=2*v+1;>q(v)__ <> q(2*v+1) useExpansionAt("<> diamond")(1, 0::Nil) & // use "[:=] assign" axiom forward at the indicated position on //  !__[v:=2*v+1;]!q(v)__ <> q(2*v+1) useAt("[:=] assign")(1, 0::0::Nil) & // use double negation at the indicated position on //  __!!q(2*v+1)__ <> q(2*v+1) useAt("!! double negation")(1, 0::Nil) & // close by (an instance of) reflexivity  p() <> p() //  q(2*v+1) <> q(2*v+1) byUS("<> reflexive") )
Another example is:
import TactixLibrary._ // Proof by pointing of  <a;++b;>p(x) <> (<a;>p(x)  <b;>p(x)) val proof = TactixLibrary.proveBy("<a;++b;>p(x) <> (<a;>p(x)  <b;>p(x))".asFormula, // use "<> diamond" axiom backwards at the indicated position on //  __<a;++b;>p(x)__ <> <a;>p(x)  <b;>p(x) useExpansionAt("<> diamond")(1, 0::Nil) & // use "[++] choice" axiom forward at the indicated position on //  !__[a;++b;]!p(x)__ <> <a;>p(x)  <b;>p(x) useAt("[++] choice")(1, 0::0::Nil) & // use "<> diamond" axiom forward at the indicated position on //  !([a;]!p(x) & [b;]!p(x)) <> __<a;>p(x)__  <b;>p(x) useExpansionAt("<> diamond")(1, 1::0::Nil) & // use "<> diamond" axiom forward at the indicated position on //  !([a;]!p(x) & [b;]!p(x)) <> ![a;]!p(x)  __<b;>p(x)__ useExpansionAt("<> diamond")(1, 1::1::Nil) & // use propositional logic to show //  !([a;]!p(x) & [b;]!p(x)) <> ![a;]!p(x)  ![b;]!p(x) prop )
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary.stepAt also uses proof by pointing but figures out the appropriate fact to use on its own. Here's a similar proof:
import TactixLibrary._ // Proof by pointing with steps of  ⟨a++b⟩p(x) <> (⟨a⟩p(x)  ⟨b⟩p(x)) val proof = TactixLibrary.proveBy("p(x) <> (p(x)  p(x))".asFormula, // use "<> diamond" axiom backwards at the indicated position on //  __⟨a++b⟩p(x)__ <> ⟨a⟩p(x)  ⟨b⟩p(x) useExpansionAt("<> diamond")(1, 0::Nil) & //  !__[a;++b;]!p(x)__ <> ⟨a⟩p(x)  ⟨b⟩p(x) // step "[++] choice" axiom forward at the indicated position stepAt(1, 0::0::Nil) & //  __!([a;]!p(x) & [b;]!p(x))__ <> ⟨a⟩p(x)  ⟨b⟩p(x) // step deMorgan forward at the indicated position stepAt(1, 0::Nil) & //  __![a;]!p(x)__  ![b;]!p(x) <> ⟨a⟩p(x)  ⟨b⟩p(x) // step "<> diamond" forward at the indicated position stepAt(1, 0::0::Nil) & //  ⟨a⟩p(x)  __![b;]!p(x)__ <> ⟨a⟩p(x)  ⟨b⟩p(x) // step "<> diamond" forward at the indicated position stepAt(1, 0::1::Nil) & //  ⟨a⟩p(x)  ⟨b⟩p(x) <> ⟨a⟩p(x)  ⟨b⟩p(x) byUS("<> reflexive") )
Likewise, for proving
x>5  !([x:=x+1; ++ x:=0;]x>=6)  x<2
it is enough to point to the highlighted position
x>5  !([x:=x+1; ++ x:=0;]x>=6)  x<2
and using the "[++] choice" axiom fact
[a;++b;]p() <> [a;]p() & [b;]p()
to reduce the proof to a proof of
x>5  !([x:=x+1;]x>6 & [x:=0;]x>=6)  x<2
which is, in turn, easy to prove by pointing to the assignments using "[:=] assign" axioms and ultimately asking propositional logic.
More proofs by pointing are shown in edu.cmu.cs.ls.keymaerax.btactics.DerivedAxioms source code.
Proof by Congruence
Proof by congruence is based on equivalence or equality or implicational rewriting within a context. This proof style can make quite quick inferences leading to significant progress using the CE, CQ, CT congruence proof rules or combinations thereof.
import TactixLibrary._ //  x*(x+1)>=0 > [y:=0;x:=__x^2+x__;]x>=y val proof = TactixLibrary.proveBy("x*(x+1)>=0 > [y:=0;x:=x^2+x;]x>=y".asFormula, CEat(proveBy("x*(x+1)=x^2+x".asFormula, QE)) (1, 1::0::1::1::Nil) & //  x*(x+1)>=0 > [y:=0;x:=__x*(x+1)__;]x>=y by CE/CQ using x*(x+1)=x^2+x at the indicated position // step uses toplevel operator [;] stepAt(1, 1::Nil) & //  x*(x+1)>=0 > [y:=0;][x:=x*(x+1);]x>=y // step uses toplevel operator [:=] stepAt(1, 1::Nil) & //  x*(x+1)>=0 > [x:=x*(x+1);]x>=0 // step uses toplevel [:=] stepAt(1, 1::Nil) & //  x*(x+1)>=0 > x*(x+1)>=0 prop )
Proof by congruence can also make use of a fact in multiple places at once by defining an appropriate context C:
import TactixLibrary._ val C = Context("x<5 & ⎵ > [{x' = 5*x & ⎵}](⎵ & x>=1)".asFormula) //  x<5 & __x^2<4__ > [{x' = 5*x & __x^2<4__}](__x^2<4__ & x>=1) val proof = TactixLibrary.proveBy("x<5 & x^2<4 > [{x' = 5*x & x^2<4}](x^2<4 & x>=1)".asFormula, CEat(proveBy("2x^2<4" .asFormula, QE), C) (1)) ) //  x<5 & (__2[{x' = 5*x & __2 println(proof.subgoals)=1) by CE
Proof by Chase
Proof by chase chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices. The canonical examples use edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase() to chase away differential forms:
import TactixLibrary._ val proof = TactixLibrary.proveBy("[{x'=22}](2*x+x*y>=5)'".asFormula, // chase the differential prime away in the postcondition chase(1, 1 :: Nil) //  [{x'=22}]2*x'+(x'*y+x*y')>=0 ) // Remaining subgoals:  [{x'=22}]2*x'+(x'*y+x*y')>=0 println(proof.subgoals)
import TactixLibrary._ val proof = TactixLibrary.proveBy("[{x'=22}](2*x+x*y>=5)' <> [{x'=22}]2*x'+(x'*y+x*y')>=0".asFormula, // chase the differential prime away in the left postcondition chase(1, 0:: 1 :: Nil) & //  [{x'=22}]2*x'+(x'*y+x*y')>=0 <> [{x'=22}]2*x'+(x'*y+x*y')>=0 byUS("<> reflexive") )
Yet edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase() is also useful to chase away other operators, say, modalities:
import TactixLibrary._ // proof by chase of  [?x>0;x:=x+1;x:=2*x; ++ ?x=0;x:=1;]x>=1 val proof = TactixLibrary.proveBy( Sequent(IndexedSeq(), IndexedSeq("[?x>0;x:=x+1;x:=2*x; ++ ?x=0;x:=1;]x>=1".asFormula)), // chase the box in the succedent away chase(1,Nil) & //  (x>0>2*(x+1)>=1)&(x=0>1>=1) QE )
Additional Mechanisms
 Tactic framework for Hilbertstyle Forward Tactics: Tactics are functions
Provable=>Provable
 edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic: Forward Hilbertstyle tactics
Provable=>Provable
 edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardPositionTactic: Positional forward Hilbertstyle tactics
Position=>(Provable=>Provable)
 edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus: Forward Hilbertstyle tactic combinators.
 edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic: Forward Hilbertstyle tactics
 To do
Expand descriptions
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
edu.cmu.cs.ls.keymaerax.btactics.DifferentialEquationCalculus
 Alphabetic
 By Inheritance
 btactics
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

sealed
trait
ArgInfo extends AnyRef
Information on the arguments, their names and sorts, that an axiom/rule/tactic requires as input.

case class
AxiomDisplayInfo(names: SimpleDisplayInfo, displayFormula: String) extends DisplayInfo with Product with Serializable
Render an axiom with a name as a UI string for the formula.

trait
AxiomInfo extends ProvableInfo
MetaInformation for an axiom or derived axiom
MetaInformation for an axiom or derived axiom

case class
AxiomaticRuleInfo(canonicalName: String, display: DisplayInfo, codeName: String) extends ProvableInfo with Product with Serializable
Information for an axiomatic proof rule
Information for an axiomatic proof rule
 See also
edu.cmu.cs.ls.keymaerax.core.AxiomBase

class
BelleREPL extends AnyRef
Created by bbohrer on 12/19/16.

class
BuiltinInfo extends DerivationInfo
Metainformation on builtin tactic expressions (expand etc.).
 case class Case(fml: Formula, simplify: Boolean = true) extends Product with Serializable

class
ConfigurableGenerator[A] extends btactics.Generator.Generator[A]
Mapbased generator providing output according to the fixed map
products
according to its program or whole formula. 
case class
CoreAxiomInfo(canonicalName: String, display: DisplayInfo, codeName: String, linear: Boolean, expr: (Unit) ⇒ DependentPositionTactic) extends AxiomInfo with Product with Serializable
MetaInformation for an axiom from the prover core
MetaInformation for an axiom from the prover core
 See also
edu.cmu.cs.ls.keymaerax.core.AxiomBase
 class DefaultTacticIndex extends TacticIndex

sealed
trait
DerivationInfo extends AnyRef
Central metainformation on a derivation step, which is an axiom, derived axiom, proof rule, or tactic.
Central metainformation on a derivation step, which is an axiom, derived axiom, proof rule, or tactic. Provides information such as unique canonical names, internal code names, display information, etc.
Each DerivationInfo is either
 AxiomInfo consisting of builtin CoreAxiomInfo and derived axioms DerivedAxiomInfo.
 AxiomaticRuleInfo for builtin axiomatic proof rules.
 DerivedRuleInfo for derived axiomatic proof rules.
 TacticInfo for tactics and its various subtypes.
Everything consisting of a proved axiom is an AxiomInfo namely CoreAxiomInfo and DerivedAxiomInfo. Everything consisting of a Provable is a ProvableInfo, namely AxiomInfo and AxiomaticRuleInfo and DerivedRuleInfo.

case class
DerivedAxiomInfo(canonicalName: String, display: DisplayInfo, codeName: String, linear: Boolean, expr: (Unit) ⇒ DependentPositionTactic) extends AxiomInfo with StorableInfo with Product with Serializable
Information for a derived axiom proved from the core.
Information for a derived axiom proved from the core.

case class
DerivedRuleInfo(canonicalName: String, display: DisplayInfo, codeName: String, expr: (Unit) ⇒ Any) extends ProvableInfo with StorableInfo with Product with Serializable
Information for a derived rule proved from the core
Information for a derived rule proved from the core

trait
DifferentialEquationCalculus extends AnyRef
Differential Equation Calculus for differential dynamic logic.
Differential Equation Calculus for differential dynamic logic. Basic axioms for differential equations are in HilbertCalculus.
Provides the elementary derived proof rules for differential equations from Figure 11.20 and Figure 12.9 in: Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
 See also
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 1324. IEEE 2012
Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541550. IEEE 2012
edu.cmu.cs.ls.keymaerax.core.AxiomBase

sealed
trait
DisplayInfo extends AnyRef
UI display information on how to render an axiom, rule, or tactic application
 case class ExpressionArg(name: String, allowsFresh: List[String] = Nil, converter: (Expression) ⇒ Either[Expression, String] = e => Left(e)) extends ArgInfo with Product with Serializable

case class
FixedGenerator[A](list: List[A]) extends btactics.Generator.Generator[A] with Product with Serializable
Generator always providing a fixed list as output.
 case class FormulaArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable

trait
HilbertCalculus extends UnifyUSCalculus
Hilbert Calculus for differential dynamic logic.
Hilbert Calculus for differential dynamic logic.
Provides the axioms and axiomatic proof rules from Figure 2 and Figure 3 in: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981
Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 1324. IEEE 2012
Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541550. IEEE 2012
HilbertCalculus.stepAt()
HilbertCalculus.derive()
edu.cmu.cs.ls.keymaerax.core.AxiomBase

trait
HybridProgramCalculus extends AnyRef
Hybrid Program Calculus for differential dynamic logic.
Hybrid Program Calculus for differential dynamic logic. Basic axioms for hybrid programs are in HilbertCalculus.
Provides the elementary derived proof rules for hybrid programs from Figure 7.4 and Figure 12.9 in: Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
 See also
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 1324. IEEE 2012
Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541550. IEEE 2012
edu.cmu.cs.ls.keymaerax.core.AxiomBase

case class
InputAxiomDisplayInfo(names: SimpleDisplayInfo, displayFormula: String, input: List[ArgInfo]) extends DisplayInfo with Product with Serializable
Render an axiom that has a name and a UI string formula but needs a list of inputs filled in first.
 case class InputPositionTacticInfo(codeName: String, display: DisplayInfo, inputs: List[ArgInfo], expr: (Unit) ⇒ TypedFunc[_, _], needsTool: Boolean = false, needsGenerator: Boolean = false, revealInternalSteps: Boolean = false) extends TacticInfo with Product with Serializable
 case class InputTacticInfo(codeName: String, display: DisplayInfo, inputs: List[ArgInfo], expr: (Unit) ⇒ TypedFunc[_, _], needsTool: Boolean = false, needsGenerator: Boolean = false, revealInternalSteps: Boolean = false) extends TacticInfo with Product with Serializable
 case class InputTwoPositionTacticInfo(codeName: String, display: DisplayInfo, inputs: List[ArgInfo], expr: (Unit) ⇒ TypedFunc[_, _], needsTool: Boolean = false, needsGenerator: Boolean = false) extends TacticInfo with Product with Serializable
 class IntegratorODESolverTool extends Tool with ODESolverTool

trait
InvGenTool extends AnyRef
Continuous invariant generation tool.
Continuous invariant generation tool.

class
MathematicaToolProvider extends WolframToolProvider
A tool provider that initializes tools to Mathematica.

trait
ModelPlexTrait extends (List[Variable], Symbol) ⇒ (Formula) ⇒ Formula
ModelPlex: Verified runtime validation of verified cyberphysical system models.
ModelPlex: Verified runtime validation of verified cyberphysical system models.
 See also
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyberphysical system models. Formal Methods in System Design, 42 pp. 2016. Special issue for selected papers from RV'14.
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyberphysical system models. In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification  5th International Conference, RV 2014, Toronto, ON, Canada, September 2225, 2014. Proceedings, volume 8734 of LNCS, pages 199214. Springer, 2014.

class
MultiToolProvider extends PreferredToolProvider[Tool]
Combines multiple tool providers.

class
NoneToolProvider extends ToolProvider
A tool provider without tools.
 case class OptionArg(arg: ArgInfo) extends ArgInfo with Product with Serializable
 case class PositionTacticInfo(codeName: String, display: DisplayInfo, expr: (Unit) ⇒ Any, needsTool: Boolean = false, needsGenerator: Boolean = false, revealInternalSteps: Boolean = false) extends TacticInfo with Product with Serializable

class
PreferredToolProvider[T <: Tool] extends ToolProvider
A tool provider that picks appropriate special tools from the list of preferences, i.e., if multiple tools with the same trait appear in
toolPreferences
, the first will be picked for that trait. 
trait
ProvableInfo extends DerivationInfo
MetaInformation for a (derived) axiom or (derived) axiomatic rule
MetaInformation for a (derived) axiom or (derived) axiomatic rule

case class
RuleDisplayInfo(names: SimpleDisplayInfo, conclusion: SequentDisplay, premises: List[SequentDisplay]) extends DisplayInfo with Product with Serializable
Render a rule with a name as a conclusion and list of premises.

trait
SequentCalculus extends AnyRef
Sequent Calculus for propositional and firstorder logic.
Sequent Calculus for propositional and firstorder logic.
 See also
Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143189, 2008.
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.

case class
SequentDisplay(ante: List[String], succ: List[String], isClosed: Boolean = false) extends Product with Serializable
Render a sequent as a list of antecedent UI strings and a list of succedent UI strings.
Render a sequent as a list of antecedent UI strings and a list of succedent UI strings.
 isClosed
true to indicate that this sequent is closed so (*) star.

case class
SimpleDisplayInfo(name: String, asciiName: String) extends DisplayInfo with Product with Serializable
Render as a UI name and a plain text ASCII name.

trait
StorableInfo extends DerivationInfo
Storable derivation info (e.g., as lemmas).
Storable derivation info (e.g., as lemmas).
 See also
 case class StringArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
 case class SubstitutionArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
 trait TacticIndex extends AnyRef

class
TacticInfo extends DerivationInfo
Metainformation on a tactic performing a proof step (or more)

class
TaylorModelArith extends AnyRef
Taylor model arithmetic
Taylor model arithmetic
Here, a Taylor model is a data structure maintaining a proof that some term is element of the Taylor model.
 case class TermArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable

trait
ToolProvider extends AnyRef
A tool factory creates various arithmetic and simulation tools.
A tool factory creates various arithmetic and simulation tools.
 case class TwoPositionTacticInfo(codeName: String, display: DisplayInfo, expr: (Unit) ⇒ Any, needsTool: Boolean = false, needsGenerator: Boolean = false) extends TacticInfo with Product with Serializable

case class
TwoThreeTreePolynomialRing(variables: IndexedSeq[Term]) extends PolynomialRing with Product with Serializable
A polynomial is represented as a set of monomials stored in a 23 Tree, the ordering is lexicographic A monomial is represented as a coefficient and a powerproduct.
A polynomial is represented as a set of monomials stored in a 23 Tree, the ordering is lexicographic A monomial is represented as a coefficient and a powerproduct. A coefficient is represented as a pair of BigDecimals for num/denum. A power product is represented densely as a list of exponents
All datastructures maintain a proof of input term = representation of data structure as Term
Representations of data structures (recursively applied on rhs):
 3Node (l, v1, m, v2, r) is "l + v1 + m + v2 + r"
 2Node (l, v, r) is "l + v + r"
 monomial (c, pp) is "c * pp"
 coefficient (num, denum) is "num / denum"
 power product [e1, ..., en] is "x1^{e1 * ... * xn } en", where instead of "x^{0", we write "1" in order to avoid trouble with 0}0, i.e., nonzeroassumptions on x or the like
All operations on the representations update the proofs accordingly.

abstract
class
TypedFunc[A, +R] extends (A) ⇒ R
Typed functions to circumvent type erasure of arguments and return types.

trait
UnifyUSCalculus extends AnyRef
Automatic unificationbased Uniform Substitution Calculus with indexing.
Automatic unificationbased Uniform Substitution Calculus with indexing. Provides a tactic framework for automatically applying axioms and axiomatic rules by matching inputs against them by unification according to the axiom's AxiomIndex.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017. arXiv:1601.06183
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.
 case class VariableArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable

class
WolframEngineToolProvider extends WolframToolProvider
A tool provider that initializes tools to Wolfram Engine.

class
WolframScriptToolProvider extends WolframToolProvider
A tool provider that initializes tools to Wolfram Script backend.

abstract
class
WolframToolProvider extends PreferredToolProvider[Tool]
Base class for Wolfram tools with alternative names.

class
Z3ToolProvider extends PreferredToolProvider[Tool]
A tool provider that provides Z3 as QE tool and our own bundled algebra tool and diff.
A tool provider that provides Z3 as QE tool and our own bundled algebra tool and diff. solution tool, everything else is None. Initializes the Z3 installation and updates the Z3 binary on version updates.

case class
ListArg(name: String, elementSort: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
 Annotations
 @deprecated
 Deprecated
(Since version 4.2b1) Until lists are actually added to the concrete syntax of Bellerophon.
Value Members

object
AnonymousLemmas
Stores lemmas without userdefined name.

object
Approximator extends Logging
Approximations
Approximations
 To do
More Ideas:
 Allow approximations at nontoplevel.
 Preprocessing  add time var w/ t_0=0, etc.
 Postprocessing  after reducing the arithmetic, hide all approximate terms except the last one. It might even be possible to do this during the tactic by remving all but the most recent <= and >=, but I'm not sure if that's true for any/all expansions.
 Generalized tactics. Not sure this makes much sense though.
 Add an (efficient) tactic that tries to close the proof using successively longer approximations. Maybe also a tactic that looks at an entire formula and tries to deduce how far to go based on pre/postconditions and statements in discrete fragments for programs or in ev dom constraints.

object
ArithmeticLibrary
Tactics for real arithmetic.

object
ArithmeticSimplification
Tactics for simplifying arithmetic subgoals.

object
AxiomIndex extends Logging
Central Axiom Indexing data structures for canonical proof strategies, including UnifyUSCalculus.chase, UnifyUSCalculus.chaseFor() and TactixLibrary.step and TactixLibrary.stepAt.
Central Axiom Indexing data structures for canonical proof strategies, including UnifyUSCalculus.chase, UnifyUSCalculus.chaseFor() and TactixLibrary.step and TactixLibrary.stepAt.
 Note
Could be generated automatically, yet better in a precomputation fashion, not on the fly.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
edu.cmu.cs.ls.keymaerax.core.AxiomBase
edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase()
edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chaseFor()
TactixLibrary.sequentStepIndex
 object AxiomInfo

object
AxiomaticODESolver
An Axiomatic ODE solver.
An Axiomatic ODE solver. Current limitations:  No support for explicitform diamond ODEs/box ODEs in context: <{x'=0*x+1}>P, ![{x'=0*x+1}]P
 See also
Page 25 in http://arxiv.org/abs/1503.01981 for a highlevel sketch.

object
BelleLabels
Default labels used by the KeYmaera X tactics.
Default labels used by the KeYmaera X tactics. Other labels can be used by the user, but this list of labels makes it easier to match.

object
Bifurcation
Implements a bifurcationbased proof search technique for the dynamic logic of ODEs.
 object CoreAxiomInfo extends Serializable
 object DebuggingTactics

object
DerivationInfo
Central list of all derivation steps (axioms, derived axioms, proof rules, tactics) with meta information of relevant names and display names and visualizations for the user interface.
 object DerivedAxiomInfo extends Serializable

object
DerivedAxioms extends Logging
Database of Derived Axioms.
Database of Derived Axioms.
 Note
To simplify bootstrap and avoid dependency management, the proofs of the derived axioms are written with explicit reference to other scalaobjects representing provables (which will be proved on demand) as opposed to by referring to the names, which needs a map canonicalName>tacticOnDemand.
,Lemmas are lazy vals, since their proofs may need a fully setup prover with QE
,Derived axioms use the Provable facts of other derived axioms in order to avoid initialization cycles with AxiomInfo's contract checking.
 See also
edu.cmu.cs.ls.keymaerax.core.AxiomBase
 object DerivedRuleInfo extends Serializable

object
DifferentialDecisionProcedures
Decision procedures for various classes of differential equations.

object
DifferentialEquationCalculus extends DifferentialEquationCalculus
Differential Equation Calculus for differential dynamic logic.
Differential Equation Calculus for differential dynamic logic.
 See also

object
DifferentialSaturation extends Logging
Differential Saturation (Fig 6.3, Logical Analysis of Hybrid Systems) Considers a sequent of the form Gamma  [ODE & Q]p All of Gamma, Q and p are assumed to be FOL_R only Does NOT construct proofs along the way

object
FOQuantifierTactics
Implementation: FOQuantifierTactics provides tactics for instantiating quantifiers.
Implementation: FOQuantifierTactics provides tactics for instantiating quantifiers.
 Attributes
 protected

object
Generator
Invariant generator

object
HilbertCalculus extends HilbertCalculus
Hilbert Calculus for differential dynamic logic.
Hilbert Calculus for differential dynamic logic.
 See also

object
HybridProgramCalculus extends HybridProgramCalculus
Hybrid Program Calculus for differential dynamic logic.
Hybrid Program Calculus for differential dynamic logic.
 See also
 object Idioms

object
Integrator extends Logging
Solves the initial value problem for systems of differential equations.

object
IntervalArithmetic extends Logging
Tactics for introducing interval arithmetic.

object
IntervalArithmeticV2
Interval Arithmetic

object
InvariantGenerator extends Logging
Invariant generators and differential invariant generators.
Invariant generators and differential invariant generators.
 See also
Andre Platzer. A differential operator approach to equational differential invariants. In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 1315, Princeton, USA, Proceedings, volume 7406 of LNCS, pages 2848. Springer, 2012.
Andre Platzer and Edmund M. Clarke. Computing differential invariants of hybrid systems as fixedpoints. Formal Methods in System Design, 35(1), pp. 98120, 2009

object
InvariantProvers
Invariant proof automation with generators.

object
IsabelleSyntax
Tactics for converting a ModelPlex formula to Isabelle/HOL (no need for interval arithmetic)

object
Kaisar
Created by bbohrer on 12/2/16.

object
ModelPlex extends ModelPlexTrait with Logging
ModelPlex: Verified runtime validation of verified cyberphysical system models.
ModelPlex: Verified runtime validation of verified cyberphysical system models.
 See also
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyberphysical system models. Formal Methods in System Design, 42 pp. 2016. Special issue for selected papers from RV'14.
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyberphysical system models. In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification  5th International Conference, RV 2014, Toronto, ON, Canada, September 2225, 2014. Proceedings, volume 8734 of LNCS, pages 199214. Springer, 2014.

object
ODEInvariance
Implements ODE tactics based on the differential equation axiomatization.
Implements ODE tactics based on the differential equation axiomatization.
Created by yongkiat on 05/14/18.
 See also
Andre Platzer and Yong Kiam Tan. Differential equation axiomatization: The impressive power of differential ghosts. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, ACM 2018.

object
PolynomialArith extends Logging
Created by yongkiat on 11/27/16.

object
PolynomialArithV2
Polynomial Arithmetic.
Polynomial Arithmetic.
Computations are carried out fairly efficiently in a distributive representation. Computations are certifying:
 the internal data structures maintain a proof that the constructed term equals the distributive representation
The main interface is that of a PolynomialRing
 object PolynomialArithV2Helpers
 object ProvableInfo

object
RicattiEquation
Decision procedure for a single Ricatti equation.

object
RicattiSystem
Decision procedure for a system of Ricatti differential equations.

object
SequentCalculus extends SequentCalculus
Sequent Calculus for propositional and firstorder logic.
Sequent Calculus for propositional and firstorder logic.
 See also

object
Simplifier
Tactic Simplifier.simp performs term simplification everywhere within a formula, as many times as possible.
Tactic Simplifier.simp performs term simplification everywhere within a formula, as many times as possible. Simplification is parameterized over a list of simplification steps. The default set of simplifications is guaranteed to terminate (using the number of constructors in the term as a termination metric), and an optional set of rules is provided for which termination is less clear. Any set of simplifications is allowed, as long as they terminate (the termination metric need not be the number of constructors in the term). Created by bbohrer on 5/21/16.

object
SimplifierV2
Created by yongkiat on 9/29/16.

object
SimplifierV3
Note: this is meant to be a watered down version of SimplifierV2 Goals: Faster, more predictable and customizable
Note: this is meant to be a watered down version of SimplifierV2 Goals: Faster, more predictable and customizable
Given a list of rewriting axioms, this traverses a term/formula bottom up and exhaustively tries the list of axioms at each step
The rewriting axioms must have the form  t = t'  f > t = t' or similarly for formulas and <>
Created by yongkiat on 12/19/16.

object
TacticFactory
Creates tactic objects
 object TacticHelper

object
TacticIndex
Tactic indexing data structures for canonical proof strategies.
Tactic indexing data structures for canonical proof strategies.
 object TacticInfo

object
TactixLibrary extends HilbertCalculus with SequentCalculus with DifferentialEquationCalculus with HybridProgramCalculus
Tactix: Main tactic library with simple interface.
Tactix: Main tactic library with simple interface. This library features all main tactics for the most common cases.
For tactics implementing builtin rules such as sequent proof rules, elaborate documentation can be found in the prover kernel.
Main search tactics that combine numerous other tactics for automation purposes include:
 TactixLibrary.master automatic proof search
 TactixLibrary.auto automatic proof search if that successfully proves the given property
 TactixLibrary.normalize normalize to sequent normal form
 TactixLibrary.unfoldProgramNormalize normalize to sequent normal form, avoiding unnecessary branching
 TactixLibrary.prop propositional logic proving
 TactixLibrary.QE prove real arithmetic
 TactixLibrary.ODE proving properties of differential equations
 TactixLibrary.step performs one canonical simplifying proof step
 TactixLibrary.chase chase the given formula away by automatic reduction proofs
The tactic library also includes important proof calculus subcollections:
 HilbertCalculus: Hilbert Calculus for differential dynamic logic.
 SequentCalculus: Sequent Calculus for propositional and firstorder logic.
 HybridProgramCalculus: Hybrid program derived proof rules for differential dynamic logic.
 DifferentialEquationCalculus: Differential equation proof rules for differential dynamic logic.
 UnifyUSCalculus: Automatic unificationbased Uniform Substitution Calculus with indexing.
 See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219266, 2017.
Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.
Andre Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.
 object TaylorModelTactics extends Logging

object
ToolProvider extends ToolProvider with Logging
Central repository providing access to arithmetic tools.
Central repository providing access to arithmetic tools.
 Note
Never keep references to the tools, the tool provider may decide to shutdown/switch out tools and thereby render all tool references invalid.
,Do especially not keep references in singletons, the tool provider will hand out nulls until properly initialized.
 See also

object
Transitivity
Proves goals of the form a>=b,b>=c  a >= c with arbitrarily many intermediate (in)equalities.
Proves goals of the form a>=b,b>=c  a >= c with arbitrarily many intermediate (in)equalities.
These goals ought to close by QE, but often don't (e.g., when function symbols are involved).
 To do
There's a bug  this function might find the string of inequalities a >= b >= c and claim it's a proof for a>c. The fix for this bug is to check in search() that the result contains at least one strict inequalities if the goal() has form a > c.

object
TypedFunc
Creates TypedFunc implicitly, e.g., by ((x: String) => x.length): TypedFunc[String, Int]

object
UnifyUSCalculus extends UnifyUSCalculus
Automatic unificationbased Uniform Substitution Calculus with indexing.
Automatic unificationbased Uniform Substitution Calculus with indexing. Provides a tactic framework for automatically applying axioms and axiomatic rules by matching inputs against them by unification according to the axiom's AxiomIndex.
 See also
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: terms, formulas, programsSequent
 Sequents of formulasProvable
 Proof certificates transformed by rules/axiomsRule
 Proof rules as well asUSubst
for uniform substitutions and renamingStaticSemantics
 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
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.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 libraryTactixLibrary
 Main KeYmaera X tactic libraryHilbertCalculus
 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 calculiedu.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.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.edu.cmu.cs.ls.keymaerax.btactics.AxiomIndex
 Axiom indexing data structures with keys and recursors for canonical proof strategies.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.DerivedAxioms
 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