btactics

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 logic
- SequentCalculus Sequent Calculus for propositional and first-order logic
- HybridProgramCalculus Hybrid Program Calculus for differential dynamic logic
- DifferentialEquationCalculus Differential Equation Calculus for differential dynamic logic
- UnifyUSCalculus Unification-based Uniform Substitution Calculus
Tactic tools
- AxIndex]: Axiom Indexing data structures for canonical proof strategies.
- DerivationInfo: Meta-information 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(
  "!!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.auto() 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 Ax.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 Ax.assignbAxiom 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 Ax.diamond axiom backwards at the indicated position on
  // |- __<v:=2*v+1;>q(v)__ <-> q(2*v+1)
  useExpansionAt(Ax.diamond)(1, 0::Nil) &
  // use Ax.assignbAxiom axiom forward at the indicated position on
  // |- !__[v:=2*v+1;]!q(v)__ <-> q(2*v+1)
  useAt(Ax.assignbAxiom(1, 0::0::Nil) &
  // use double negation at the indicated position on
  // |- __!!q(2*v+1)__ <-> q(2*v+1)
  useAt(Ax.doubleNegation)(1, 0::Nil) &
  // close by (an instance of) reflexivity |- p() <-> p()
  // |- q(2*v+1) <-> q(2*v+1)
  byUS(Ax.equivReflexive)
)

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 Ax.diamond axiom backwards at the indicated position on
  // |- __<a;++b;>p(x)__  <->  <a;>p(x) | <b;>p(x)
  useExpansionAt(Ax.diamond)(1, 0::Nil) &
  // use Ax.choiceb axiom forward at the indicated position on
  // |- !__[a;++b;]!p(x)__  <->  <a;>p(x) | <b;>p(x)
  useAt(Ax.choiceb)(1, 0::0::Nil) &
  // use Ax.diamond axiom forward at the indicated position on
  // |- !([a;]!p(x) & [b;]!p(x))  <->  __<a;>p(x)__ | <b;>p(x)
  useExpansionAt(Ax.diamond)(1, 1::0::Nil) &
  // use Ax.diamond axiom forward at the indicated position on
  // |- !([a;]!p(x) & [b;]!p(x))  <->  ![a;]!p(x) | __<b;>p(x)__
  useExpansionAt(Ax.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 Ax.diamond axiom backwards at the indicated position on
  // |- __⟨a++b⟩p(x)__  <->  ⟨a⟩p(x) | ⟨b⟩p(x)
  useExpansionAt(Ax.diamond)(1, 0::Nil) &
  // |- !__[a;++b;]!p(x)__  <->  ⟨a⟩p(x) | ⟨b⟩p(x)
  // step Ax.choiceb 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 Ax.diamond forward at the indicated position
  stepAt(1, 0::0::Nil) &
  // |- ⟨a⟩p(x) | __![b;]!p(x)__  <-> ⟨a⟩p(x) | ⟨b⟩p(x)
  // step Ax.diamond forward at the indicated position
  stepAt(1, 0::1::Nil) &
  // |- ⟨a⟩p(x) | ⟨b⟩p(x)  <-> ⟨a⟩p(x) | ⟨b⟩p(x)
  byUS(Ax.equivReflexive)
)

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 Ax.choiceb 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 Ax.assignbAxiom axioms and ultimately asking propositional logic.

More proofs by pointing are shown in edu.cmu.cs.ls.keymaerax.btactics.Ax 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 top-level operator [;]
  stepAt(1, 1::Nil) &
  // |- x*(x+1)>=0 -> [y:=0;][x:=x*(x+1);]x>=y
  // step uses top-level operator [:=]
  stepAt(1, 1::Nil) &
  // |- x*(x+1)>=0 -> [x:=x*(x+1);]x>=0
  // step uses top-level [:=]
  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=1) by CE
println(proof.subgoals)

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(Ax.equivReflexive)
)

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(
  "[?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 Hilbert-style Forward Tactics: Tactics are functions Provable=>Provable
- edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic: Forward Hilbert-style tactics Provable=>Provable
- edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardPositionTactic: Positional forward Hilbert-style tactics Position=>(Provable=>Provable)
- edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus: Forward Hilbert-style tactic combinators.

To do: Expand descriptions
See also: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
edu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
edu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
edu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
edu.cmu.cs.ls.keymaerax.btactics.HybridProgramCalculus
edu.cmu.cs.ls.keymaerax.btactics.DifferentialEquationCalculus
edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus

Linear Supertypes

AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

btactics
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Type Members

class BelleREPL extends AnyRef
Created by bbohrer on 12/19/16.
case class Case(fml: Formula, simplify: Boolean = true) extends Product with Serializable
class ConfigurableGenerator[A] extends btactics.Generator.Generator[A]
Map-based generator providing output according to the fixed map products according to its program or whole formula.
class DefaultTacticIndex extends TacticIndex
trait Derive extends UnifyUSCalculus
Derive: provides individual differential axioms bundled as HilbertCalculus.derive.
Derive: provides individual differential axioms bundled as HilbertCalculus.derive.
There is rarely a reason to use these separate axioms, since HilbertCalculus.derive already uses the appropriate differential axiom as needed.

See also
Figure 3 in Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
HilbertCalculus.derive
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 Cyber-Physical Systems. Springer, 2018.

To do
@Tactic only partially implemented so far
See also
Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. 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 541-550. IEEE 2012
edu.cmu.cs.ls.keymaerax.core.AxiomBase
edu.cmu.cs.ls.keymaerax.btactics.Ax
TactixLibrary
case class FixedGenerator[A](list: List[A]) extends btactics.Generator.Generator[A] with Product with Serializable
Generator always providing a fixed list as output.
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. 219-266, 2017.

See also
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
Andre Platzer. Logical Foundations of Cyber-Physical 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 13-24. 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 541-550. IEEE 2012
HilbertCalculus.stepAt()
HilbertCalculus.derive()
edu.cmu.cs.ls.keymaerax.core.AxiomBase
edu.cmu.cs.ls.keymaerax.btactics.Ax
TactixLibrary
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 Cyber-Physical Systems. Springer, 2018.

See also
Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.
Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. 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 541-550. IEEE 2012
edu.cmu.cs.ls.keymaerax.core.AxiomBase
edu.cmu.cs.ls.keymaerax.btactics.Ax
HilbertCalculus
TactixLibrary
class IntegratorODESolverTool extends Tool with ODESolverTool
trait InvGenTool extends AnyRef
Continuous invariant generation tool.
Continuous invariant generation tool.

See also
edu.cmu.cs.ls.keymaerax.btactics.ToolProvider
case class MathematicaToolProvider(config: ToolProvider.Configuration) extends WolframToolProvider[Mathematica] with Product with Serializable
A tool provider that initializes tools to Mathematica.
A tool provider that initializes tools to Mathematica.
config
The Mathematica configuration (linkName, libDir).
case class ModelPlexConjecture(init: Formula, conjecture: Formula, constAssumptions: List[Formula]) extends Product with Serializable
A ModelPlex conjecture.
A ModelPlex conjecture. The constAssumptions are a subset of init for variables/function symbols not bound in the program.
trait ModelPlexTrait extends (List[Variable], Symbol) ⇒ (Formula) ⇒ Formula
ModelPlex: Verified runtime validation of verified cyber-physical system models.
ModelPlex: Verified runtime validation of verified cyber-physical system models.

See also
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyber-physical 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 cyber-physical system models. In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of LNCS, pages 199-214. Springer, 2014.
case class MultiToolProvider(providers: List[ToolProvider]) extends PreferredToolProvider[Tool] with Product with Serializable
Combines multiple tool providers.
class NanoTimer extends Timer
class NoneToolProvider extends ToolProvider
A tool provider without tools.
trait PolynomialRing extends AnyRef
Polynomial Ring:
Polynomial Ring:
- interface that describes Polynomials and operations on them - constructors for Polynomials from constant numbers, variables, and recursively from terms
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 SequentCalculus extends AnyRef
Sequent Calculus for propositional and first-order logic.
Sequent Calculus for propositional and first-order logic.

See also
Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008.
Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
edu.cmu.cs.ls.keymaerax.core.Rule
TactixLibrary
trait TacticIndex extends AnyRef

See also
AxIndex
trait TaylorModelOptions extends AnyRef
trait TimeStepOptions extends AnyRef
trait Timer extends AnyRef
trait ToolProvider extends AnyRef
A tool factory creates various arithmetic and simulation tools.
A tool factory creates various arithmetic and simulation tools.

See also
edu.cmu.cs.ls.keymaerax.tools.ToolInterface
case class TwoThreeTreePolynomialRing(variableOrdering: Ordering[Term], monomialOrdering: Ordering[IndexedSeq[(Term, Int)]]) extends PolynomialRing with Product with Serializable
A polynomial is represented as a set of monomials stored in a 2-3 Tree, the ordering is lexicographic A monomial is represented as a coefficient and a power-product.
A polynomial is represented as a set of monomials stored in a 2-3 Tree, the ordering is lexicographic A monomial is represented as a coefficient and a power-product. A coefficient is represented as a pair of BigDecimals for num/denom. A power product is represented densely as a list of exponents
All data-structures maintain a proof of input term = representation of data structure as Term
Representations of data structures (recursively applied on rhs):
- 3-Node (l, v1, m, v2, r) is "l + v1 + m + v2 + r"
- 2-Node (l, v, r) is "l + v + r"
- monomial (c, pp) is "c * pp"
- coefficient (num, denom) is "num / denom"
- 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., nonzero-assumptions on x or the like
All operations on the representations update the proofs accordingly.
trait UnifyUSCalculus extends AnyRef
Automatic unification-based Uniform Substitution Calculus with indexing.
Automatic unification-based 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 AxIndex.
This central collection of unification-based algorithms for focused proof strategies is the basis for using axioms and axiomatic proof rules in flexible ways. It is also central for deciding upon their succession in proof strategies, e.g., which steps to take next.
The most important algorithms are: - UnifyUSCalculus.useAt() makes use of a (derived) axiom or axiomatic rule in any position and logically transforms the goal to prove what is required for the transformation. - UnifyUSCalculus.chase chains together a sequence of canonical useAt inferences to make a formula disappear (chase it away) as far as possible.
Which part of a (derived) axiom to latch on to during a useAt is determined by the unification keys in the AxiomInfo.theKey. Which resulting subexpressions to consider next during a chase is determined by the recursors in the AxiomInfo.theRecursor. What unifier is used for the default key is, in turn, determined by AxiomInfo.unifier. Which (derived) axiom is the canonical one to decompose a given expression is determined by AxIndex.axiomsFor() Default keys and default recursors and default axiom indices can be overwritten by specifing extra arguments. This can be useful for noncanonical useAts or chases.
The combination of the UnifyUSCalculus algorithms make it possible to implement a tactic for using an axiom as follows:
```
useAt(Ax.composeb)
```
Such a tactic can then be applied in different positions of a sequent, e.g.:
```
useAt(Ax.composeb)(1)
useAt(Ax.composeb)(-2)
useAt(Ax.composeb)(1, 1::0::Nil)
```
The combination of the UnifyUSCalculus algorithms also make it possible to implement longer proof strategies. For example, completely chasing away a formula by successively using the canonical axioms on the resulting formulas is:
```
chase
```
Applying it at different positions of a sequent proceeds as follows, e.g.:
```
chase(1)
chase(-2)
chase(1, 1::0::Nil)
```
See also
AxiomInfo
edu.cmu.cs.ls.keymaerax.infrastruct.UnificationMatch
AxIndex
Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 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 WolframEngineToolProvider(config: ToolProvider.Configuration) extends WolframToolProvider[Mathematica] with Product with Serializable
A tool provider that initializes tools to Wolfram Engine.
case class WolframScriptToolProvider(config: ToolProvider.Configuration) extends WolframToolProvider[Mathematica] with Product with Serializable
A tool provider that initializes tools to Wolfram Script backend.
abstract class WolframToolProvider[T <: Tool] extends PreferredToolProvider[T]
Base class for Wolfram tools with alternative names.
case class Z3ToolProvider(config: ToolProvider.Configuration = Map("z3Path" -> Z3Installer.z3Path)) extends PreferredToolProvider[Tool] with Product with Serializable
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.

Value Members

object AnonymousLemmas
Stores lemmas without user-defined name.
object Approximator extends Logging
Approximations
Approximations
To do
More Ideas:
Allow approximations at non-top-level.
Pre-processing -- add time var w/ t_0=0, etc.
Post-processing -- 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/post-conditions and statements in discrete fragments for programs or in ev dom constraints.
object ArithmeticLibrary
Tactics for real arithmetic.
object ArithmeticSimplification
Tactics for simplifying arithmetic sub-goals.
object Ax extends Logging
Central Database of Derived Axioms and Derived Axiomatic Rules, including information about core axioms and axiomatic rules from This registry of also provides meta information for matching keys and recursors for unificiation and chasing using the @Axiom]] annotation.
Central Database of Derived Axioms and Derived Axiomatic Rules, including information about core axioms and axiomatic rules from This registry of also provides meta information for matching keys and recursors for unificiation and chasing using the @Axiom]] annotation.
Using Axioms and Axiomatic Rules
Using a (derived) axiom merely requires indicating the position where to use it:
```
UnifyUSCalculus.useAt(Ax.choiceb)(1)
```
Closing a proof or using an axiomatic rule after unification works as follows:
```
UnifyUSCalculus.byUS(Ax.choiceb)
```
Closing a proof or using an axiomatic rule verbatim without unification works as follows:
```
UnifyUSCalculus.by(Ax.choiceb)
```
Equivalently one can also write TactixLibrary.useAt or TactixLibrary.byUS because TactixLibrary extends UnifyUSCalculus.
Adding Derived Axioms and Derived Axiomatic Rules
Core Axioms are loaded from the core and their meta information is annotated in this file e.g. as follows:
```
@Axiom(("[∪]", "[++]"), conclusion = "__[a∪b]P__↔[a]P∧[b]P",
       key = "0", recursor = "0;1", unifier = "surjlinear")
val choiceb = coreAxiom("[++] choice")
```
Derived Axioms are proved with a tactic and their meta information is annotated in this file e.g. as follows:
```
@Axiom("V", conclusion = "p→__[a]p__",
       key = "1", recursor = "*")
lazy val V = derivedAxiom("V vacuous",
  "p() -> [a{|^@|};]p()".asFormula,
  useAt(Ax.VK, PosInExpr(1::Nil))(1) &
  useAt(Ax.boxTrue)(1)
)
```
Derived Axiomatic Rules are derived with a tactic and their meta information is annotated in this file as follows:
```
@ProofRule("M[]", conclusion = "[a;]P |- [a;]Q", premises = "P |- Q")
lazy val monb = derivedRuleSequent("M[]",
  Sequent(immutable.IndexedSeq("[a_;]p_(||)".asFormula), immutable.IndexedSeq("[a_;]q_(||)".asFormula)),
  someTactic)
```
Note
To simplify bootstrap and avoid dependency management, the proofs of the derived axioms are written with explicit reference to other scala-objects 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
edu.cmu.cs.ls.keymaerax.btactics.macros.AxiomInfo
edu.cmu.cs.ls.keymaerax.btactics.macros.Axiom
UnifyUSCalculus.matcherFor()
object AxIndex extends (Expression) ⇒ List[DerivationInfo] with 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. 219-266, 2017.
edu.cmu.cs.ls.keymaerax.core.AxiomBase
edu.cmu.cs.ls.keymaerax.btactics.macros.AxiomInfo
edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase()
edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chaseFor()
TactixLibrary.step
TactixLibrary.sequentStepIndex
object AxiomaticODESolver
An Axiomatic ODE solver.
An Axiomatic ODE solver. Current limitations: - No support for explicit-form 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 high-level 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 bifurcation-based proof search technique for the dynamic logic of ODEs.
object ConfigurableGenerator
object DebuggingTactics
object DerivationInfoRegistry extends Logging
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 Derive extends Derive
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
HilbertCalculus
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
HilbertCalculus
object HybridProgramCalculus extends HybridProgramCalculus
Hybrid Program Calculus for differential dynamic logic.
Hybrid Program Calculus for differential dynamic logic.

See also
HilbertCalculus
object Idioms
object ImplicitAx
Derives axioms from implicit (differential) definitionss
object Integrator extends Logging
Solves the initial value problem for systems of differential equations.
object IntervalArithmeticV2
Interval Arithmetic
object InvariantGenerator extends Logging
Invariant generators and differential invariant generators.
Invariant generators and differential invariant generators.

See also
TactixLibrary.invSupplier
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 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pages 28-48. Springer, 2012.
Andre Platzer and Edmund M. Clarke. Computing differential invariants of hybrid systems as fixedpoints. Formal Methods in System Design, 35(1), pp. 98-120, 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 cyber-physical system models.
ModelPlex: Verified runtime validation of verified cyber-physical system models.

See also
Stefan Mitsch and André Platzer. ModelPlex: Verified runtime validation of verified cyber-physical 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 cyber-physical system models. In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of LNCS, pages 199-214. Springer, 2014.
object MonomialOrders
object NoTimer extends Timer
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 ODELiveness
Implements ODE tactics for liveness.
Implements ODE tactics for liveness.
Created by yongkiat on 24 Feb 2020.
object ODEStability
Implements ODE tactics for stability
object PolynomialArith extends Logging
Created by yongkiat on 11/27/16.
object PolynomialArithV2 extends TwoThreeTreePolynomialRing
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 RicattiEquation
Decision procedure for a single Ricatti equation.
object RicattiSystem
Decision procedure for a system of Ricatti differential equations.
object SOSSolve
tactics to prove SOSsolve witnesses
object SequentCalculus extends SequentCalculus
Sequent Calculus for propositional and first-order logic.
Sequent Calculus for propositional and first-order logic.

See also
SequentCalculus
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 SwitchedSystems
Provides support for generating switched system models under various switching mechanisms.
Provides support for generating switched system models under various switching mechanisms.
Also provides proof automation for stability proofs
object TacticFactory
Basic facilities for easily creating tactic objects.
object TacticHelper
Some commonly useful helper utilities for basic tactic implementations.
object TacticIndex
Tactic indexing data structures for canonical proof strategies.
Tactic indexing data structures for canonical proof strategies.

See also
edu.cmu.cs.ls.keymaerax.btactics.AxiomInfo
object TactixInit
Initialization routine needs to set some global fields without causing TactixLibrary to initialize, so those fields are set here and can then be referenced from TactixLibrary
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 built-in 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.auto automatic proof search
- TactixLibrary.autoClose 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 first-order logic.
- HybridProgramCalculus: Hybrid program derived proof rules for differential dynamic logic.
- DifferentialEquationCalculus: Differential equation proof rules for differential dynamic logic.
- UnifyUSCalculus: Automatic unification-based 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. 219-266, 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 Cyber-Physical Systems. Springer, 2018.
HilbertCalculus
SequentCalculus
DifferentialEquationCalculus
HybridProgramCalculus
UnifyUSCalculus
Ax
AxiomInfo
edu.cmu.cs.ls.keymaerax.core.Rule
ToolProvider
object TaylorModelArith
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.
object TaylorModelTactics extends Logging
object Timer
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
edu.cmu.cs.ls.keymaerax.tools
edu.cmu.cs.ls.keymaerax.tools.ToolInterface
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 UnifyUSCalculus extends UnifyUSCalculus
Automatic unification-based Uniform Substitution Calculus with indexing.
Automatic unification-based 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 AxIndex.

See also
UnifyUSCalculus

Packages

KeYmaera X: An aXiomatic Tactical Theorem Prover

Package Structure

Entry Points

References

Proof Styles

Explicit Proof Certificates

Explicit Proofs

Proof by Search

Proof by Pointing

Proof by Congruence

Proof by Chase

Additional Mechanisms

KeYmaera X Kernel

Usage Overview

Constructing Proofs

Combining Proofs

Differential Dynamic Logic

Syntax

Static Semantics

Theorem Prover

Axioms

Uniform Substitutions

Sequent Proof Rules

Additional Capabilities

Stored Provable Mechanism

Error Reporting

Set Lattice

Overall Code Complexity

Lemma Mechanism

Usage Overview

Printing Differential Dynamic Logic

Printing Fully Parenthesized Forms

Parsing Differential Dynamic Logic

Parsing Only Formulas of Differential Dynamic Logic

Parsing Pretty-Printed Strings

Pretty-Printing Parsed Strings

Pretty-Printing Sequents

btactics 

package btactics

Proof Styles

Explicit Proof Certificates

Explicit Proofs

Proof by Search

Proof by Pointing

Proof by Congruence

Proof by Chase

Additional Mechanisms

Type Members

Value Members

Using Axioms and Axiomatic Rules

Adding Derived Axioms and Derived Axiomatic Rules

Inherited from AnyRef

Inherited from Any

Ungrouped

btactics