Packages

package core

KeYmaera X Kernel: Soundness-critical core of the Axiomatic Tactical Theorem Prover KeYmaera X

The KeYmaera X Kernel implements Differential Dynamic Logic and defines

Usage Overview

The KeYmaera X Kernel package provides the soundness-critical core of KeYmaera X. It provides ways of constructing proofs that, by construction, can only be constructed using the proof rules that the KeYmaera X Kernel provides. The proof tactics that KeYmaera X provides give you a more powerful and flexible and easier way of constructing and searching for proofs, but they internally reduce to what is shown here.

Constructing Proofs

The proof certificates of KeYmaera X are of type edu.cmu.cs.ls.keymaerax.core.Provable. edu.cmu.cs.ls.keymaerax.core.Provable.startProof begins a new proof of a edu.cmu.cs.ls.keymaerax.core.Sequent containing the conjectured differential dynamic logic formula. A proof rule of type edu.cmu.cs.ls.keymaerax.core.Rule can be applied to any subgoal of a edu.cmu.cs.ls.keymaerax.core.Provable by edu.cmu.cs.ls.keymaerax.core.Provable.apply to advance the proof until that Provable has been proved since edu.cmu.cs.ls.keymaerax.core.Provable.isProved is true. Subgoals are identified by integers.

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, i.e. no remaining subgoals
if (proof.isProved) println("Successfully proved " + proof.proved)

Of course, edu.cmu.cs.ls.keymaerax.btactics make it much easier to describe proof search procedures compared to the above explicit proof construction. The tactics internally construct proofs this way, but add additional flexibility and provide convenient ways of expressing proof search strategies in a tactic language.

Combining Proofs

Multiple Provable objects for subderivations obtained from different sources can also be merged into a single Provable object by substitution with edu.cmu.cs.ls.keymaerax.core.Provable.apply()(edu.cmu.cs.ls.keymaerax.core.Provable,Int). The above example can be continued to merge proofs as follows:

// ... continued from above
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 (substitution)
val mergedProof = moreProof(proof, 0)
// check if proof successful, i.e. no remaining subgoals
if (mergedProof.isProved) println("Successfully proved " + mergedProof.proved)

More styles for proof construction are shown in Provable's.

Differential Dynamic Logic

The language of differential dynamic logic is described in KeYmaera X by its syntax and static semantics.

Syntax

The immutable algebraic data structures for the expressions of differential dynamic logic are of type edu.cmu.cs.ls.keymaerax.core.Expression. Expressions are categorized according to their kind by 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

See Section 2.1

Static Semantics

The static semantics of differential dynamic logic is captured in edu.cmu.cs.ls.keymaerax.core.StaticSemantics in terms of the free variables and bound variables that expressions have as well as their signatures (set of occurring symbols). See Section 2.4

Theorem Prover

The KeYmaera X Prover Kernel provides uniform substitutions, uniform and bound variable renaming, and axioms of differential dynamic logic. For efficiency, it also directly provides propositional sequent proof rules and Skolemization.

Axioms

The axioms and axiomatic rules of differential dynamic logic can be looked up with edu.cmu.cs.ls.keymaerax.core.Provable.axioms and edu.cmu.cs.ls.keymaerax.core.Provable.rules respectively. All available axioms are listed in edu.cmu.cs.ls.keymaerax.core.Provable.axioms, all available axiomatic rules are listed in edu.cmu.cs.ls.keymaerax.core.Provable.rules which both ultimately come from the file edu.cmu.cs.ls.keymaerax.core.AxiomBase. See Sections 4 and 5.0 Additional axioms are available as derived axioms and lemmas in edu.cmu.cs.ls.keymaerax.btactics.DerivedAxioms.

Uniform Substitutions

Uniform substitutions uniformly replace all occurrences of a given predicate p(.) by a formula in (.) and likewise for function symbols f(.) and program constants. Uniform substitutions and their application mechanism for differential dynamic logic are implemented in edu.cmu.cs.ls.keymaerax.core.USubst. See Section 3

Uniform substitutions can be used on proof certificates with the edu.cmu.cs.ls.keymaerax.core.Provable.apply(edu.cmu.cs.ls.keymaerax.core.USubst), including uniform substitution instances of axioms or axiomatic rules. See Section 3

Sequent Proof Rules

All proof rules for differential dynamic logic, including the uniform substitution and bound variable renaming rules as well as efficient propositional sequent proof rules and Skolemization edu.cmu.cs.ls.keymaerax.core.Skolemize are all of type edu.cmu.cs.ls.keymaerax.core.Rule, which are the only proof rules that can ever be applied to a proof. See sequent calculus

Additional Capabilities

Lemma Mechanism

A lemma storage mechanism and an interface to real arithmetic decision procedures are defined in edu.cmu.cs.ls.keymaerax.core.Lemma and edu.cmu.cs.ls.keymaerax.core.QETool.

Error Reporting

Errors from the prover core are reported as exceptions of type edu.cmu.cs.ls.keymaerax.core.ProverException whose main responsibility is to propagate problems in traceable ways to the user by augmenting them with contextual information. The prover core throws exceptions of type edu.cmu.cs.ls.keymaerax.core.CoreException.

Set Lattice

A data structure for sets (or rather lattice completions of sets) is provided in edu.cmu.cs.ls.keymaerax.core.SetLattice based on Scala's immutable sets.

Note

Code Review 2016-08-17

See also

edu.cmu.cs.ls.keymaerax.core.Lemma

edu.cmu.cs.ls.keymaerax.core.USubst

edu.cmu.cs.ls.keymaerax.core.StaticSemantics

edu.cmu.cs.ls.keymaerax.core.Expression

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

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

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

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. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Volp and Andre 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, LNCS. Springer, 2015.

Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.

Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.

Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015. arXiv 1503.01981

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

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

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. sealed trait ApplicationOf extends Composite

    Function/predicate/predicational application

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

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

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

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

  8. sealed trait Atomic extends Expression

    Atomic expressions

  9. sealed trait AtomicDifferentialProgram extends AtomicProgram with DifferentialProgram

    Atomic differential programs

  10. sealed trait AtomicFormula extends Formula with Atomic

    Atomic formulas

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

    x'=e atomic differential equation

  12. sealed trait AtomicProgram extends Program with Atomic

    Atomic programs

  13. sealed trait AtomicTerm extends Term with Atomic

    Atomic terms

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

  15. sealed trait BinaryComposite extends Composite

    Binary composite expressions that are composed of two subexpressions

  16. sealed trait BinaryCompositeFormula extends BinaryComposite with CompositeFormula

    Binary Composite Formulas, i.e.

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

  17. sealed trait BinaryCompositeProgram extends BinaryComposite with CompositeProgram

    Binary Composite Programs, i.e.

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

  18. sealed trait BinaryCompositeTerm extends BinaryComposite with CompositeTerm

    Binary Composite Terms, i.e.

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

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

    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.

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

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

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

    left++right nondeterministic choice

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

    Close / Identity rule

    Close / Identity rule

           *
    ------------------ (Id)
      p, G |- p, D
  23. case class CloseFalse(pos: AntePos) extends LeftRule with Product with Serializable

    Close by false.

    Close by false.

           *
    ------------------ (close false)
      false, G |- D
  24. case class CloseTrue(pos: SuccPos) extends RightRule with Product with Serializable

    Close by true

    Close by true

          *
    ------------------ (close true)
      G |- true, D
  25. 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
  26. case class CoHideLeft(pos: AntePos) extends LeftRule with Product with Serializable

    CoHide left.

    CoHide left.

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

    Not used, just contained for symmetry reasons

    ,

    Rarely useful (except for contradictory p)

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

    CoHide right.

    CoHide right.

        |- p
    ------------- (CoHide right)
      G |- p, D
  28. 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

  29. 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
  30. sealed trait ComparisonFormula extends AtomicFormula with BinaryComposite

    Atomic comparison formula composed of two terms.

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

    left;right sequential composition

  32. sealed trait Composite extends Expression

    Composite expressions that are composed of subexpressions

  33. sealed trait CompositeFormula extends Formula with Composite

    Composite formulas

  34. sealed trait CompositeProgram extends Program with Composite

    composite programs

  35. sealed trait CompositeTerm extends Term with Composite

    Composite terms

  36. class CoreException extends ProverException

    Critical exceptions from the KeYmaera X Prover Core.

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

    Cut in the given formula c.

    Cut in the given formula c.

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

    c will be added at the end on the subgoals

  38. 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?

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

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

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

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

    ' differential of a term

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

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

  43. 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 reassociates to list form DifferentialProduct(AtomicDifferentialProgram, DifferentialProduct(AtomicDifferentialProgram, ....))

    Note

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

    ,

    This is a case class except for an override of the apply function.

  44. sealed trait DifferentialProgram extends Program

    Differential programs of differential dynamic logic.

    Differential programs of differential dynamic logic.

    Differential Programs are of the form

    See also

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

  45. sealed 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 taboo is neither free nor bound, so the run does not depend on the value of taboo nor does the value of taboo change when space=Except(taboo).

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

    Differential symbol x' for variable x

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

    / real division

  48. sealed 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 symbol \\cdot for uniform substitutions are unlike ordinary function symbols

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

    child^d dual program

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

    = equality left = right

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

    <-> logical biimplication: equivalent

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

  53. 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
  54. 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
  55. trait Evidence extends AnyRef

    "Weak" Correctness evidence for lemmas

  56. case class Except(taboo: Variable) extends Space with Product with Serializable

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

  57. 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
  58. 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
  59. case class Exists(vars: Seq[Variable], child: Formula) extends Quantified with Product with Serializable

    \exists vars existentially quantified formula

  60. sealed trait Expression extends AnyRef

    Expressions of differential dynamic logic.

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

    \forall vars universally quantified formula

  62. sealed trait Formula extends Expression

    Formulas of differential dynamic logic.

    Formulas of differential dynamic logic.

    Formulas are of the form

    See also

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

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

    Function symbol applied to argument child func(child)

  64. sealed case class Function(name: String, index: Option[Int] = None, domain: Sort, sort: Sort, interpreted: Boolean = false) extends Expression with 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

    interpreted

    when true this function symbol has a fixed interpretation/definition.

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

    > greater than comparison left > right

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

    >= greater or equal comparison left >= right

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

    Hide left.

    Hide left.

        G |- D
    ------------- (Weaken left)
     p, G |- D
  68. case class HideRight(pos: SuccPos) extends RightRule with Product with Serializable

    Hide right.

    Hide right.

       G |- D
    ------------- (Weaken right)
       G |- p, D
  69. case class Imply(left: Formula, right: Formula) extends BinaryCompositeFormula with Product with Serializable

    -> logical implication: implies

  70. 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
  71. 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
  72. case class InapplicableRuleException(msg: String, r: Rule, s: Sequent = null) extends CoreException with Product with Serializable

    Rule is not applicable as indicated

  73. sealed trait Kind extends AnyRef

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

  74. trait LeftRule extends PositionRule

    A rule applied to a position in the antecedent on the left

  75. final case class Lemma(fact: ProvableSig, evidence: List[Evidence], name: Option[String] = None) extends Product with Serializable

    Lemmas are named Provables, supported by some evidence of how they came about.

    Lemmas are named Provables, supported by some evidence of how they came about. The soundness-critical part in a lemma is its provable fact, which can only be obtained from the prover core.

    Example:
    1. // prove a lemma
      val proved = TactixLibrary.proveBy(
         Sequent(IndexedSeq(), IndexedSeq("true | x>5".asFormula)),
         orR(1) & close
       )
      // store a lemma
      val lemmaDB = LemmaDBFactory.lemmaDB
      val evidence = ToolEvidence(immutable.Map("input" -> proved.toString, "output" -> "true")) :: Nil))
      val lemmaID = lemmaDB.add(
        Lemma(proved, evidence, Some("Lemma  test"))
      )
      
      // retrieve a lemma
      val lemmaFact = lemmaDB.get(lemmaID).get.fact
      // use a lemma literally
      TactixLibrary.by(lemmaFact)
      // use a uniform substitution instance of a lemma
      TactixLibrary.byUS(lemmaFact)
    Note

    Construction is not soundness-critical so constructor is not private, because Provables can only be constructed by prover core.

    See also

    Lemma.fromString

    edu.cmu.cs.ls.keymaerax.lemma.LemmaDB

    ProvableSig.proveArithmetic

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

    <= less than comparison left < right

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

    < less or equal comparison left <= right

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

    child* nondeterministic repetition

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

    - binary subtraction

  80. sealed trait Modal extends CompositeFormula

    Modal formulas

  81. sealed trait NamedSymbol extends Expression with Ordered[NamedSymbol]

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

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

    Note

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

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

    - unary negation: minus

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

    ! logical negation: not

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

    != disequality left != right

  85. 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
  86. 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
  87. case class Number(value: BigDecimal) extends AtomicTerm with RTerm with Product with Serializable

    Number literal

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

    Differential equation system ode with given evolution domain constraint

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

    User-defined object sort

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

    | logical disjunction: or

  91. 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
  92. 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
  93. 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.

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

    + binary addition

  95. trait PositionRule extends Rule

    A rule applied to a position

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

    real exponentiation or power: leftright

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

    Predicate symbol applied to argument child func(child)

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

  99. sealed trait Program extends Expression

    Hybrid programs of differential dynamic logic.

    Hybrid programs of differential dynamic logic.

    Hybrid Programs are of the form

    See also

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

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

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

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

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

    Examples:
    1. 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)
      )
    2. ,
    3. 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)
    4. ,
    5. 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)
    6. ,
    7. 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)
    8. ,
    9. 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)
    10. ,
    11. 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)
    Note

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

    ,

    Only private constructor calls for soundness

    ,

    soundness-critical logical framework.

    See also

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

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

    Assertions that fail in the prover

  103. class ProverException extends RuntimeException

    KeYmaera X Prover Exceptions.

  104. trait QETool extends AnyRef

    Quantifier elimination tool.

    Quantifier elimination tool.

    See also

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

  105. sealed trait Quantified extends CompositeFormula

    Quantified formulas

  106. case class RenamingClashException(msg: String, ren: String, e: String, info: String = "") extends CoreException with Product with Serializable

    Uniform or bound renaming clash exception

  107. trait RightRule extends PositionRule

    A rule applied to a position in the succedent on the right

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

    Subclasses represent all proof rules.

    Subclasses represent all proof rules. A proof rule is ultimately a named mapping from sequents to lists of sequents. The resulting list of sequents represent the subgoal/premise and-branches 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

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

    SuccPos

    AntePos

    Sequent.apply()

    SeqPos.apply()

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

  111. sealed trait SetLattice[A] extends AnyRef

    Lattice of sets, i.e.

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

    A

    Type of elements in the set

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

    Skolem symbol clash

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

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

  114. sealed trait Sort extends AnyRef

    Sorts of expressions (real, bool, etc).

  115. sealed trait Space extends AnyRef

    Sorts of state spaces for state-dependent operators

  116. sealed trait SpaceDependent extends StateDependent

    Expressions limited to a given sub state-space.

    Expressions limited to a given sub state-space.

    Since

    4.2

  117. sealed 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.

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

    Substitution clash

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

    what

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

    repl

    the expression to be used in place of what.

    See also

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

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

  121. sealed case class SystemConst(name: String) extends NamedSymbol with AtomicProgram with StateDependent with Product with Serializable

    Uninterpreted hybrid system program constant that are NOT hybrid games.

  122. sealed trait Term extends Expression

    Terms of differential dynamic logic.

    Terms of differential dynamic logic.

    Terms are of the form

    See also

    Syntax of differential dynamic logic

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

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

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

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

    * binary multiplication

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

    Tuple sort for Pair.

  126. final case class URename(what: Variable, repl: Variable) 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').

    what

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

    repl

    The target variable to replace what with and vice versa.

    Note

    soundness-critical

    See also

    BoundRenaming

    UniformRenaming

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

    A Uniform Substitution with its application mechanism.

    A Uniform Substitution with its 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 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.

    Examples:
    1. 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)
    2. ,
    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. ,
    5. 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)
    6. ,
    7. 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))
    Note

    soundness-critical

    ,

    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.

    See also

    edu.cmu.cs.ls.keymaerax.core.Provable.apply(edu.cmu.cs.ls.keymaerax.core.UniformSubstitution)

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

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.

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

  128. sealed trait UnaryComposite extends Composite

    Unary composite expressions that are composed of one subexpression

  129. sealed trait UnaryCompositeFormula extends UnaryComposite with CompositeFormula

    Unary Composite Formulas, i.e.

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

  130. sealed trait UnaryCompositeProgram extends UnaryComposite with CompositeProgram

    Unary Composite Programs, i.e.

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

  131. sealed trait UnaryCompositeTerm extends UnaryComposite with CompositeTerm

    Unary Composite Terms, i.e.

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

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

    what

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

    repl

    The target variable to replace what with.

    See also

    URename

  133. 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, limited to the given state space.

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

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

    Arity 0 predicational symbol name:bool, limited to the given state space.

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

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

    Thrown to indicate when an unknown operator occurs

  136. sealed 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.

Value Members

  1. val VERSION: String

    KeYmaera X core kernel version number

  2. final def insist(requirement: Boolean, message: ⇒ Any): scala.Unit

    Insist on requirement being true, throwing a CoreException if false.

    Insist on requirement being true, throwing a CoreException if false. This method is a require coming from the prover core that cannot be disabled. Blame is on the caller of the method for violating the contract.

    requirement

    the expression to test for being true

    message

    a String explaining what is expected.

    Annotations
    @inline()
    See also

    scala.Predef.require()

  3. final def noException[T](e: ⇒ T): Boolean

    Check that the given expression e does not throw an exception.

    Check that the given expression e does not throw an exception.

    returns

    true if e completed without raising any exceptions or errors. false if e raised an exception or error.

    Annotations
    @inline()
    Example:
    1. insist(noExeption(complicatedComputation), "The complicated computation should complete without throwing exceptions")
  4. object AnyArg extends Space

    The sort denoting the whole state space alias list of all variables as arguments \bar{x} (axioms that allow any variable dependency)

  5. object Bool extends Sort

    Sort of booleans: True, False.

  6. object DifferentialProduct
  7. object DifferentialProgramKind extends Kind

    All differential programs are of kind DifferentialProgramKind

  8. object DotFormula extends NamedSymbol with AtomicFormula with StateDependent

    ⎵: Placeholder for formulas in uniform substitutions.

    ⎵: Placeholder for formulas in uniform substitutions. Reserved nullary predicational symbol _ for substitutions are unlike ordinary predicational symbols

  9. object ExpressionKind extends Kind

    All expressions that are neither terms nor formulas nor programs nor functions are of kind ExpressionKind

  10. object False extends AtomicFormula

    Falsum formula false

  11. object FormulaKind extends Kind

    All formulas are of kind FormulaKind

  12. object FunctionKind extends Kind

    Function/predicate symbols that are not themselves terms or formulas are of kind FunctionKind

  13. object Lemma extends Serializable

    Facility for reading lemmas back in from their string representation.

  14. object NoProverException extends ProverException

    Nil case for exceptions, which is almost useless except when an exception type is needed to indicate that there really was none.

  15. object Nothing extends NamedSymbol with AtomicTerm

    The empty argument of Unit sort (as argument for arity 0 function/predicate symbols)

  16. object PrettyPrinter extends (Expression) ⇒ String

    A pretty printer for differential dynamic logic is a function from Expressions to Strings.

    A pretty printer for differential dynamic logic is a function from Expressions to Strings. This object manages the default pretty printer that KeYmaera X uses in Expression.prettyString.

    See also

    Expression.prettyString

    edu.cmu.cs.ls.keymaerax.parser.PrettyPrinter

  17. object ProgramKind extends Kind

    All programs are of kind ProgramKind

  18. object Provable extends Serializable

    Starting new Provables to begin a proof, either with unproved conjectures or with proved axioms or axiomatic proof rules.

  19. object Real extends Sort

    Sort of real numbers: 0, 1, 2.5

  20. object SeqPos
  21. object SetLattice
  22. object StaticSemantics

    The static semantics of differential dynamic logic.

    The static semantics of differential dynamic logic. This object defines the static semantics of differential dynamic logic in terms of the free variables and bound variables that expressions have as well as their signatures. See Section 2.3

    Example:
    1. val fml = Imply(Greater(Variable("x",None,Real), Number(5)),
        Forall(Seq(Variable("y",None,Real)),
          GreaterEqual(Variable("x",None,Real), FuncOf(Function("f",None,Real,Real), Variable("y",None,Real)))))
      // determine the static semantics of the above formula
      val stat = StaticSemantics(fml)
      println("Free variables  " + stat.fv)
      println("Bound variables " + stat.bv)
      // determine all function, predicate and program constants occurring in the above formula
      println("Signature       " + StaticSemantics.signature(fml))
      // determine all symbols occurring in the above formula
      println("Symbols         " + StaticSemantics.symbols(fml))
    Note

    soundness-critical

    See also

    edu.cmu.cs.ls.keymaerax.btactics.StaticSemanticsTools

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.

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

  23. object SubstitutionAdmissibility

    Admissibility conditions.

  24. object TermKind extends Kind

    All terms are of kind TermKind

  25. object Trafo extends Sort

    Sort of state transformations (i.e.

    Sort of state transformations (i.e. programs)

  26. object True extends AtomicFormula

    Verum formula true

  27. object UniformRenaming extends Serializable

    Convenience for uniform renaming.

  28. object Unit extends Sort

    Unit type of Nothing

  29. object Variable

Inherited from AnyRef

Inherited from Any

Ungrouped