class UIKeYmaeraXAxiomPrettyPrinter extends KeYmaeraXWeightedPrettyPrinter with HTMLPrinter
User-interface pretty printer for UI axiom entries.
- Alphabetic
- By Inheritance
- UIKeYmaeraXAxiomPrettyPrinter
- HTMLPrinter
- KeYmaeraXWeightedPrettyPrinter
- KeYmaeraXPrecedencePrinter
- KeYmaeraXSkipPrinter
- KeYmaeraXPrinter
- BasePrettyPrinter
- PrettyPrinter
- Function1
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new UIKeYmaeraXAxiomPrettyPrinter()
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
val
HTML_CLOSE: String
- Definition Classes
- HTMLPrinter
-
val
HTML_END_SPAN: String
- Definition Classes
- HTMLPrinter
-
val
HTML_OPEN: String
- Definition Classes
- HTMLPrinter
-
def
andThen[A](g: (String) ⇒ A): (Expression) ⇒ A
- Definition Classes
- Function1
- Annotations
- @unspecialized()
-
def
apply(seq: Sequent): String
Pretty-print sequent to a string
Pretty-print sequent to a string
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → BasePrettyPrinter → PrettyPrinter
-
def
apply(expr: Expression): String
Pretty-print term to a string
Pretty-print term to a string
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → BasePrettyPrinter → PrettyPrinter → Function1
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
compose[A](g: (A) ⇒ Expression): (A) ⇒ String
- Definition Classes
- Function1
- Annotations
- @unspecialized()
-
def
emit(q: PosInExpr, s: String): String
Emit the string
sqEmit the string
sq- Attributes
- protected
- Definition Classes
- KeYmaeraXPrinter
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
val
fullPrinter: (Expression) ⇒ String
The corresponding full-form pretty printer producing full parentheses.
The corresponding full-form pretty printer producing full parentheses.
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXPrinter → PrettyPrinter
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
htmlElement(tag: String, body: String, clazz: Option[String] = None): String
Returns the
bodyenclosed in an encoded HTMLtag.Returns the
bodyenclosed in an encoded HTMLtag.- Definition Classes
- HTMLPrinter
-
def
htmlEncode(html: String): String
Replaces KeYmaeraX syntax with HTML characters (e.g., < becomes <) and introduces opening/closing tags HTML syntax.
Replaces KeYmaeraX syntax with HTML characters (e.g., < becomes <) and introduces opening/closing tags HTML syntax.
- Definition Classes
- HTMLPrinter
-
def
htmlEndTag(tag: String): String
Returns a closing tag with encoded <>.
Returns a closing tag with encoded <>.
- Definition Classes
- HTMLPrinter
-
def
htmlOpenTag(tag: String, clazz: Option[String] = None): String
Returns an opening tag with encoded <>.
Returns an opening tag with encoded <>.
- Definition Classes
- HTMLPrinter
-
def
htmlTagEncode(text: String): String
Encodes HTML tags <>& etc.
Encodes HTML tags <>& etc. that may occur in text.
- Definition Classes
- HTMLPrinter
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
lazy val
parser: Parser
A parser that can read the input that this pretty-printer produces
A parser that can read the input that this pretty-printer produces
- Definition Classes
- KeYmaeraXPrinter → PrettyPrinter
-
def
pp(q: PosInExpr, program: Program): String
- Attributes
- protected
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXPrinter
-
def
pp(q: PosInExpr, term: Term): String
- Attributes
- protected
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXPrinter
-
def
pp(q: PosInExpr, fml: Formula): String
- Attributes
- protected
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXPrinter
-
def
ppODE(q: PosInExpr, program: DifferentialProgram): String
- Attributes
- protected
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXPrinter
-
def
ppOp(expr: Expression): String
Pretty-print the operator of a term
Pretty-print the operator of a term
- Attributes
- protected
- Definition Classes
- KeYmaeraXPrinter
-
def
pwrapLeft(t: BinaryComposite, leftPrint: String): String
Wrap
leftPrintt.leftWrap
leftPrintt.left- Attributes
- protected
- Definition Classes
- KeYmaeraXWeightedPrettyPrinter → KeYmaeraXSkipPrinter → KeYmaeraXPrinter
-
def
pwrapRight(t: BinaryComposite, rightPrint: String): String
Wrap
rightPrintt.rightWrap
rightPrintt.right- Attributes
- protected
- Definition Classes
- KeYmaeraXWeightedPrettyPrinter → KeYmaeraXSkipPrinter → KeYmaeraXPrinter
-
def
reparse(expr: Expression, print: String): Expression
Reparse the string print as the same kind as expr has
Reparse the string print as the same kind as expr has
- Attributes
- protected[edu.cmu.cs.ls.keymaerax]
- Definition Classes
- BasePrettyPrinter
-
val
rewritings: List[(String, String)]
- Definition Classes
- HTMLPrinter
-
def
skipParens(t: Modal): Boolean
Whether parentheses around
t.childWhether parentheses around
t.child- Attributes
- protected
- Definition Classes
- KeYmaeraXPrecedencePrinter → KeYmaeraXSkipPrinter
-
def
skipParens(t: Quantified): Boolean
Whether parentheses around
t.childWhether parentheses around
t.child- Attributes
- protected
- Definition Classes
- KeYmaeraXPrecedencePrinter → KeYmaeraXSkipPrinter
-
def
skipParens(t: UnaryComposite): Boolean
Whether parentheses around
t.childWhether parentheses around
t.child- Attributes
- protected
- Definition Classes
- KeYmaeraXPrecedencePrinter → KeYmaeraXSkipPrinter
-
def
skipParensLeft(t: BinaryComposite): Boolean
Whether parentheses around
t.leftWhether parentheses around
t.left- Attributes
- protected
- Definition Classes
- KeYmaeraXPrecedencePrinter → KeYmaeraXSkipPrinter
- Note
Based on (seemingly redundant) inequality comparisons since equality incompatible with comparison ==
-
def
skipParensRight(t: BinaryComposite): Boolean
Whether parentheses around
t.rightWhether parentheses around
t.right- Attributes
- protected
- Definition Classes
- KeYmaeraXPrecedencePrinter → KeYmaeraXSkipPrinter
- Note
Based on (seemingly redundant) inequality comparisons since equality incompatible with comparison ==
-
def
spaceLeft(t: BinaryComposite, leftPrint: String): String
- Attributes
- protected
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXWeightedPrettyPrinter
-
def
spaceRight(t: BinaryComposite, rightPrint: String): String
- Attributes
- protected
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXWeightedPrettyPrinter
-
def
statement(s: String): String
Formatting the atomic statement s
Formatting the atomic statement s
- Attributes
- protected
- Definition Classes
- KeYmaeraXPrinter
-
def
stringify(e: Expression): String
Pretty-print term to a string but without contract checking!
Pretty-print term to a string but without contract checking!
- Definition Classes
- KeYmaeraXWeightedPrettyPrinter → KeYmaeraXPrinter → BasePrettyPrinter
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
val
textTagRewritings: List[(String, String)]
- Definition Classes
- HTMLPrinter
-
def
toString(): String
- Definition Classes
- Function1 → AnyRef → Any
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
def
weight(sub: Expression, par: BinaryComposite): Int
- Attributes
- protected
- Definition Classes
- UIKeYmaeraXAxiomPrettyPrinter → KeYmaeraXWeightedPrettyPrinter
-
def
wrap(text: String, expr: Expression): String
Pretty-print enclosing parentheses, braces, brackets etc.
Pretty-print enclosing parentheses, braces, brackets etc.
- Attributes
- protected
- Definition Classes
- KeYmaeraXPrinter
-
def
wrapChild(t: Modal, childPrint: String): String
Wrap
childPrintt.childWrap
childPrintt.child- Attributes
- protected
- Definition Classes
- KeYmaeraXWeightedPrettyPrinter → KeYmaeraXSkipPrinter → KeYmaeraXPrinter
-
def
wrapChild(t: Quantified, childPrint: String): String
Wrap
childPrintt.childWrap
childPrintt.child- Attributes
- protected
- Definition Classes
- KeYmaeraXSkipPrinter → KeYmaeraXPrinter
-
def
wrapChild(t: UnaryComposite, childPrint: String): String
Wrap
childPrintt.childWrap
childPrintt.child- Attributes
- protected
- Definition Classes
- KeYmaeraXSkipPrinter → KeYmaeraXPrinter
-
def
wrapLeft(t: BinaryComposite, leftPrint: String): String
Wrap
leftPrintt.leftWrap
leftPrintt.left- Attributes
- protected
- Definition Classes
- KeYmaeraXWeightedPrettyPrinter → KeYmaeraXSkipPrinter → KeYmaeraXPrinter
-
def
wrapRight(t: BinaryComposite, rightPrint: String): String
Wrap
rightPrintt.rightWrap
rightPrintt.right- Attributes
- protected
- Definition Classes
- KeYmaeraXWeightedPrettyPrinter → KeYmaeraXSkipPrinter → KeYmaeraXPrinter
KeYmaera X: An aXiomatic Tactical Theorem Prover
KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems with mixed discrete and continuous dynamics. Reasoning about complicated hybrid systems requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute tactics in parallel, and interface with partial proofs via an extensible user interface.
http://keymaeraX.org/
Concrete syntax for input language Differential Dynamic Logic
Package Structure
Main documentation entry points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.core- KeYmaera X kernel, proof certificates, main data structuresExpression- Differential dynamic logic expressions:Term,Formula,ProgramSequent- Sequents of formulasProvable- Proof certificates transformed by rules/axiomsRule- Proof rules as well asUSubstOnefor (one-pass) uniform substitutions and renaming.StaticSemantics- Static semantics with free and bound variable analysisKeYmaeraXParser.edu.cmu.cs.ls.keymaerax.parser- Parser and pretty printer with concrete syntax and notation for differential dynamic logic.KeYmaeraXPrettyPrinter- Pretty printer producing concrete KeYmaera X syntaxKeYmaeraXParser- Parser reading concrete KeYmaera X syntaxKeYmaeraXArchiveParser- Parser reading KeYmaera X model and proof archive.kyxfilesDLParser- Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser- Combinator parser reading KeYmaera X model and proof archive.kyxfilesedu.cmu.cs.ls.keymaerax.infrastruct- Prover infrastructure outside the kernelUnificationMatch- Unification algorithmRenUSubst- Renaming Uniform Substitution quickly combining kernel's renaming and substitution.Context- Representation for contexts of formulas in which they occur.Augmentors- Augmenting formula and expression data structures with additional functionalityExpressionTraversal- Generic traversal functionality for expressionsedu.cmu.cs.ls.keymaerax.bellerophon- Bellerophon tactic language and tactic interpreterBelleExpr- Tactic language expressionsSequentialInterpreter- Sequential tactic interpreter for Bellerophon tacticsedu.cmu.cs.ls.keymaerax.btactics- Bellerophon tactic library for conducting proofs.TactixLibrary- Main KeYmaera X tactic library including many proof tactics.HilbertCalculus- Hilbert Calculus for differential dynamic logicSequentCalculus- Sequent Calculus for propositional and first-order logicHybridProgramCalculus- Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus- Differential Equation Calculus for differential dynamic logicUnifyUSCalculus- Unification-based uniform substitution calculus underlying the other calculi[edu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus.ForwardTactic ForwardTactic]- Forward tactic framework for conducting proofs from premises to conclusionsedu.cmu.cs.ls.keymaerax.lemma- Lemma mechanismLemma- Lemmas are Provables stored under a name, e.g., in files.LemmaDB- Lemma database stored in files or database etc.edu.cmu.cs.ls.keymaerax.tools.qe- Real arithmetic back-end solversMathematicaQETool- Mathematica interface for real arithmetic.Z3QETool- Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext- Extended back-ends for noncritical ODE solving, counterexamples, algebra, simplifiers, etc.Mathematica- Mathematica interface for ODE solving, algebra, simplification, invariant generation, etc.Z3- Z3 interface for real arithmetic including simplifiers.Entry Points
Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX- Command-line launcher for KeYmaera X supports command-line argument-helpto obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.AxIndex- Axiom indexing data structures with keys and recursors for canonical proof strategies.edu.cmu.cs.ls.keymaerax.btactics.DerivationInfo- Meta-information on all derivation steps (axioms, derived axioms, proof rules, tactics) with user-interface info.edu.cmu.cs.ls.keymaerax.bellerophon.UIIndex- Index determining which canonical reasoning steps to display on the KeYmaera X User Interface.edu.cmu.cs.ls.keymaerax.btactics.Ax- Registry for derived axioms and axiomatic proof rules that are proved from the core.References
Full references on KeYmaera X are provided at http://keymaeraX.org/. The main references are the following:
1. André Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-265, 2017.
2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer. KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015.
3. André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. Videos