Packages

package root

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.

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 structures
- Expression - Differential dynamic logic expressions: Term, Formula, Program
- Sequent - Sequents of formulas
- Provable - Proof certificates transformed by rules/axioms
- Rule - Proof rules as well as USubstOne for (one-pass) uniform substitutions and renaming.
- StaticSemantics - Static semantics with free and bound variable analysis
- Instead of constructing dL expressions from constructors, it is easier to use the KeYmaeraXParser.
edu.cmu.cs.ls.keymaerax.parser - Parser and pretty printer with concrete syntax and notation for differential dynamic logic.
- Concrete syntax for input language Differential Dynamic Logic
- KeYmaeraXPrettyPrinter - Pretty printer producing concrete KeYmaera X syntax
- KeYmaeraXParser - Parser reading concrete KeYmaera X syntax
- KeYmaeraXArchiveParser - Parser reading KeYmaera X model and proof archive .kyx files
- DLParser - Combinator parser reading concrete KeYmaera X syntax
- DLArchiveParser - Combinator parser reading KeYmaera X model and proof archive .kyx files
edu.cmu.cs.ls.keymaerax.infrastruct - Prover infrastructure outside the kernel
- UnificationMatch - Unification algorithm
- RenUSubst - Renaming Uniform Substitution quickly combining kernel's renaming and substitution.
- Context - Representation for contexts of formulas in which they occur.
- Augmentors - Augmenting formula and expression data structures with additional functionality
- ExpressionTraversal - Generic traversal functionality for expressions
edu.cmu.cs.ls.keymaerax.bellerophon - Bellerophon tactic language and tactic interpreter
- BelleExpr - Tactic language expressions
- SequentialInterpreter - Sequential tactic interpreter for Bellerophon tactics
edu.cmu.cs.ls.keymaerax.btactics - Bellerophon tactic library for conducting proofs.
- TactixLibrary - Main KeYmaera X tactic library including many proof tactics.
- HilbertCalculus - Hilbert Calculus for differential dynamic 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 underlying the other calculi
- [edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic] - Forward tactic framework for conducting proofs from premises to conclusions
edu.cmu.cs.ls.keymaerax.lemma - Lemma mechanism
- Lemma - 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 back-end solvers
- MathematicaQETool - Mathematica interface for real arithmetic.
- Z3QETool - Z3 interface for real arithmetic.
edu.cmu.cs.ls.keymaerax.tools.ext - Extended back-ends 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 - Command-line launcher for KeYmaera X supports command-line argument -help to obtain usage information
edu.cmu.cs.ls.keymaerax.btactics.AxIndex - Axiom indexing data structures with keys and recursors for canonical proof strategies.
edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo - Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.
edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex - Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.
edu.cmu.cs.ls.keymaerax.btactics.Ax - Registry for derived axioms and axiomatic proof rules that are proved from the core.

References

Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:

1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.

2. Nathan Fulton, Stefan Mitsch, Jan-David 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. 527-538. Springer, 2015.

3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos

Definition Classes: root

package edu

Definition Classes: root

package cmu

Definition Classes: edu

package cs

Definition Classes: cmu

package ls

Definition Classes: cs

package keymaerax

Definition Classes: ls

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.

Definition Classes: keymaerax
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

package arithmetic

Definition Classes: btactics

package cexsearch

Definition Classes: btactics

package coasterx

Definition Classes: btactics

package components

Definition Classes: btactics

package dRL

Definition Classes: btactics

package helpers

Helper functions for implementing tactics.

Helper functions for implementing tactics. Note that these are **not** themselves tactics.

Definition Classes: btactics
See also: helpers.DifferentialHelper Differential Equation-specific program helpers.
helpers.ProgramHelpers Hybrid Program helpers that are not specific to Differential Equations.

package macros

Definition Classes: btactics

package robustify

Definition Classes: btactics

AnonymousLemmas

Approximator

ArithmeticLibrary

ArithmeticSimplification

AxIndex

AxiomaticODESolver

BelleLabels

BelleREPL

Bifurcation

Case

ConfigurableGenerator

DebuggingTactics

DefaultTacticIndex

DerivationInfoRegistry

Derive

DifferentialDecisionProcedures

DifferentialEquationCalculus

DifferentialSaturation

FOQuantifierTactics

FixedGenerator

Generator

HilbertCalculus

HybridProgramCalculus

Idioms

ImplicitAx

Integrator

IntegratorODESolverTool

IntervalArithmeticV2

InvGenTool

InvariantGenerator

InvariantProvers

IsabelleSyntax

Kaisar

MathematicaToolProvider

ModelPlex

ModelPlexConjecture

ModelPlexTrait

MonomialOrders

MultiToolProvider

NanoTimer

NoTimer

NoneToolProvider

ODEInvariance

ODELiveness

ODEStability

PolynomialArith

PolynomialArithV2

PolynomialArithV2Helpers

PolynomialRing

PreferredToolProvider

RicattiEquation

RicattiSystem

SOSSolve

SequentCalculus

Simplifier

SimplifierV2

SimplifierV3

SwitchedSystems

TacticFactory

TacticHelper

TacticIndex

TactixInit

TactixLibrary

TaylorModelArith

TaylorModelOptions

TaylorModelTactics

TimeStepOptions

Timer

ToolProvider

Transitivity

TwoThreeTreePolynomialRing

UnifyUSCalculus

WolframEngineToolProvider

WolframScriptToolProvider

WolframToolProvider

Z3ToolProvider

edu.cmu.cs.ls.keymaerax.btactics

ODELiveness

object ODELiveness

Implements ODE tactics for liveness.

Created by yongkiat on 24 Feb 2020.

Linear Supertypes

AnyRef, Any

Ordering

Alphabetic
By Inheritance

Inherited

ODELiveness
AnyRef
Any

Hide All
Show All

Visibility

Public
All

Value Members

final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def affine_form(odes: DifferentialProgram): (List[List[Term]], List[Term], List[Term])
Computes the affine form for ODEs
Computes the affine form for ODEs
odes
the ODEs to put into affine form
returns
A (matrix of terms), b (list of terms), x (list of variables) such that x'=Ax+b
final def asInstanceOf[T0]: T0

Definition Classes
Any
def bDG(ghost: Expression, p: Term): DependentPositionWithAppliedInputTactic
Wrapper around bDG for display.
Wrapper around bDG for display.

Annotations
@Tactic( x$13 , x$19 , x$14 , x$15 , x$16 , x$20 , x$21 , x$17 , x$22 , x$23 , x$18 , x$24 )
def bDG(ghost: DifferentialProgram, p: Term): DependentPositionTactic
Implements bDG rule that adds ghosts to box ODEs on the right of the turnstile
Implements bDG rule that adds ghosts to box ODEs on the right of the turnstile
G |- [ghosts, ODE] (||ghosts||)^2 <= p G |- [ghosts, ODE]P ---- dDG G |- [ODE]P
ghost
the ghost ODEs, L, M as above
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@native() @throws( ... )
def closedRef(R: Formula): DependentPositionWithAppliedInputTactic
Refinement for a closed domain constraint (e.g.
Refinement for a closed domain constraint (e.g. Q = p>=0)
G |- <ODE & R> P G |- p>0 //must start in interior of domain G |-[ODE & R & p>=0 & !P] p>0 //must stay in interior of domain except by possibly exiting exactly at the end ---- (closedRefine) G |- <ODE & p>=0> P

Annotations
@Tactic( x$73 , x$74 , x$75 , x$76 , x$77 , x$79 , x$80 , x$78 , x$81 , x$82 , x$83 , x$84 )
def compatCut(R: Formula): DependentPositionWithAppliedInputTactic
A tiny wrapper around cut.
A tiny wrapper around cut. This introduces a cut that is compatible for the ODE at a given position (regardless of modality and position, although most useful for diamond ODEs)
G, [x'=f(x)&Q]R |- C([x'=f(x)&Q]P) G|-[x'=f(x)&Q]R --- compatCut G |- C([x'=f(x)&Q]P)

Annotations
@Tactic( x$37 , x$38 , x$39 , x$40 , x$41 , x$44 , x$45 , x$42 , x$46 , x$47 , x$43 , x$48 )
def dBDG(p: Term): DependentPositionWithAppliedInputTactic

Annotations
@Tactic( x$85 , x$86 , x$87 , x$88 , x$89 , x$91 , x$92 , x$90 , x$93 , x$94 , x$95 , x$96 )
def dBDG(p: Term, dim: Int): DependentPositionTactic
def dDDG(L: Term, M: Term): DependentPositionWithAppliedInputTactic

Annotations
@Tactic( x$97 , x$98 , x$99 , x$100 , x$101 , x$103 , x$104 , x$102 , x$105 , x$106 , x$107 , x$108 )
def dDDG(L: Term, M: Term, dim: Int): DependentPositionTactic
def dDG(ghost: DifferentialProgram, L: Term, M: Term): DependentPositionTactic
Implements dDG rule that adds ghosts to box ODEs on the right of the turnstile
Implements dDG rule that adds ghosts to box ODEs on the right of the turnstile
G |- [ghosts, ODE] (||ghosts||)' <= L ||ghosts|| + M G |- [ghosts, ODE]P ---- dDG G |- [ODE]P
ghost
the ghost ODEs, L, M as above
def dDR(R: Formula): DependentPositionWithAppliedInputTactic
Implements DR<.> rule Note: uses auto cuts for the later premise
Implements DR<.> rule Note: uses auto cuts for the later premise
G |- <ODE & R> P G |- [ODE & R] Q ---- (dDR) G |- <ODE & Q> P
R
the formula R to refine the domain constraint
returns
two premises, as shown above when applied to a top-level succedent diamond

Annotations
@Tactic( x$61 , x$62 , x$63 , x$64 , x$65 , x$67 , x$68 , x$66 , x$69 , x$70 , x$71 , x$72 )
def dDX: BuiltInPositionTactic
ODE diamond is true if domain and postcondition was already true initially
ODE diamond is true if domain and postcondition was already true initially
G |- Q & P ---- G |- <x'=f(x)&Q>P
returns
see rule above
def dV(eps: Option[Term]): DependentPositionWithAppliedInputTactic

Annotations
@Tactic( x$121 , x$122 , x$123 , x$124 , x$125 , x$128 , x$129 , x$126 , x$130 , x$131 , x$127 , x$132 )
def dV(bnd: Term, manual: Boolean = false): DependentPositionTactic
Implements dV rule for atomic postconditions The bottom two premises are auto-closed because of the need to Dconstify The first one is partially auto-closed if odeReduce is able to prove global existence e.g.
Implements dV rule for atomic postconditions The bottom two premises are auto-closed because of the need to Dconstify The first one is partially auto-closed if odeReduce is able to prove global existence e.g. (similarly for dV >),
Note: autonormalizes to >= and > (but provided e_() must be for the normalized shape!)
G, t=0 |- <t'=1, ODE & Q> t > const G, t=0 |- e_() > 0 G, t=0 |- [t'=1, ODE & Q & p-q < 0] p'-q' >= e () (this uses compatible cuts ) ---- (dV >=) G |- <ODE & Q> p >= q
Note that domain constraint Q is kept around!
bnd
the lower bound on derivatives
manual
whether to try closing automatically
returns
closes (or partially so)
def dVAuto(autoqe: Boolean = true): DependentPositionTactic
def deriveGlobalExistence(ode: DifferentialProgram): Option[ProvableSig]
Given ODE, returns the global existence axiom <t'=1,x'=f(x)>t>p() (if it proves)
Given ODE, returns the global existence axiom <t'=1,x'=f(x)>t>p() (if it proves)
returns
(optional) ProvableSig proving the global existence axiom, None if failed
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
def gEx(hint: Option[Formula]): DependentPositionWithAppliedInputTactic

Annotations
@Tactic( x$109 , x$110 , x$111 , x$112 , x$113 , x$115 , x$116 , x$114 , x$117 , x$118 , x$119 , x$120 )
def gEx(hints: List[Formula]): DependentPositionTactic
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@native()
def getDDG(dim: Int): ProvableSig
def getDDGinst(ghostODEs: DifferentialProgram): ProvableSig
Helper that gets the appropriate DDG instance (already instantiated for the ghosts by renaming and friends) This helps simplify the (y^2)' term away
Helper that gets the appropriate DDG instance (already instantiated for the ghosts by renaming and friends) This helps simplify the (y^2)' term away
ghostODEs
the ghosts to add to the ODE
returns
DDG instantiated for the particular boxode question
def getVDGinst(ghostODEs: DifferentialProgram): (ProvableSig, ProvableSig)
Helper that gets the appropriate VDG instance (already instantiated for the ghosts and ODE by renaming and friends)
Helper that gets the appropriate VDG instance (already instantiated for the ghosts and ODE by renaming and friends)
ghostODEs
the ghost ODEs
returns
both directions of VDG instantiated for the ghost ODEs (everything else is left uninstantiated)
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@native()
def higherdV(bnds: List[Term]): DependentPositionTactic
Implements higher dV series rule for atomic postconditions with less automation Given a series a_0, a_1, ...
Implements higher dV series rule for atomic postconditions with less automation Given a series a_0, a_1, ... , a_n :
G |- [t'=1, ODE&Q & p<0] p >= a_0 + a_1 t + a_2 t^{2 + ... + a_n t}n G |- <t'=1, ODE & Q> a_0 + a_1 t + a_2 t^{2 + ... + a_n t}n > 0 ---- (higherdV >=) G |- <ODE & Q> p >= 0
Note that domain constraint Q is kept around!
bnds
the lower bound on derivatives
returns
two subgoals, shown above
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
def kDomainDiamond(R: Formula): DependentPositionWithAppliedInputTactic
Implements K<&> rule Note: uses auto cuts for the later premise
Implements K<&> rule Note: uses auto cuts for the later premise
G |- <ODE & Q> R G |- [ODE & Q & !P] !R ---- (kDomD) G |- <ODE & Q> P
R
the formula R to refine the postcondition
returns
two premises, as shown above when applied to a top-level succedent diamond

Annotations
@Tactic( x$49 , x$50 , x$54 , x$51 , x$52 , x$55 , x$56 , x$53 , x$57 , x$58 , x$59 , x$60 )
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@native()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@native()
def odeReduce(strict: Boolean = true, hints: List[Formula]): DependentPositionTactic
Applied to a top-level position containing a succedent diamond, this tactic removes irrelevant ODEs
Applied to a top-level position containing a succedent diamond, this tactic removes irrelevant ODEs
strict
whether to throw an error when it meets a nonlinear ODE that can't be reduced
hints
a list of
returns
reduces away all irrelevant ODEs
def odeUnify: DependentPositionTactic
Adds compatible (ODE unifiable) box modalities from the assumptions to the domain constraint e.g.
Adds compatible (ODE unifiable) box modalities from the assumptions to the domain constraint e.g. [x'=f(x)&A]B is compatible for [x'=f(x)&Q]P if A implies Q
[z'=g(z)&Q]P is compatible for [x'=f(x)&Q]P if z'=g(z) contains a subset of ODEs of x'=f(x)
For compatible assumptions, the rule adds them by diff cut, e.g.:
G, [x'=f(x)&A]B |- [x'=f(x)&Q&B]P --- G, [x'=f(x)&A]B |- [x'=f(x)&Q]P

Annotations
@Tactic( x$25 , x$26 , x$27 , x$28 , x$29 , x$31 , x$32 , x$30 , x$33 , x$34 , x$35 , x$36 )
def saveBox: DependentPositionTactic
Saves a (negated) box version of the liveness postcondition.
Saves a (negated) box version of the liveness postcondition. This is a helpful pattern because of compat cuts
G, [ODE & Q]!P |- <ODE & Q> P ---- (saveBox) G |- <ODE & Q> P
def semialgdV(bnd: Term): DependentPositionTactic
def semialgdVAuto(autoqe: Boolean = true): DependentPositionTactic
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
def toString(): String

Definition Classes
AnyRef → Any
def vDG(ghost: Expression): DependentPositionWithAppliedInputTactic
Wrapper around vDG for display.
Wrapper around vDG for display.

Annotations
@Tactic( x$1 , x$7 , x$2 , x$3 , x$4 , x$8 , x$9 , x$5 , x$10 , x$11 , x$6 , x$12 )
def vDG(ghost: DifferentialProgram): DependentPositionTactic
Implements linear vDG rule that adds ghosts to an ODE on the left or right, in either modality For boxes on the right and diamonds on the left, the ODE must be affine
Implements linear vDG rule that adds ghosts to an ODE on the left or right, in either modality For boxes on the right and diamonds on the left, the ODE must be affine
```
G |- [y'=g(x,y),x'=f(x)]P
---- vDG (g affine in y)
G |- [x'=f(x)]P

[y'=g(x,y),x'=f(x)]P |- D
----
[x'=f(x)]P |- D
```
ghost
the ODEs to ghost in
returns
the sequent with ghosts added in requested position
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@native() @throws( ... )

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

ODELiveness

object ODELiveness

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

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

ODELiveness 

object ODELiveness

Value Members

Inherited from AnyRef

Inherited from Any

Ungrouped

ODELiveness