Type Members

1.  case class And(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable

   & logical conjunction: and.

2.  case class AndLeft(pos: AntePos) extends LeftRule with Product with Serializable

   &L And left.

   &L And left.

     G, p, q |- D
   --------------- (&L And left)
     p&q, G |- D

3.  case class AndRight(pos: SuccPos) extends RightRule with Product with Serializable

   &R And right

   &R And right

   G |- p, D    G |- q, D
   ---------------------- (&R And right)
     G |- p&q, D

4.  case class AntePos extends SeqPos with Product with Serializable

   Antecedent Positions of formulas in a sequent, i.e.

   Antecedent Positions of formulas in a sequent, i.e. in the assumptions on the left of the sequent arrow.

5.  trait ApplicationOf extends Composite

   Function/predicate/predicational application.

6.  class Assertion extends AnyRef

   A wrapper around the Java assert keyword.

   A wrapper around the Java assert keyword. Lazy evaluation of conditions and messages.

   Disabled by default. Enable at run-time with java -ea. Disable with java -da.

7.  case class Assign(x: Variable, e: Term) extends AtomicProgram with Product with Serializable

   x:=e assignment and/or differential assignment x':=e.

8.  case class AssignAny(x: Variable) extends AtomicProgram with Product with Serializable

   x:=* nondeterministic assignment and/or nondeterministic differential assignment x':=*.

9.  trait Atomic extends Expression

   Atomic expressions that do not have any proper subexpressions.

10.  trait AtomicDifferentialProgram extends AtomicProgram with DifferentialProgram

    Atomic differential programs that have no sub-differential-equations (but may still have subterms)

11.  trait AtomicFormula extends Formula with Atomic

    Atomic formulas that have no subformulas (but may still have subterms).

12.  case class AtomicODE(xp: DifferentialSymbol, e: Term) extends AtomicDifferentialProgram with Product with Serializable

    x'=e atomic differential equation where x is evolving for some time with time-derivative e.

13.  trait AtomicProgram extends Program with Atomic

    Atomic programs that have no subprograms (but may still have subterms or subformulas).

14.  trait AtomicTerm extends Term with Atomic

    Atomic terms that have no proper subterms.

15.  case class BaseVariable(name: String, index: Option[Int] = None, sort: Sort = Real) extends Variable with Product with Serializable

    Elementary variable called name with an index of a fixed sort (that is not a differential variable).

16.  trait BinaryComposite extends Composite

    Binary composite expressions that are composed of two subexpressions.

17.  trait BinaryCompositeFormula extends BinaryComposite with CompositeFormula

    Binary Composite Formulas, i.e.

    Binary Composite Formulas, i.e. formulas composed of two subformulas.

18.  trait BinaryCompositeProgram extends BinaryComposite with CompositeProgram

    Binary Composite Programs, i.e.

    Binary Composite Programs, i.e. programs composed of two subprograms.

19.  trait BinaryCompositeTerm extends BinaryComposite with CompositeTerm

    Binary Composite Terms, i.e.

    Binary Composite Terms, i.e. terms composed of two subterms.

20.  final case class BoundRenaming(what: Variable, repl: Variable, pos: SeqPos) extends PositionRule with Product with Serializable

    Performs bound renaming renaming all occurrences of variable what (and its associated DifferentialSymbol) to repl.

    Performs bound renaming renaming all occurrences of variable what (and its associated DifferentialSymbol) to repl. Proper bound renaming requires the replacement to be a fresh variable that does not occur previously.

     G |- [repl:=e]r(P), D
    ------------------------ BR (where what',repl,repl' do not occur in P)
     G |- [what:=e]P,    D

    where r(P) is the result of uniformly renaming what to the (fresh) repl in P. The proof rule works accordingly for diamond modalities, nondeterministic assignments, or quantifiers, or in the antecedent.

     G |- <repl:=e>r(P), D
    ------------------------ BR (where what',repl,repl' do not occur in P)
     G |- <what:=e>P,    D

     G |- \forall repl r(P), D
    --------------------------- BR (where what',repl,repl' do not occur in P)
     G |- \forall what P,    D

     G |- \exists repl r(P), D
    --------------------------- BR (where what',repl,repl' do not occur in P)
     G |- \exists what P,    D

     G, [repl:=e]r(P) |- D
    ------------------------ BR (where what',repl,repl' do not occur in P)
     G, [what:=e]P    |- D

    what

    What variable (and its associated DifferentialSymbol) to replace.

    repl

    The target variable to replace what with.

    pos

    The position at which to perform a bound renaming.

    Note

    soundness-critical: For bound renaming purposes semantic renaming would be unsound.

    See also

    UniformRenaming

    RenamingClashException

21.  case class Box(program: Program, child: Formula) extends Modal with Product with Serializable

    box modality all runs of program satisfy child: [program]child.

22.  case class Choice(left: Program, right: Program) extends BinaryCompositeProgram with Product with Serializable

    left++right nondeterministic choice running either left or right.

23.  case class Close(assume: AntePos, pos: SuccPos) extends Rule with Product with Serializable

    Close / Identity rule proving an assumption available in the antecedent.

    Close / Identity rule proving an assumption available in the antecedent.

           *
    ------------------ (Id)
      p, G |- p, D

24.  case class CloseFalse(pos: AntePos) extends LeftRule with Product with Serializable

    Close by false among the antecedent assumptions.

    Close by false among the antecedent assumptions.

           *
    ------------------ (close false)
      false, G |- D

25.  case class CloseTrue(pos: SuccPos) extends RightRule with Product with Serializable

    Close by true among the succedent desiderata.

    Close by true among the succedent desiderata.

          *
    ------------------ (close true)
      G |- true, D

26.  case class CoHide2(pos1: AntePos, pos2: SuccPos) extends Rule with Product with Serializable

    CoHide2 hides all but the two indicated positions.

    CoHide2 hides all but the two indicated positions.

         p |- q
    --------------- (CoHide2)
      p, G |- q, D

27.  case class CoHideLeft(pos: AntePos) extends LeftRule with Product with Serializable

    CoHide left.

    CoHide left.

         p |-
    ------------- (CoHide left)
      p, G |- D

    Note

    Rarely useful (except for contradictory p)

    ,

    Not used, just contained for symmetry reasons

28.  case class CoHideRight(pos: SuccPos) extends RightRule with Product with Serializable

    CoHide right.

    CoHide right.

        |- p
    ------------- (CoHide right)
      G |- p, D

29.  case class CommuteEquivLeft(pos: AntePos) extends LeftRule with Product with Serializable

    Commute equivalence left

    Commute equivalence left

    q<->p, G |-  D
    -------------- (<->cL)
    p<->q, G |-  D

    Note

    Not used, just contained for symmetry reasons

30.  case class CommuteEquivRight(pos: SuccPos) extends RightRule with Product with Serializable

    Commute equivalence right

    Commute equivalence right

    G |- q<->p, D
    ------------- (<->cR)
    G |- p<->q, D

31.  trait ComparisonFormula extends AtomicFormula with BinaryComposite

    Atomic comparison formula composed of two terms.

32.  case class Compose(left: Program, right: Program) extends BinaryCompositeProgram with Product with Serializable

    left;right sequential composition running right after left.

33.  trait Composite extends Expression

    Composite expressions that are composed of subexpressions

34.  trait CompositeFormula extends Formula with Composite

    Composite formulas composed of subformulas.

35.  trait CompositeProgram extends Program with Composite

    Composite programs that are composed of subprograms.

36.  trait CompositeTerm extends Term with Composite

    Composite terms that are composed of subterms.

37.  class CoreException extends ProverException

    Reasoning exceptions directly from the KeYmaera X Prover Kernel.

    Reasoning exceptions directly from the KeYmaera X Prover Kernel. The most important distinction of prover kernel exceptions are CriticalCoreException for unsound logical mistakes versus NoncriticalCoreException for plausible but inappropriate reasoning attempts.

38.  class CriticalCoreException extends CoreException

    Critical reasoning exceptions directly from the KeYmaera X Prover Core that indicate a proof step was attempted that would be unsound, and was consequently denied.

39.  case class Cut(c: Formula) extends Rule with Product with Serializable

    Cut in the given formula c to use c on the first branch and proving c on the second branch.

    Cut in the given formula c to use c on the first branch and proving c on the second branch.

    G, c |- D     G |- D, c
    ----------------------- (cut)
            G |- D

    The ordering of premises is optimistic, i.e., the premise using the cut-in formula c comes before the one proving c.

    Note

    c will be added at the end on the subgoals

40.  case class CutLeft(c: Formula, pos: AntePos) extends Rule with Product with Serializable

    Cut in the given formula c in place of p on the left.

    Cut in the given formula c in place of p on the left.

    c, G |- D    G |- D, p->c
    ------------------------- (Cut Left)
           p, G |- D

    Forward Hilbert style rules can move further away, implicationally, from the sequent implication. Backwards tableaux style sequent rules can move closer, implicationally, toward the sequent implication.

    Note

    this would perhaps surprising that inconsistent posititioning within this rule, unlike in ImplyLeft?

41.  case class CutRight(c: Formula, pos: SuccPos) extends Rule with Product with Serializable

    Cut in the given formula c in place of p on the right.

    Cut in the given formula c in place of p on the right.

    G |- c, D    G |- c->p, D
    ------------------------- (Cut right)
           G |- p, D

    Forward Hilbert style rules can move further away, implicationally, from the sequent implication. Backwards tableaux style sequent rules can move closer, implicationally, toward the sequent implication.

42.  case class Diamond(program: Program, child: Formula) extends Modal with Product with Serializable

    diamond modality some run of program satisfies child: ⟨program⟩child.

43.  case class Differential(child: Term) extends RUnaryCompositeTerm with Product with Serializable

    (child)' differential of the term child.

    (child)' differential of the term child.

    See also

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

44.  case class DifferentialFormula(child: Formula) extends UnaryCompositeFormula with Product with Serializable

    Differential formula are differentials of formulas in analogy to differential terms (child)'.

    Differential formula are differentials of formulas in analogy to differential terms (child)'. In theory they are only used in the form (e>=k)' which is (e)'>=(k)'. In practice, derived forms are useful.

45.  final class DifferentialProduct extends DifferentialProgram with BinaryComposite

    left,right parallel product of differential programs.

    left,right parallel product of differential programs. This data structure automatically left-reassociates to list form so that left never is a Differential Product. DifferentialProduct(AtomicDifferentialProgram, DifferentialProduct(AtomicDifferentialProgram, ....))

    Note

    This is a case class except for an override of the apply function to ensure left-associative representation.

    ,

    Private constructor so only DifferentialProduct.apply can ever create this, which will re-associate et al.

46.  sealed trait DifferentialProgram extends Program

    Differential programs of differential dynamic logic.

    Differential programs of differential dynamic logic.

    Differential Programs are of the form

    • AtomicDifferentialProgram atomic differential programs are not composed of other differential programs
      • x'=e atomic differential equation as AtomicODE(DifferentialSymbol,Term)
      • c differential program constant as DifferentialProgramConst
    • BinaryCompositeDifferentialProgram except it's the only composition for differential programs.
      • c,d differential product as DifferentialProduct(DifferentialProgram], DifferentialProgram])

    See also

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.differentialProgramParser

47.  case class DifferentialProgramConst(name: String, space: Space = AnyArg) extends AtomicDifferentialProgram with SpaceDependent with NamedSymbol with Product with Serializable

    Uninterpreted differential program constant, limited to the given state space.

    Uninterpreted differential program constant, limited to the given state space. The semantics of arity 0 DifferentialProgramConst symbol is looked up by the state, with the additional promise that taboos are neither free nor bound, so the run does not depend on the value of taboos nor does the value of taboos change when space=Except(taboos).

    space

    The part of the state space that the interpretation/replacement of this symbol is limited to have free or bound. AnyArg is the default allowing full read/write access to the state. Taboo(x) means x can neither be free nor bound.

48.  case class DifferentialSymbol(x: Variable) extends Variable with RTerm with Product with Serializable

    Differential symbol x' for variable x.

    Differential symbol x' for variable x. Differential symbols are also called differential variables, because they are symbolic but are also variables.

49.  case class Divide(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable

    / real division of reals where right nonzero.

50.  case class DotTerm(s: Sort = Real, idx: Option[Int] = None) extends Expression with NamedSymbol with AtomicTerm with Product with Serializable

    •: Placeholder for terms in uniform substitutions of given sort.

    •: Placeholder for terms in uniform substitutions of given sort. Reserved nullary function symbols \\cdot for uniform substitutions are unlike ordinary function symbols by convention.

51.  case class Dual(child: Program) extends UnaryCompositeProgram with Product with Serializable

    child^d dual program continuing game child after passing control to the opponent.

52.  implicit final class Ensures[A] extends AnyVal

    Contracts (like scala.Predef.Ensuring) implemented with Java-style assertions (see assertion)

53.  case class Equal(left: Term, right: Term) extends ComparisonFormula with Product with Serializable

    = equality left = right.

54.  case class Equiv(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable

    <-> logical biimplication: equivalent.

55.  case class EquivLeft(pos: AntePos) extends LeftRule with Product with Serializable

    <->L Equiv left.

    <->L Equiv left.

    p&q, G |- D    !p&!q, G |- D
    ----------------------------- (<-> Equiv left)
      p<->q, G |- D

    Note

    Positions remain stable when decomposed this way around.

56.  case class EquivRight(pos: SuccPos) extends RightRule with Product with Serializable

    <->R Equiv right.

    <->R Equiv right.

    G, p |- D, q    G, q |- D, p
    ----------------------------- (<->R Equiv right)
      G |- p<->q, D

57.  case class EquivifyRight(pos: SuccPos) extends RightRule with Product with Serializable

    Equivify Right: Convert implication to equivalence.

    Equivify Right: Convert implication to equivalence.

    G |- a<->b, D
    -------------
    G |- a->b,  D

58.  case class Except(taboos: Seq[Variable]) extends Space with Product with Serializable

    The sort denoting a slice of the state space that does not include/depend on/affect variables taboos.

59.  case class ExchangeLeftRule(pos1: AntePos, pos2: AntePos) extends Rule with Product with Serializable

    Exchange left rule reorders antecedent.

    Exchange left rule reorders antecedent.

    q, p, G |- D
    ------------- (Exchange left)
    p, q, G |- D

60.  case class ExchangeRightRule(pos1: SuccPos, pos2: SuccPos) extends Rule with Product with Serializable

    Exchange right rule reorders succedent.

    Exchange right rule reorders succedent.

    G |- q, p, D
    ------------- (Exchange right)
    G |- p, q, D

61.  case class Exists(vars: Seq[Variable], child: Formula) extends Quantified with Product with Serializable

    \exists vars existentially quantified formula for some real value of vars.

62.  sealed trait Expression extends AnyRef

    Expressions of differential dynamic logic.

    Expressions of differential dynamic logic. Expressions are categorized according to the syntactic categories of the grammar of differential dynamic logic:

    1. terms are of type edu.cmu.cs.ls.keymaerax.core.Term of kind edu.cmu.cs.ls.keymaerax.core.TermKind 2. formulas are of type edu.cmu.cs.ls.keymaerax.core.Formula of kind edu.cmu.cs.ls.keymaerax.core.FormulaKind 3. hybrid programs are of type edu.cmu.cs.ls.keymaerax.core.Program of kind edu.cmu.cs.ls.keymaerax.core.ProgramKind 4. differential programs are of type edu.cmu.cs.ls.keymaerax.core.DifferentialProgram of kind edu.cmu.cs.ls.keymaerax.core.DifferentialProgramKind 5. function symbols are degenerate expressions that are syntactically incomplete, since not yet applied to arguments via FuncOf to form a term or via PredOf or PredicationalOf to form a formula.

    See Section 2.1

    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. Logical Foundations of Cyber-Physical Systems. Springer, 2018.

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.apply

    Syntax of differential dynamic logic

    Grammar

    Wiki

    Term

    Formula

    Program

    DifferentialProgram

63.  case class Forall(vars: Seq[Variable], child: Formula) extends Quantified with Product with Serializable

    \forall vars universally quantified formula for all real values of vars.

64.  sealed trait Formula extends Expression

    Formulas of differential dynamic logic.

    Formulas of differential dynamic logic. Also includes formulas of differential game logic, which only differ in the permitted mention of Dual.

    Formulas are of the form

    • AtomicFormula atomic formulas that are not composed of other formulas
      • true truth as True and false as False
      • P nullary predicational as UnitPredicational written P(||) in internal syntax.
      • _ dot as reserved nullary predicational DotFormula for formula argument placeholders
    • ComparisonFormula are AtomicFormula composed of two terms but not composed of formulas
      • e>=d comparisons as GreaterEqual(Term,Term) and likewise Equal, NotEqual, Greater, LessEqual, Less
    • ApplicationOf predicate applications
      • p(e) predicate application as PredOf(Function, Term)
      • P{Q} predicational application or quantifier symbol as PredicationalOf(Function, Formula)
    • UnaryCompositeFormula unary composite formulas composed of one child formula
      • !P logical negation as Not(Formula)
      • (P)' differential formula as DifferentialFormula(Formula])
    • BinaryCompositeFormula binary composite formulas composed of a left and a right formula
      • P&Q conjunction as And(Formula], Formula])
      • P|Q disjunction as Or(Formula], Formula])
      • P->Q implication as Imply(Formula], Formula])
      • P<->Q biimplication as Equiv(Formula], Formula])
    • Quantified quantified formulas quantifying a variable
      • \forall x P universal quantification as Forall(Variable], Formula])
      • \exists x P existential quantification as Exists(Variable], Formula])
    • Modal modal formulas with a program and a formula child
      • [a]P box modality application for all runs as Box(Program], Formula])
      • ⟨a⟩P diamond modality application for some run as Diamond(Program], Formula])

    See also

    edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.formulaParser

65.  case class FuncOf(func: Function, child: Term) extends CompositeTerm with ApplicationOf with Product with Serializable

    Function symbol applied to argument child func(child).

66.  case class Function(name: String, index: Option[Int] = None, domain: Sort, sort: Sort, interp: Option[Formula] = None) extends NamedSymbol with Product with Serializable

    Function symbol or predicate symbol or predicational symbol name_index:domain->sort

    Function symbol or predicate symbol or predicational symbol name_index:domain->sort

    domain

    the sort of expected arguments.

    sort

    the sort resulting when this function/predicate/predicational symbol has been applied to an argument.

    interp

    if present, this function symbol f has a fixed interpretation defined by

    y = f(x) <-> P(y,x)

    where P is the interp formula, substituting (y,x) for the dot terms. That is

    ._0 = f(._1) <-> P(._0,._1)

67.  case class Greater(left: Term, right: Term) extends RComparisonFormula with Product with Serializable

    > greater than comparison left > right of reals.

68.  case class GreaterEqual(left: Term, right: Term) extends RComparisonFormula with Product with Serializable

    >= greater or equal comparison left >= right of reals.

69.  case class HideLeft(pos: AntePos) extends LeftRule with Product with Serializable

    Hide left.

    Hide left.

        G |- D
    ------------- (Weaken left)
     p, G |- D

70.  case class HideRight(pos: SuccPos) extends RightRule with Product with Serializable

    Hide right.

    Hide right.

       G |- D
    ------------- (Weaken right)
       G |- p, D

71.  case class Imply(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable

    -> logical implication: implies.

72.  case class ImplyLeft(pos: AntePos) extends LeftRule with Product with Serializable

    ->L Imply left.

    ->L Imply left.

    G |- D, p    q, G |- D
    ---------------------- (-> Imply left)
      p->q, G |- D

73.  case class ImplyRight(pos: SuccPos) extends RightRule with Product with Serializable

    ->R Imply right.

    ->R Imply right.

      G, p |- D, q
    --------------- (->R Imply right)
      G |- p->q, D

74.  case class InapplicableRuleException(msg: String, r: Rule, s: Sequent = null) extends NoncriticalCoreException with Product with Serializable

    Rule is not applicable as indicated.

    Rule is not applicable as indicated. For example, InapplicableRuleException can be raised when trying to apply AndRight at the correct position 2 in bounds on the right-hand side where it turns out there is an Or formula not an And formula. For readability and code performance reasons, the prover kernel may also raise scala.MatchError if the shape of a formula is not as expected, but core tactics will then convert MatchError to InapplicableRuleException.

    See also

    Rule

    Close

    CloseFalse

    CloseTrue

    Skolemize

75.  sealed trait Kind extends AnyRef

    Kinds of expressions (term, formula, program, differential program).

    Kinds of expressions (term, formula, program, differential program).

    See also

    Expression

76.  trait LeftRule extends PositionRule

    A rule applied to a position in the antecedent on the left of a sequent.

    A rule applied to a position in the antecedent on the left of a sequent. LeftRules can only be applied to antecedent positions.

    See also

    AntePos

77.  case class Less(left: Term, right: Term) extends RComparisonFormula with Product with Serializable

    <= less than comparison left < right of reals.

78.  case class LessEqual(left: Term, right: Term) extends RComparisonFormula with Product with Serializable

    < less or equal comparison left <= right of reals.

79.  case class Loop(child: Program) extends UnaryCompositeProgram with Product with Serializable

    child* nondeterministic repetition running child arbitrarily often.

80.  case class Minus(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable

    - binary subtraction of reals.

81.  trait Modal extends CompositeFormula

    Modal formulas.

82.  trait NamedSymbol extends Expression with Ordered[NamedSymbol]

    A named symbol such as a variable or function symbol or predicate symbol or program constant symbol.

    A named symbol such as a variable or function symbol or predicate symbol or program constant symbol.

    Note

    User-level symbols should not use underscores, which are reserved for the core.

83.  case class Neg(child: Term) extends RUnaryCompositeTerm with Product with Serializable

    - unary negation of reals: minus.

84.  class NoncriticalCoreException extends CoreException

    Noncritical reasoning exceptions directly from the KeYmaera X Prover Core that indicate a proof step was perfectly plausible to try, just did not fit the expected pattern, and consequently turned out impossible.

85.  case class Not(child: Formula) extends UnaryCompositeFormula with Product with Serializable

    ! logical negation: not.

86.  case class NotEqual(left: Term, right: Term) extends ComparisonFormula with Product with Serializable

    != disequality left != right.

87.  case class NotLeft(pos: AntePos) extends LeftRule with Product with Serializable

    !L Not left.

    !L Not left.

      G |- D, p
    ------------ (!L Not left)
     !p, G |- D

88.  case class NotRight(pos: SuccPos) extends RightRule with Product with Serializable

    !R Not right.

    !R Not right.

      G, p |- D
    ------------ (!R Not right)
      G |- !p, D

89.  case class Number(value: BigDecimal) extends AtomicTerm with RTerm with Product with Serializable

    Number literal such as 0.5 or 42 etc.

90.  case class ODESystem(ode: DifferentialProgram, constraint: Formula = True) extends Program with Product with Serializable

    Differential equation system ode with given evolution domain constraint.

91.  case class ObjectSort(name: String) extends Sort with Product with Serializable

    User-defined object sort.

92.  case class Or(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable

    | logical disjunction: or.

93.  case class OrLeft(pos: AntePos) extends LeftRule with Product with Serializable

    |L Or left.

    |L Or left.

    p, G |- D     q, G |- D
    ----------------------- (|L Or left)
      p|q, G |- D

94.  case class OrRight(pos: SuccPos) extends RightRule with Product with Serializable

    |R Or right.

    |R Or right.

      G |- D, p,q
    --------------- (|R Or right)
      G |- p|q, D

95.  case class Pair(left: Term, right: Term) extends BinaryCompositeTerm with Product with Serializable

    Pairs (left,right) for binary Function and FuncOf and PredOf.

    Pairs (left,right) for binary Function and FuncOf and PredOf.

    Note

    By convention, pairs are usually used in right-associative ways. That is, n-ary argument terms (t1,t2,t3,...tn) are represented as (t1,(t2,(t3,...tn))). This is not a strict requirement, but the default parse and suggested use.

96.  case class Plus(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable

    + binary addition of reals.

97.  trait PositionRule extends Rule

    A rule applied to a position in a sequent.

    A rule applied to a position in a sequent.

    See also

    SeqPos

98.  case class Power(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable

    real exponentiation or power: left^right.

    real exponentiation or power: left^right.

    Note

    By mathematical conventions, powers are parsed in right-associative ways. That is, x⁴2 is parsed as x⁽⁴2).

99.  case class PredOf(func: Function, child: Term) extends AtomicFormula with ApplicationOf with Product with Serializable

    Predicate symbol applied to argument child func(child) where func is Boolean-valued .

100.  case class PredicationalOf(func: Function, child: Formula) extends AtomicFormula with ApplicationOf with StateDependent with Product with Serializable

     Predicational or quantifier symbol applied to argument formula child, written C{child}.

     Predicational or quantifier symbol applied to argument formula child, written C{child}. Predicationals are similar to predicate symbol applications, except that they accept a formula as an argument rather than a term. Also, their truth-value may depend on the entire truth table of child at any state.

     Note

     In theory, C{child} is written C(child).

101.  sealed trait Program extends Expression

     Hybrid programs of differential dynamic logic.

     Hybrid programs of differential dynamic logic. Also includes hybrid games of differential game logic, which only differ in the permitted mention of Dual.

     Hybrid Programs are of the form

     • AtomicProgram atomic programs that are not composed of other programs
       • x:=e assignment as Assign(Variable,Term) and likewise differential assignment x':=e as Assign(DifferentialSymbol,Term)
       • x:=* nondeterministic assignment as AssignAny(Variable) and likewise nondeterministic differential assignment x':=* as AssignAny(DifferentialSymbol)
       • a program constant as ProgramConst written a{|^x|} if x taboo.
       • a system constant as SystemConst without games, written a{|^@|} in internal syntax.
       • ?P test as Test(Formula)
     • BinaryCompositeProgram binary composite programs composed of a left and right program
       • a++b nondeterministic choice as Choice(Program], Program])
       • a;b sequential composition as Compose(Program], Program])
     • UnaryCompositeProgram unary composite programs composed of a child program
       • {a}* nondeterministic repetition as Loop(Program])
       • {a}^@ dual game as Dual(Program]) for hybrid games of differential game logic.
     • Special
       • {c&Q} differential equation system as ODESystem(DifferentialProgram, Formula)

     See also

     edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.programParser

102.  case class ProgramConst(name: String, space: Space = AnyArg) extends NamedSymbol with AtomicProgram with SpaceDependent with Product with Serializable

     Uninterpreted program constant symbol / game symbol, possibly limited to the given state space.

     Uninterpreted program constant symbol / game symbol, possibly limited to the given state space. The semantics of ProgramConst symbol is looked up by the state, with the additional promise that taboos are neither free nor bound, so the run does not depend on the value of taboos nor does the value of taboos change when space=Except(taboos).

     space

     The part of the state space that the interpretation/replacement of this symbol is limited to have free or bound.

     • AnyArg is the default allowing full read/write access to the state.
     • Taboo(x) means x can neither be free nor bound. Written a{|x|} in internal syntax.

     Note

     In theory, a; is written a. By analogy, a{|x|} has read/write access to the entire state except the taboo x.

103.  final case class Provable extends Product with Serializable

     Provable(conclusion, subgoals) is the proof certificate representing certified provability of conclusion from the premises in subgoals.

     Provable(conclusion, subgoals) is the proof certificate representing certified provability of conclusion from the premises in subgoals. If subgoals is an empty list, then conclusion is provable. Otherwise conclusion is provable from the set of all assumptions in subgoals.

      G1 |- D1 ... Gn |- Dn    (subgoals)
     -----------------------
              G |- D           (conclusion)

     Invariant: All Provables ever produced are locally sound, because only the prover kernel can create Provable objects and chooses not to use the globally sound uniform substitution rule.

     Provables are stateless and do not themselves remember other provables that they resulted from. The ProofTree data structure outside the kernel provides such proof tree navigation information.

     Examples:

     1. Proofs can be constructed in (backward/tableaux) sequent order using Provables:

        import scala.collection.immutable._
        val verum = new Sequent(IndexedSeq(), IndexedSeq(True))
        // conjecture
        val provable = Provable.startProof(verum)
        // construct a proof
        val proof = provable(CloseTrue(SuccPos(0)), 0)
        // check if proof successful
        if (proof.isProved) println("Successfully proved " + proof.proved)

     ,

     2. Multiple Provable objects for subderivations obtained from different sources can also be merged

        // ... continuing other example
        val more = new Sequent(IndexedSeq(),
          IndexedSeq(Imply(Greater(Variable("x"), Number(5)), True)))
        // another conjecture
        val moreProvable = Provable.startProof(more)
        // construct another (partial) proof
        val moreProof = moreProvable(ImplyRight(SuccPos(0)), 0)(HideLeft(AntePos(0)), 0)
        // merge proofs by gluing their Provables together
        val mergedProof = moreProof(proof, 0)
        // check if proof successful
        if (mergedProof.isProved) println("Successfully proved " + mergedProof.proved)

     ,

     3. Proofs in backward tableaux sequent order are straight-forward

        import scala.collection.immutable._
        val fm = Greater(Variable("x"), Number(5))
        // |- x>5 -> x>5 & true
        val finGoal = new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True))))
        // conjecture
        val finProvable = Provable.startProof(finGoal)
        // construct a proof
        val proof = finProvable(
          ImplyRight(SuccPos(0)), 0)(
            AndRight(SuccPos(0)), 0)(
            HideLeft(AntePos(0)), 1)(
            CloseTrue(SuccPos(0)), 1)(
            Close(AntePos(0), SuccPos(0)), 0)
        // proof of finGoal
        println(proof.proved)

     ,

     4. Proofs in forward Hilbert order are straightforward with merging of branches

        import scala.collection.immutable._
        val fm = Greater(Variable("x"), Number(5))
        // proof of x>5 |- x>5 & true merges left and right branch by AndRight
        val proof = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(And(fm, True))))(
          AndRight(SuccPos(0)), 0) (
          // left branch: x>5 |- x>5
          Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(fm)))(
            Close(AntePos(0), SuccPos(0)), 0),
          0) (
          //right branch: |- true
          Provable.startProof(Sequent(IndexedSeq(), IndexedSeq(True)))(
            CloseTrue(SuccPos(0)), 0)(
              // x>5 |- true
              Sequent(IndexedSeq(fm), IndexedSeq(True)), HideLeft(AntePos(0))),
          0) (
          // |- x>5 -> x>5 & true
          new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True)))),
          ImplyRight(SuccPos(0))
        )
        // proof of finGoal:  |- x>5 -> x>5 & true
        println(proof.proved)

     ,

     5. Proofs in Hilbert-calculus style order can also be based exclusively on subsequent merging

        import scala.collection.immutable._
        val fm = Greater(Variable("x"), Number(5))
        // x>0 |- x>0
        val left = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(fm)))(
          Close(AntePos(0), SuccPos(0)), 0)
        // |- true
        val right = Provable.startProof(Sequent(IndexedSeq(), IndexedSeq(True)))(
          CloseTrue(SuccPos(0)), 0)
        val right2 = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(True)))(
          HideLeft(AntePos(0)), 0) (right, 0)
        // gluing order for subgoals is irrelevant. Could use: (right2, 1)(left, 0))
        val merged = Provable.startProof(Sequent(IndexedSeq(fm), IndexedSeq(And(fm, True))))(
          AndRight(SuccPos(0)), 0) (
          left, 0)(
            right2, 0)
        // |- x>5 -> x>5 & true
        val finGoal = new Sequent(IndexedSeq(), IndexedSeq(Imply(fm, And(fm, True))))
        val proof = Provable.startProof(finGoal)(
          ImplyRight(SuccPos(0)), 0) (merged, 0)
        // proof of finGoal
        println(proof.proved)

     ,

     6. Branching proofs in backward tableaux sequent order are straight-forward, yet might become more readable when closing branches right-to-left to keep explicit subgoals:

        // 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)
        )

     Note

     soundness-critical logical framework.

     ,

     Only private constructor calls for soundness

     ,

     For soundness: No reflection should bypass constructor call privacy, nor reflection to bypass immutable val algebraic data types.

     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.Provable.startProof(goal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Sequent):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

     edu.cmu.cs.ls.keymaerax.core.Provable.axioms

     edu.cmu.cs.ls.keymaerax.core.Provable.rules

     edu.cmu.cs.ls.keymaerax.core.Provable.proveArithmetic

     edu.cmu.cs.ls.keymaerax.core.Provable.fromStorageString(storedProvable:String):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

104.  class ProvableStorageException extends CoreException

     Exception indicating that a Provable Storage representation as a String cannot be read, because it has been tampered with.

     Exception indicating that a Provable Storage representation as a String cannot be read, because it has been tampered with.

     See also

     Provable.fromStorageString

105.  case class ProverAssertionError(msg: String) extends ProverException with Product with Serializable

     Internal core assertions that fail in the prover

106.  class ProverException extends RuntimeException

     KeYmaera X Prover Exceptions.

107.  trait QETool extends AnyRef

     Interface to quantifier elimination tools.

108.  trait Quantified extends CompositeFormula

     Quantified formulas.

109.  case class RenamingClashException(msg: String, ren: String, e: String, info: String = "") extends CriticalCoreException with Product with Serializable

     Uniform or bound renaming clashes are unsound renaming reasoning attempts.

     Uniform or bound renaming clashes are unsound renaming reasoning attempts.

     See also

     BoundRenaming

     UniformRenaming

     URename

     edu.cmu.cs.ls.keymaerax.core.Provable.apply(ren:edu\.cmu\.cs\.ls\.keymaerax\.core\.URename):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

110.  trait RightRule extends PositionRule

     A rule applied to a position in the succedent on the right of a sequent.

     A rule applied to a position in the succedent on the right of a sequent. RightRules can only be applied to succedent positions.

     See also

     SuccPos

111.  sealed trait Rule extends (Sequent) ⇒ List[Sequent]

     Subclasses represent all built-in proof rules.

     Subclasses represent all built-in proof rules. A proof rule is ultimately a named mapping from sequents to lists of sequents. The resulting list of sequents represent the subgoals/premises all of which need to be proved to prove the current sequent (desired conclusion).

     Note

     soundness-critical This class is sealed, so no rules can be added outside Proof.scala

     See also

     Provable.rules

112.  sealed trait SeqPos extends AnyRef

     Position of a formula in a sequent, i.e.

     Position of a formula in a sequent, i.e. antecedent or succedent positions.

     See also

     SeqPos$.apply(signedPos:Int):edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos*

     Sequent.apply(pos:edu\.cmu\.cs\.ls\.keymaerax\.core\.SeqPos):edu\.cmu\.cs\.ls\.keymaerax\.core\.Formula*

     AntePos

     SuccPos

113.  final case class Sequent(ante: IndexedSeq[Formula], succ: IndexedSeq[Formula]) extends Product with Serializable

     Sequent ante |- succ with antecedent ante and succedent succ.

     Sequent ante |- succ with antecedent ante and succedent succ.

     ante(0),ante(1),...,ante(n) |- succ(0),succ(1),...,succ(m)

     This sequent is often pretty-printed with signed line numbers:

         -1: ante(0)
         -2: ante(1)
             ...
     -(n+1): ante(n)
      ==> 1: succ(0)
          2: succ(1)
             ...
      (m+1): succ(m)

     The semantics of sequent ante |- succ is the conjunction of the formulas in ante implying the disjunction of the formulas in succ.

     ante

     The ordered list of antecedents of this sequent whose conjunction is assumed.

     succ

     The orderd list of succedents of this sequent whose disjunction needs to be shown.

     See also

     Andre Platzer. Differential dynamic logic for hybrid systems. Journal of Automated Reasoning, 41(2), pages 143-189, 2008.

114.  sealed trait SetLattice[A] extends AnyRef

     Lattice of sets, i.e.

     Lattice of sets, i.e. the lattice of sets that also includes bottom, top and near-top elements.

     A

     Type of elements in the set

115.  case class SkolemClashException(msg: String, clashedNames: SetLattice[Variable], vars: String, s: String) extends CriticalCoreException with Product with Serializable

     Skolem symbol clashes are unsound Skolemization reasoning attempts.

     Skolem symbol clashes are unsound Skolemization reasoning attempts.

     See also

     Skolemize

116.  case class Skolemize(pos: SeqPos) extends PositionRule with Product with Serializable

     Skolemization assumes that the names of the quantified variables to be skolemized are unique within the sequent.

     Skolemization assumes that the names of the quantified variables to be skolemized are unique within the sequent. This can be ensured by finding a unique name and renaming the bound variable through alpha conversion.

     G |- p(x), D
     ----------------------- (Skolemize) provided x not in G,D
     G |- \forall x p(x), D

     Skolemization also handles existential quantifiers on the left:

               p(x), G |- D
     ------------------------ (Skolemize) provided x not in G,D
     \exists x p(x), G |- D

     Note

     Could in principle replace by uniform substitution rule application mechanism for rule "all generalization" along with tactics expanding scope of quantifier with axiom "all quantifier scope" at the cost of propositional repacking and unpacking. p(x) ---------------all generalize \forall x. p(x) Kept because of the incurred cost.

     See also

     SkolemClashException

117.  sealed trait Sort extends AnyRef

     Sorts of expressions (real, bool, etc).

     Sorts of expressions (real, bool, etc).

     See also

     Expression

118.  sealed trait Space extends AnyRef

     Sorts of state spaces for state-dependent operators.

     Sorts of state spaces for state-dependent operators.

     See also

     SpaceDependent

119.  trait SpaceDependent extends StateDependent

     Expressions limited to a given sub state-space of only some variables and differential variables.

     Expressions limited to a given sub state-space of only some variables and differential variables.

     Since

     4.2

120.  trait StateDependent extends Expression

     Expressions whose semantic interpretations have access to the state.

     Expressions whose semantic interpretations have access to the state.

     Note

     Not soundness-critical, merely speeds up matching in SubstitutionPair.freeVars.

121.  case class SubderivationSubstitutionException(subderivation: String, conclusion: String, subgoal: String, subgoalid: Int, provable: String) extends CriticalCoreException with Product with Serializable

     Exceptions that arise from trying to substitute a subderivation in for a subgoal that does not equal the conclusion of the subderivation.

     Exceptions that arise from trying to substitute a subderivation in for a subgoal that does not equal the conclusion of the subderivation.

     See also

     edu.cmu.cs.ls.keymaerax.core.Provable.apply(rule:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable,subgoal:edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable\.Subgoal):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

122.  case class SubstitutionClashException(subst: String, U: String, e: String, context: String, clashes: String, info: String = "") extends CriticalCoreException with Product with Serializable

     Substitution clashes are raised for unsound substitution reasoning attempts.

     Substitution clashes are raised for unsound substitution reasoning attempts.

     See also

     USubstOne

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

123.  final case class SubstitutionPair(what: Expression, repl: Expression) extends Product with Serializable

     Representation of a substitution replacing what with repl uniformly, everywhere.

     Representation of a substitution replacing what with repl uniformly, everywhere. Data structure invariant: Only substitutable expressions will be accepted for what with compatible repl.

     what

     the expression to be replaced. what can have one of the following forms:

     • PredOf(p:Function, DotTerm/Nothing/Nested Pair of DotTerm)
     • FuncOf(f:Function, DotTerm/Nothing/Nested Pair of DotTerm)
     • ProgramConst or DifferentialProgramConst or SystemConst
     • UnitPredicational
     • UnitFunctional
     • PredicationalOf(p:Function, DotFormula)
     • DotTerm
     • DotFormula

     repl

     the expression to be used in place of what.

     See also

     USubstOne

     USubstChurch

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

     Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425-441. Springer, 2019.

124.  case class SuccPos extends SeqPos with Product with Serializable

     Antecedent Positions of formulas in a sequent, i.e.

     Antecedent Positions of formulas in a sequent, i.e. on the right of the sequent arrow.

125.  case class SystemConst(name: String, space: Space = AnyArg) extends NamedSymbol with AtomicProgram with SpaceDependent with Product with Serializable

     Uninterpreted hybrid system program constant symbols that are NOT hybrid games, limited to the given state space.

     Uninterpreted hybrid system program constant symbols that are NOT hybrid games, limited to the given state space. Written a{|^@|} in internal syntax.

     space

     The part of the state space that the interpretation/replacement of this symbol is limited to have free or bound.

     • AnyArg is the default allowing full read/write access to the state.
     • Taboo(x) means x can neither be free nor bound. Written a{|^@x|} in internal syntax.

     Since

     4.7.4 also SpaceDependent with space parameter.

126.  sealed trait Term extends Expression

     Terms of differential dynamic logic.

     Terms of differential dynamic logic. Also terms of differential game logic, which only differ in the permitted mention of Dual.

     Terms are of the form

     • AtomicTerm atomic terms are not composed of other terms
       • x variable as Variable, including differential symbol x' as DifferentialSymbol
       • 5 number literals as Number
       • F nullary functional as UnitFunctional written F(||) in internal syntax.
       • . dot as reserved nullary function symbol DotTerm for term argument placeholders
       • Nothing for empty arguments Nothing for nullary functions
     • ApplicationOf terms that are function applications
       • f(e) function application as FuncOf(Function, Term)
     • UnaryCompositeTerm unary composite terms composed of one child term
       • -e negation as Neg(Term)
       • (e)' differential as Differential(Term)
     • BinaryCompositeTerm binary composite terms composed of two children terms
       • e+d addition as Plus(Term, Term)
       • e-d subtraction as Minus(Term, Term)
       • e*d multiplication as Times(Term, Term)
       • e/d division as Divide(Term, Term)
       • e^d power as Power(Term, Term)
       • (e,d) for pair as Pair for arguments

     See also

     edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser.termParser

     Syntax of differential dynamic logic

127.  case class Test(cond: Formula) extends AtomicProgram with Product with Serializable

     ?cond test a formula as a condition on the current state.

128.  case class Times(left: Term, right: Term) extends RBinaryCompositeTerm with Product with Serializable

     * binary multiplication of reals.

129.  case class Tuple(left: Sort, right: Sort) extends Sort with Product with Serializable

     Tuple sort for Pair.

130.  final case class URename(what: Variable, repl: Variable, semantic: Boolean = false) extends (Expression) ⇒ Expression with Product with Serializable

     Uniformly rename all occurrences of what and what' to repl and repl' and vice versa, but clash for program constants etc.

     Uniformly rename all occurrences of what and what' to repl and repl' and vice versa, but clash for program constants etc. Uniformly rename all occurrences of variable what (and its associated DifferentialSymbol what') to repl (and its associated DifferentialSymbol repl') everywhere and vice versa uniformly rename all occurrences of variable repl (and its associated DifferentialSymbol) to what (and what'). Uniform renaming, thus, is a transposition.

     what

     What variable to replace (along with its associated DifferentialSymbol).

     repl

     The target variable to replace what with and vice versa.

     semantic

     true to allow semantic renaming of SpaceDependent symbols, which preserves local soundness when applied to inferences.

     Note

     soundness-critical

     See also

     UniformRenaming

     BoundRenaming

     Provable.apply(ren:edu\.cmu\.cs\.ls\.keymaerax\.core\.URename):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

131.  type USubst = USubstOne

     The uniform substitution type to use

132.  final case class USubstOne(subsDefsInput: Seq[SubstitutionPair]) extends (Expression) ⇒ Expression with Product with Serializable

     A Uniform Substitution with its one-pass application mechanism.

     A Uniform Substitution with its one-pass application mechanism. 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 predicational / quantifier symbols C(-) by a formula in (-) and all occurrences of program constant symbol b by a hybrid program.

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

     Since

     4.7

     Note

     Implements the one-pass version that checks admissibility on the fly and checking upon occurrence. Faster than the alternative USubstChurch. Main ingredient of prover core.

     ,

     soundness-critical

     See also

     Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425-441. Springer, 2019.

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

     USubstChurch

133.  trait UnaryComposite extends Composite

     Unary composite expressions that are composed of one subexpression.

134.  trait UnaryCompositeFormula extends UnaryComposite with CompositeFormula

     Unary Composite Formulas, i.e.

     Unary Composite Formulas, i.e. formulas composed of one subformula.

135.  trait UnaryCompositeProgram extends UnaryComposite with CompositeProgram

     Unary Composite Programs, i.e.

     Unary Composite Programs, i.e. programs composed of one subprogram.

136.  trait UnaryCompositeTerm extends UnaryComposite with CompositeTerm

     Unary Composite Terms, i.e.

     Unary Composite Terms, i.e. terms composed of one real subterm.

137.  final case class UniformRenaming(what: Variable, repl: Variable) extends Rule with Product with Serializable

     Uniformly rename all occurrences of what and what' to repl and repl' and vice versa.

     Uniformly rename all occurrences of what and what' to repl and repl' and vice versa. Uniformly rename all occurrences of variable what (and its associated DifferentialSymbol) to repl. Uniform renaming, thus, is a transposition.

      r(G) |- r(D)
     --------------- UR
         G |- D

     what

     What variable to replace (along with its associated DifferentialSymbol).

     repl

     The target variable to replace what with (and vice versa).

     Note

     soundness-critical: For uniform renaming purposes the semantic renaming proof rule would be sound but not locally sound. The kernel is easier when keeping everything locally sound.

     See also

     URename

     edu.cmu.cs.ls.keymaerax.core.Provable.apply(ren:edu\.cmu\.cs\.ls\.keymaerax\.core\.URename):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

     BoundRenaming

     RenamingClashException

138.  case class UnitFunctional(name: String, space: Space, sort: Sort) extends AtomicTerm with SpaceDependent with NamedSymbol with Product with Serializable

     Arity 0 functional symbol name:sort, written f(||), or limited to the given state space f(|x||).

     Arity 0 functional symbol name:sort, written f(||), or limited to the given state space f(|x||). The semantics of arity 0 functional symbol is given by the state, with the additional promise that the taboos are not free so the value does not depend on taboos when space=Except(taboos).

     Note

     In theory, f(||) is written f(\bar{x}) where \bar{x} is the vector of all variables. By analogy, f(|x|) is like having all variables other than taboo x as argument.

139.  case class UnitPredicational(name: String, space: Space) extends AtomicFormula with SpaceDependent with NamedSymbol with Product with Serializable

     Arity 0 predicational symbol name:bool, written P(||), or limited to the given state space P(|x|).

     Arity 0 predicational symbol name:bool, written P(||), or limited to the given state space P(|x|). The semantics of arity 0 predicational symbol is looked up by the state, with the additional promise that taboos are not free so the value does not depend on taboos when space=Except(taboos).

     Note

     In theory, P(||) is written P(\bar{x}) where \bar{x} is the vector of all variables. By analogy, P(|x|) is like having all variables other than taboo x as argument.

140.  case class UnknownOperatorException(msg: String, e: Expression) extends ProverException with Product with Serializable

     Thrown to indicate when an unknown operator occurs

141.  class UnprovedException extends CoreException

     Exception indicating an attempt to steal a proved sequent from a Provable that was not proved.

     Exception indicating an attempt to steal a proved sequent from a Provable that was not proved.

     See also

     Provable.proved

     Provable.isProved

142.  trait Variable extends NamedSymbol with AtomicTerm

     Variables have a name and index and sort.

     Variables have a name and index and sort. They are either BaseVariable or DifferentialSymbol.

143.  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 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. 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. 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. 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