Packages

p

edu.cmu.cs.ls.keymaerax

btactics

package btactics

Tactic library in the Bellerophon tactic language.

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:

  1. 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 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("<-> 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

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
  1. Alphabetic
  2. By Inheritance
Inherited
  1. btactics
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. sealed trait ArgInfo extends AnyRef

    Information on the arguments, their names and sorts, that an axiom/rule/tactic requires as input.

  2. 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.

  3. trait AxiomInfo extends ProvableInfo

    Meta-Information for an axiom or derived axiom

    Meta-Information for an axiom or derived axiom

    See also

    edu.cmu.cs.ls.keymaerax.btactics.AxiomIndex

  4. 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

    DerivedRuleInfo

  5. class BelleREPL extends AnyRef

    Created by bbohrer on 12/19/16.

  6. class BuiltinInfo extends DerivationInfo

    Meta-information on builtin tactic expressions (expand etc.).

  7. case class Case(fml: Formula, simplify: Boolean = true) extends Product with Serializable
  8. 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.

  9. case class CoreAxiomInfo(canonicalName: String, display: DisplayInfo, codeName: String, linear: Boolean, expr: (Unit) ⇒ DependentPositionTactic) extends AxiomInfo with Product with Serializable

    Meta-Information for an axiom from the prover core

    Meta-Information for an axiom from the prover core

    See also

    edu.cmu.cs.ls.keymaerax.core.AxiomBase

    DerivedAxiomInfo

  10. class DefaultTacticIndex extends TacticIndex
  11. sealed trait DerivationInfo extends AnyRef

    Central meta-information on a derivation step, which is an axiom, derived axiom, proof rule, or tactic.

    Central meta-information 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

    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.

    See also

    CoreAxiomInfo

    DerivedAxiomInfo

    AxiomaticRuleInfo

    DerivedRuleInfo

    TacticInfo

  12. 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.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.DerivedAxioms

    CoreAxiomInfo

  13. 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

    See also

    edu.cmu.cs.ls.keymaerax.btactics.DerivedAxioms

    AxiomaticRuleInfo

  14. 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.

    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.DerivedAxioms

  15. sealed trait DisplayInfo extends AnyRef

    UI display information on how to render an axiom, rule, or tactic application

  16. case class ExpressionArg(name: String, allowsFresh: List[String] = Nil, converter: (Expression) ⇒ Either[Expression, String] = e => Left(e)) extends ArgInfo with Product with Serializable
  17. case class FixedGenerator[A](list: List[A]) extends btactics.Generator.Generator[A] with Product with Serializable

    Generator always providing a fixed list as output.

  18. case class FormulaArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
  19. 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.DerivedAxioms

  20. 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.DerivedAxioms

    HilbertCalculus

  21. 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.

  22. 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
  23. 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
  24. 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
  25. class IntegratorODESolverTool extends Tool with ODESolverTool
  26. trait InvGenTool extends AnyRef

    Continuous invariant generation tool.

    Continuous invariant generation tool.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.ToolProvider

  27. class MathematicaToolProvider extends WolframToolProvider

    A tool provider that initializes tools to Mathematica.

  28. 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.

  29. class MultiToolProvider extends PreferredToolProvider[Tool]

    Combines multiple tool providers.

  30. class NoneToolProvider extends ToolProvider

    A tool provider without tools.

  31. case class OptionArg(arg: ArgInfo) extends ArgInfo with Product with Serializable
  32. 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
  33. 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.

  34. trait ProvableInfo extends DerivationInfo

    Meta-Information for a (derived) axiom or (derived) axiomatic rule

    Meta-Information for a (derived) axiom or (derived) axiomatic rule

    See also

    AxiomInfo

    AxiomaticRuleInfo

    DerivedRuleInfo

  35. 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.

  36. 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

  37. 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.

  38. case class SimpleDisplayInfo(name: String, asciiName: String) extends DisplayInfo with Product with Serializable

    Render as a UI name and a plain text ASCII name.

  39. trait StorableInfo extends DerivationInfo

    Storable derivation info (e.g., as lemmas).

    Storable derivation info (e.g., as lemmas).

    See also

    DerivedAxiomInfo

    DerivedRuleInfo

  40. case class StringArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
  41. case class SubstitutionArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
  42. trait TacticIndex extends AnyRef
  43. class TacticInfo extends DerivationInfo

    Meta-information on a tactic performing a proof step (or more)

  44. 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.

  45. case class TermArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
  46. 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

  47. case class TwoPositionTacticInfo(codeName: String, display: DisplayInfo, expr: (Unit) ⇒ Any, needsTool: Boolean = false, needsGenerator: Boolean = false) extends TacticInfo with Product with Serializable
  48. case class TwoThreeTreePolynomialRing(variables: IndexedSeq[Term]) 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/denum. 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, denum) is "num / denum"
    • power product [e1, ..., en] is "x1e1 * ... * xn en", where instead of "x0", we write "1" in order to avoid trouble with 00, i.e., nonzero-assumptions on x or the like

    All operations on the representations update the proofs accordingly.

  49. abstract class TypedFunc[-A, +R] extends (A) ⇒ R

    Typed functions to circumvent type erasure of arguments and return types.

  50. 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 AxiomIndex.

    See also

    edu.cmu.cs.ls.keymaerax.infrastruct.UnificationMatch

    AxiomIndex

    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.

  51. case class VariableArg(name: String, allowsFresh: List[String] = Nil) extends ArgInfo with Product with Serializable
  52. class WolframEngineToolProvider extends WolframToolProvider

    A tool provider that initializes tools to Wolfram Engine.

  53. class WolframScriptToolProvider extends WolframToolProvider

    A tool provider that initializes tools to Wolfram Script backend.

  54. abstract class WolframToolProvider extends PreferredToolProvider[Tool]

    Base class for Wolfram tools with alternative names.

  55. 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.

  56. 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

  1. object AnonymousLemmas

    Stores lemmas without user-defined name.

  2. 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.
  3. object ArithmeticLibrary

    Tactics for real arithmetic.

  4. object ArithmeticSimplification

    Tactics for simplifying arithmetic sub-goals.

  5. 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. 219-266, 2017.

    edu.cmu.cs.ls.keymaerax.core.AxiomBase

    edu.cmu.cs.ls.keymaerax.btactics.AxiomInfo

    edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chase()

    edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.chaseFor()

    TactixLibrary.step

    TactixLibrary.sequentStepIndex

  6. object AxiomInfo
  7. 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.

  8. 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.

  9. object Bifurcation

    Implements a bifurcation-based proof search technique for the dynamic logic of ODEs.

  10. object CoreAxiomInfo extends Serializable
  11. object DebuggingTactics

  12. 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.

  13. object DerivedAxiomInfo extends Serializable
  14. 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 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

  15. object DerivedRuleInfo extends Serializable
  16. object DifferentialDecisionProcedures

    Decision procedures for various classes of differential equations.

  17. object DifferentialEquationCalculus extends DifferentialEquationCalculus

    Differential Equation Calculus for differential dynamic logic.

    Differential Equation Calculus for differential dynamic logic.

    See also

    HilbertCalculus

  18. 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

  19. object FOQuantifierTactics

    Implementation: FOQuantifierTactics provides tactics for instantiating quantifiers.

    Implementation: FOQuantifierTactics provides tactics for instantiating quantifiers.

    Attributes
    protected
  20. object Generator

    Invariant generator

  21. object HilbertCalculus extends HilbertCalculus

    Hilbert Calculus for differential dynamic logic.

    Hilbert Calculus for differential dynamic logic.

    See also

    HilbertCalculus

  22. object HybridProgramCalculus extends HybridProgramCalculus

    Hybrid Program Calculus for differential dynamic logic.

    Hybrid Program Calculus for differential dynamic logic.

    See also

    HilbertCalculus

  23. object Idioms

  24. object Integrator extends Logging

    Solves the initial value problem for systems of differential equations.

  25. object IntervalArithmetic extends Logging

    Tactics for introducing interval arithmetic.

  26. object IntervalArithmeticV2

    Interval Arithmetic

  27. object InvariantGenerator extends Logging

    Invariant generators and differential invariant generators.

    Invariant generators and differential invariant generators.

    See also

    TactixLibrary.invGenerator

    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

  28. object InvariantProvers

    Invariant proof automation with generators.

  29. object IsabelleSyntax

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

  30. object Kaisar

    Created by bbohrer on 12/2/16.

  31. 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.

  32. 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.

  33. object PolynomialArith extends Logging

    Created by yongkiat on 11/27/16.

  34. 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

  35. object PolynomialArithV2Helpers
  36. object ProvableInfo
  37. object RicattiEquation

    Decision procedure for a single Ricatti equation.

  38. object RicattiSystem

    Decision procedure for a system of Ricatti differential equations.

  39. object SequentCalculus extends SequentCalculus

    Sequent Calculus for propositional and first-order logic.

    Sequent Calculus for propositional and first-order logic.

    See also

    SequentCalculus

  40. 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.

  41. object SimplifierV2

    Created by yongkiat on 9/29/16.

  42. 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.

  43. object TacticFactory

    Creates tactic objects

  44. object TacticHelper
  45. 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

  46. object TacticInfo
  47. 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:

    The tactic library also includes important proof calculus subcollections:

    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

    DerivedAxioms

    AxiomInfo

    edu.cmu.cs.ls.keymaerax.core.Rule

    ToolProvider

  48. object TaylorModelTactics extends Logging
  49. 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

  50. 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.

  51. object TypedFunc

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

  52. 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 AxiomIndex.

    See also

    UnifyUSCalculus

Inherited from AnyRef

Inherited from Any

Ungrouped