Packages

c

edu.cmu.cs.ls.keymaerax.core

USubstChurch

final case class USubstChurch(subsDefsInput: Seq[SubstitutionPair]) extends (Expression) ⇒ Expression with Product with Serializable

A Uniform Substitution with its application mechanism (original version). A Uniform Substitution uniformly replaces all occurrences of a given predicate p(.) by a formula in (.). It can also replace all occurrences of a function symbol f(.) by a term in (.) and all occurrences of a quantifier symbols C(-) by a formula in (-) and all occurrences of program constant b by a hybrid program.

This type implements the application of uniform substitutions to terms, formulas, programs, and sequents.

Annotations
@deprecated
Deprecated

Use faster USubstOne instead

Examples:

  1. Uniform substitution can be applied to a formula

    val p = Function("p", None, Real, Bool)
val x = Variable("x", None, Real)
// p(x) <-> ! ! p(- - x)
val prem = Equiv(PredOf(p, x), Not(Not(PredOf(p, Neg(Neg(x))))))
val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm),
    GreaterEqual(Power(DotTerm, Number(5)), Number(0)))))
// x^5>=0 <-> !(!((-(-x))^5>=0))
println(s(prem))
    2. ,

  2. Uniform substitutions can be applied via the uniform substitution proof rule to a sequent:

    val p = Function("p", None, Real, Bool)
val x = Variable("x", None, Real)
// p(x) <-> ! ! p(- - x)
val prem = Equiv(PredOf(p, x), Not(Not(PredOf(p, Neg(Neg(x))))))
val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm), GreaterEqual(Power(DotTerm, Number(5)), Number(0)))))
val conc = "x^5>=0 <-> !(!((-(-x))^5>=0))".asFormula
val next = UniformSubstitutionRule(s,
  Sequent(IndexedSeq(), IndexedSeq(prem)))(
    Sequent(IndexedSeq(), IndexedSeq(conc)))
// results in: p(x) <-> ! ! p(- - x)
println(next)
    3. ,

  3. Uniform substitutions also work for substituting hybrid programs

    val p = Function("p", None, Real, Bool)
val x = Variable("x", None, Real)
val a = ProgramConst("a")
// [a]p(x) <-> [a](p(x)&true)
val prem = Equiv(Box(a, PredOf(p, x)), Box(a, And(PredOf(p, x), True)))
val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm), GreaterEqual(DotTerm, Number(2))),
  SubstitutionPair(a, ODESystem(AtomicODE(DifferentialSymbol(x), Number(5)), True))))
// "[x'=5;]x>=2 <-> [x'=5;](x>=2&true)".asFormula
println(s(prem))
    4. ,

  4. Uniform substitution rule also works when substitution hybrid programs

    val p = Function("p", None, Real, Bool)
val x = Variable("x", None, Real)
val a = ProgramConst("a")
// [a]p(x) <-> [a](p(x)&true)
val prem = Equiv(Box(a, PredOf(p, x)), Box(a, And(PredOf(p, x), True)))
val s = USubst(Seq(SubstitutionPair(PredOf(p, DotTerm), GreaterEqual(DotTerm, Number(2))),
  SubstitutionPair(a, ODESystem(AtomicODE(DifferentialSymbol(x), Number(5)), True))))
val conc = "[x'=5;]x>=2 <-> [x'=5;](x>=2&true)".asFormula
val next = UniformSubstitutionRule(s,
 Sequent(IndexedSeq(), IndexedSeq(prem)))(
   Sequent(IndexedSeq(), IndexedSeq(conc)))
// results in: [x'=5;]x>=2 <-> [x'=5;](x>=2&true)
println(next)
Note

Implements the "global" version that checks admissibility eagerly at bound variables rather than computing bounds on the fly and checking upon occurrence. Main ingredient of prover core.

,

Superseded by faster alternative USubstOne.

,

soundness-critical

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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

Andre Platzer. Uniform substitution for differential game logic. In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Automated Reasoning, 9th International Joint Conference, IJCAR 2018, volume 10900 of LNCS, pp. 211-227. Springer 2018.

Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

edu.cmu.cs.ls.keymaerax.core.Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubstChurch):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

USubstOne

Linear Supertypes
Serializable, Serializable, Product, Equals, (Expression) ⇒ Expression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. USubstChurch
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. Function1
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new USubstChurch(subsDefsInput: Seq[SubstitutionPair])

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def ++(other: USubstChurch): USubstChurch

    Union of uniform substitutions, i.e., both replacement lists merged.

    Union of uniform substitutions, i.e., both replacement lists merged.

    Note

    Convenience method not used in the core, but used for stapling uniform substitutions together during unification etc.

  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  6. def apply(s: Sequent): Sequent

    Apply uniform substitution everywhere in the sequent.

  7. def apply(p: DifferentialProgram): DifferentialProgram

    apply this uniform substitution everywhere in a differential program

  8. def apply(p: Program): Program

    apply this uniform substitution everywhere in a program

  9. def apply(f: Formula): Formula

    apply this uniform substitution everywhere in a formula

  10. def apply(t: Term): Term

    apply this uniform substitution everywhere in a term

  11. def apply(e: Expression): Expression
    Definition Classes
    USubstChurch → Function1
  12. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  13. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  14. def compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  15. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. def finalize(): scala.Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  17. lazy val freeVars: SetLattice[Variable]

    The (new) free variables that this substitution introduces (without DotTerm/DotFormula arguments).

    The (new) free variables that this substitution introduces (without DotTerm/DotFormula arguments). That is the (new) free variables introduced by this substitution, i.e. free variables of all repl that are not bound as arguments in what.

    returns

    union of the freeVars of all our substitution pairs.

  18. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  19. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  20. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  21. final def notify(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  22. final def notifyAll(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  23. lazy val signature: Set[NamedSymbol]

    The signature of the replacement introduced by this substitution.

    The signature of the replacement introduced by this substitution.

    returns

    union of the freeVars of all our substitution pairs.

  24. val subsDefsInput: Seq[SubstitutionPair]
  25. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  26. def toString(): String
    Definition Classes
    USubstChurch → Function1 → AnyRef → Any
  27. final def wait(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. final def wait(arg0: Long, arg1: Int): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped