Packages

trait DifferentialEquationCalculus extends AnyRef

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

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. DifferentialEquationCalculus
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. def dC(R: List[Formula]): DependentPositionWithAppliedInputTactic
    Annotations
    @Tactic( x$32 , x$33 , x$25 , x$26 , x$27 , x$28 , x$29 , x$34 , x$35 , x$31 , x$36 , x$30 )
  7. def dC(R: Formula): DependentPositionWithAppliedInputTactic

    DC: Differential Cut a new invariant, use old(x) to refer to initial values of variable x.

    DC: Differential Cut a new invariant, use old(x) to refer to initial values of variable x. Use special function old(.) to introduce a discrete ghost for the starting value of a variable that can be used in the evolution domain constraint.

    Use:                      Show:
    G |- [x'=f(x)&Q&R]P, D    G |- [x'=f(x)&Q]R, D
    ---------------------------------------------- dC(R)
    G |- [x'=f(x)&Q]P, D

    Also works in context, e.g.:

    Use:                         Show:
    G |- A->[x'=f(x)&Q&R]P, D    G |- A->[x'=f(x)&Q]R, D
    ---------------------------------------------- dC(R)
    G |- A->[x'=f(x)&Q]P, D
    R

    the formula that will be cut into the differential equation (in that order if it is a list). The formulas are typically shown to be differential invariants subsequently. They can use old(x) and old(y) etc. to refer to the initial values of x and y, respectively.

    Examples:
    1. x>0 |- [{x'=2&x>0}]x>=0     x>0 |- [{x'=2}]x>0
      -----------------------------------------------dC("x>0".asFormula)(1)
      x>0 |- [{x'=2}]x>=0
    2. ,
    3. x>0, x_0=x |- [{x'=2&x>=x_0}]x>=0     x>0, x_0=x |- [{x'=2}]x>=x_0
      -------------------------------------------------------------------dC("x>=old(x)".asFormula)(1)
      x>0 |- [{x'=2}]x>=0
    4. ,
    5. x>0, v>=0, x_0=x |- [{x'=v,v'=1&v>=0&x>=x_0}]x>=0
             x>0, v>=0 |- [{x'=v,v'=1}]v>=0
      x>0, v>=0, x_0=x |- [{x'=v,v'=1&v>=0}]x>=x_0
      --------------------------------------------------dC("v>=0".asFormula, "x>=old(x)".asFormula)(1)
             x>0, v>=0 |- [{x'=v,v'=1}]x>=0
    Note

    dC is often needed when FV(post) depend on BV(ode) that are not in FV(constraint).

  8. def dG(E: Expression, G: Option[Formula]): DependentPositionWithAppliedInputTactic

    dG(ghost,r): Differential Ghost add auxiliary differential equations with extra variables ghost of the form y'=a*y+b and the postcondition replaced by r, if provided.

    dG(ghost,r): Differential Ghost add auxiliary differential equations with extra variables ghost of the form y'=a*y+b and the postcondition replaced by r, if provided.

    G |- \exists y [x'=f(x),y'=g(x,y)&q(x)]r(x,y), D
    ----------------------------------------------------------  dG using p(x) <-> \exists y. r(x,y) by QE
    G |- [x'=f(x)&q(x)]p(x), D
    Annotations
    @Tactic( x$80 , x$81 , x$73 , x$74 , x$75 , x$76 , x$77 , x$82 , x$83 , x$78 , x$79 , x$84 )
    Example:
    1. proveBy("x>0->[{x'=-x}]x>0".asFormula, implyR(1) &
        dG("{y'=(1/2)*y}".asDifferentialProgram, Some("x*y^2=1".asFormula))(1) &
          diffInd()(1, 0::Nil) & QE
        )

      with optional instantiation of initial y

      proveBy("x>0->[{x'=-x}]x>0".asFormula, implyR(1) &
        dG("{y'=(1/2)*y}".asDifferentialProgram, Some("x*y^2=1".asFormula))(1) &
          existsR("1/x^(1/2)".asFormula)(1) & diffInd()(1) & QE
        )
    Note

    Uses QE to prove p(x) <-> \exists y. r(x,y)

  9. def dGold(y: Variable, t1: Term, t2: Term, p: Option[Formula]): DependentPositionWithAppliedInputTactic
    Annotations
    @Tactic( x$85 , x$90 , x$86 , x$88 , x$87 , x$91 , x$92 , x$93 , x$94 , x$95 , x$89 , x$96 )
  10. def dI(auto: Symbol = 'full): DependentPositionTactic

    dI: Differential Invariant proves a formula to be an invariant of a differential equation (with the usual steps to prove it invariant).

    dI: Differential Invariant proves a formula to be an invariant of a differential equation (with the usual steps to prove it invariant). (uses DI, DW, DE, QE)

    auto

    One of 'none, 'diffInd, 'full. Whether or not to automatically close and use DE, DW. 'full: tries to close everything after diffInd rule (turning free variables to constants)

      *
    --------------------------
    G |- [x'=f(x)&q(x)]p(x), D

    'none: behaves as using DI axiom per cheat sheet

    G, q(x) |- p(x), D    G, q(x) |- [x'=f(x)&q(x)](p(x))', D
    ---------------------------------------------------------
                G |- [x'=f(x)&q(x)]p(x), D

    'diffInd: behaves as dI rule per cheat sheet

    G, q(x) |- p(x), D     q(x) |- [x':=f(x)]p'(x')    @note derive on (p(x))' already done
    ----------------------------------------------
                G |- [x'=f(x)&q(x)]p(x), D
    Examples:
    1.      *
      ---------------------diffInd('full)(1)
      x>=5 |- [{x'=2}]x>=5
    2. ,
    3. x>=5, true |- x>=5    true |- [{x':=2}]x'>=0
      --------------------------------------------diffInd('diffInd)(1)
      x>=5 |- [{x'=2}]x>=5
    4. ,
    5. x>=5, true |- x>=5    x>=5, true |- [{x'=2}](x>=5)'
      ---------------------------------------------------diffInd('none)(1)
      x>=5 |- [{x'=2}]x>=5
    6. ,
    7. x>=5 |- [x:=x+1;](true -> x>=5&2>=0)
      -------------------------------------diffInd('full)(1, 1::Nil)
      x>=5 |- [x:=x+1;][{x'=2}]x>=5
    8. ,
    9. proveBy("x^2>=2->[{x'=x^3}]x^2>=2".asFormula, implyR(1) &
        diffInd()(1) & QE
      )
    See also

    HilbertCalculus.DI

  11. def dIClose: DependentPositionTactic

    dIClose: Differential Invariant proves a formula to be an invariant of a differential equation closing with the usual steps to prove it invariant.

    dIClose: Differential Invariant proves a formula to be an invariant of a differential equation closing with the usual steps to prove it invariant. (uses DI, DW, DE, QE). Tries to close everything after diffInd rule (turning free variables to constants)

         *
    -------------------------- dIClose
    G |- [x'=f(x)&q(x)]p(x), D
    Annotations
    @Tactic( x$56 , x$57 , x$49 , x$50 , x$51 , x$52 , x$53 , x$54 , x$58 , x$55 , x$59 , x$60 )
    Examples:
    1.      *
      ---------------------dIClose(1)
      x>=5 |- [{x'=2}]x>=5
    2. ,
    3. x>=5 |- [x:=x+1;](true -> x>=5&2>=0)
      -------------------------------------dIClose(1, 1::Nil)
      x>=5 |- [x:=x+1;][{x'=2}]x>=5
    See also

    HilbertCalculus.DI

  12. def dIRule: DependentPositionTactic

    dIRule: Differential Invariant proves a formula to be an invariant of a differential equation.

    dIRule: Differential Invariant proves a formula to be an invariant of a differential equation. (uses DI, DW, DE).

    G, q(x) |- p(x), D     q(x) |- [x':=f(x)]p'(x')    @note derive on (p(x))' already done
    ---------------------------------------------- dIRule
         G |- [x'=f(x)&q(x)]p(x), D
    Annotations
    @Tactic( x$44 , x$45 , x$37 , x$38 , x$39 , x$40 , x$41 , x$42 , x$46 , x$43 , x$47 , x$48 )
    Example:
    1. x>=5, true |- x>=5    true |- [{x':=2}]x'>=0
      --------------------------------------------dIRule(1)
      x>=5 |- [{x'=2}]x>=5
    See also

    HilbertCalculus.DI

  13. def dIX: DependentPositionTactic
    Annotations
    @Tactic( x$61 , x$69 , x$62 , x$63 , x$64 , x$65 , x$66 , x$67 , x$70 , x$68 , x$71 , x$72 )
  14. def dR(formula: Formula, hide: Boolean = true): DependentPositionTactic

    Refine top-level antecedent/succedent ODE domain constraint G|- [x'=f(x)&R]P, D G|- [x'=f(x)&Q]R, (D)? ---------------------------------------------- dR G|- [x'=f(x)&Q]P, D

    Refine top-level antecedent/succedent ODE domain constraint G|- [x'=f(x)&R]P, D G|- [x'=f(x)&Q]R, (D)? ---------------------------------------------- dR G|- [x'=f(x)&Q]P, D

    formula

    the formula R to refine Q to

    hide

    whether to keep the extra succedents (D) around (default true), which makes position management easier

  15. lazy val dW: DependentPositionTactic

    DW: Differential Weakening uses evolution domain constraint so [{x'=f(x)&q(x)}]p(x) reduces to \forall x (q(x)->p(x)).

    DW: Differential Weakening uses evolution domain constraint so [{x'=f(x)&q(x)}]p(x) reduces to \forall x (q(x)->p(x)).

    Note

    FV(post)/\BV(x'=f(x)) subseteq FV(q(x)) usually required to have a chance to succeed.

    See also

    HilbertCalculus.DW

  16. lazy val dWPlus: DependentPositionTactic

    Same as dW but preserves information about the initial conditions

    Same as dW but preserves information about the initial conditions

    See also

    dW

  17. def diffInvariant(invariants: List[Formula]): DependentPositionWithAppliedInputTactic
  18. def diffInvariant(invariant: Formula): DependentPositionWithAppliedInputTactic

    DC+DI: Prove the given list of differential invariants in that order by DC+DI via dC followed by dI Combines differential cut and differential induction.

    DC+DI: Prove the given list of differential invariants in that order by DC+DI via dC followed by dI Combines differential cut and differential induction. Use special function old(.) to introduce a ghost for the starting value of a variable that can be used in the evolution domain constraint. Uses diffInd to prove that the formulas are differential invariants. Fails if diffInd cannot prove invariants.

    Annotations
    @Tactic( x$102 , x$103 , x$97 , x$98 , x$99 , x$104 , x$105 , x$106 , x$107 , x$101 , x$100 , x$108 )
    Examples:
    1. x>0 |- [{x'=2&x>0}]x>=0
      ------------------------diffInvariant("x>0".asFormula)(1)
      x>0 |- [{x'=2}]x>=0
    2. ,
    3. x>0, x_0=x |- [{x'=2&x>x_0}]x>=0
      ---------------------------------diffInvariant("x>old(x)".asFormula)(1)
             x>0 |- [{x'=2}]x>=0
    4. ,
    5. x>0, v>=0, x_0=x |- [{x'=v,v'=1 & v>=0&x>x_0}]x>=0
      ---------------------------------------------------diffInvariant("v>=0".asFormula, "x>old(x)".asFormula)(1)
             x>0, v>=0 |- [{x'=v,v'=1}]x>=0
    See also

    dC

    dI

  19. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  20. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  21. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  22. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  23. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  24. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  25. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  27. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  28. def openDiffInd: DependentPositionTactic

    DIo: Open Differential Invariant proves an open formula to be an invariant of a differential equation (with the usual steps to prove it invariant) openDiffInd: proves an inequality to be an invariant of a differential equation (by DIo, DW, DE, QE) For strict inequalities, it uses open diff ind (<,>)

    DIo: Open Differential Invariant proves an open formula to be an invariant of a differential equation (with the usual steps to prove it invariant) openDiffInd: proves an inequality to be an invariant of a differential equation (by DIo, DW, DE, QE) For strict inequalities, it uses open diff ind (<,>)

    Examples:
    1.      *
      ---------------------openDiffInd(1)
      x^2>5 |- [{x'=x^3+x^4}]x^2>5
    2. ,
    3.      *
      ---------------------openDiffInd(1)
      x^3>5 |- [{x'=x^3+x^4}]x^3>5
    4. ,
    5. proveBy("x^2>9->[{x'=x^4}]x^2>9".asFormula, implyR(1) &
        openDiffInd()(1)
      )
  29. lazy val solve: DependentPositionTactic

    diffSolve: solve a differential equation [x'=f]p(x) to \forall t>=0 [x:=solution(t)]p(x).

    diffSolve: solve a differential equation [x'=f]p(x) to \forall t>=0 [x:=solution(t)]p(x). Similarly, [x'=f(x)&q(x)]p(x) turns to \forall t>=0 (\forall 0<=s<=t q(solution(s)) -> [x:=solution(t)]p(x)).

    Annotations
    @Tactic( x$1 , x$9 , x$2 , x$3 , x$4 , x$5 , x$6 , x$8 , x$10 , x$7 , x$11 , x$12 )
  30. lazy val solveEnd: DependentPositionTactic

    diffSolve with evolution domain check at duration end: solve [x'=f]p(x) to \forall t>=0 [x:=solution(t)]p(x).

    diffSolve with evolution domain check at duration end: solve [x'=f]p(x) to \forall t>=0 [x:=solution(t)]p(x). Similarly, [x'=f(x)&q(x)]p(x) turns to \forall t>=0 (q(solution(t)) -> [x:=solution(t)]p(x)).

    Annotations
    @Tactic( x$18 , x$19 , x$13 , x$14 , x$15 , x$20 , x$21 , x$17 , x$22 , x$16 , x$23 , x$24 )
  31. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  32. def toString(): String
    Definition Classes
    AnyRef → Any
  33. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  34. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  35. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped