object AssessmentProver
Assesses dL terms and formulas for equality, equivalence, implication etc. with restricted automation.
- Alphabetic
- By Inheritance
- AssessmentProver
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- case class AnyChoiceGrader(args: Map[String, String], expected: ChoiceArtifact) extends Grader with Product with Serializable
-
case class
AnyOfArtifact(artifacts: List[Artifact]) extends Artifact with Product with Serializable
Any of the artifacts is correct.
- case class ArchiveArtifact(s: String) extends Artifact with Product with Serializable
-
abstract
class
Artifact extends AnyRef
Assessment prover input artifacts (expressions, sequents etc.)
- case class AskGrader(mode: Option[String], args: Map[String, String], expected: Artifact) extends Grader with Product with Serializable
- case class AskTFGrader(expected: BoolArtifact) extends Grader with Product with Serializable
- case class BoolArtifact(value: Option[Boolean]) extends Artifact with Product with Serializable
- case class ChoiceArtifact(selected: List[String]) extends Artifact with Product with Serializable
- case class ExpressionArtifact(exprString: String, kind: Option[Kind] = None) extends Artifact with Product with Serializable
- abstract class Grader extends AnyRef
- case class ListExpressionArtifact(exprs: List[Expression]) extends Artifact with Product with Serializable
-
case class
MultiArtifact(artifacts: List[Artifact]) extends Artifact with Product with Serializable
Artifacts from multiple questions.
-
case class
MultiAskGrader(main: Grader, earlier: Map[Int, Grader]) extends Grader with Product with Serializable
A grader that has access to multiple answers.
- case class OneChoiceGrader(args: Map[String, String], expected: ChoiceArtifact) extends Grader with Product with Serializable
- case class SequentArtifact(goals: List[Sequent]) extends Artifact with Product with Serializable
- case class SkipGrader(expected: Artifact, reason: String) extends Grader with Product with Serializable
- case class SubstitutionArtifact(s: List[SubstitutionPair]) extends Artifact with Product with Serializable
- case class TacticArtifact(s: String, t: BelleExpr) extends Artifact with Product with Serializable
- case class TexExpressionArtifact(expr: Expression) extends Artifact with Product with Serializable
- case class TextArtifact(value: Option[String]) extends Artifact with Product with Serializable
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
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
- def contractEquivalence(have: Formula, expected: Formula): ProvableSig
-
def
dICheck(ode: ODESystem, inv: Formula): ProvableSig
Checks
invfor being a differential invariant ofode. - def dIPremiseCheck(a: Sequent, b: Sequent, diffAssignsMandatory: Boolean, normalize: Boolean): ProvableSig
- def dIPremiseCheck(a: Formula, b: Formula, diffAssignsMandatory: Boolean, normalize: Boolean): ProvableSig
-
def
dIReductionCheck(h: Formula, e: Formula): ProvableSig
Checks that formula
his equivalent differential invariant to formulae, i.e.Checks that formula
his equivalent differential invariant to formulae, i.e. (e<->h) & (e' -> h') -
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
exportAnswers(chapter: Chapter, out: String): Unit
Exports answers from
chapterto individual files in directoryout, on for each question (named 1a.txt ...Exports answers from
chapterto individual files in directoryout, on for each question (named 1a.txt ... Xy.txt) -
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
- def formulaImplication(a: Formula, b: Formula): ProvableSig
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
grade(options: OptionMap, msgOut: OutputStream, resultOut: OutputStream, usage: String): Unit
Grades a submission.
Grades a submission.
- options
The prover options:
- 'in (mandatory) identifies the file to grade
- 'exportanswers (optional) exports answers to text files instead of grading
- 'skiponparseerror (optional) skips grading on parse errors
-
def
grade(options: OptionMap, usage: String): Unit
Grades a submission.
Grades a submission.
- options
The prover options:
- 'in (mandatory) identifies the file to grade
- 'res (optional) result file
- 'msg (optional) message file
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
isFormulaImplied(a: Formula, b: Formula): Boolean
True if a->b.
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
loopCheck(question: Formula, inv: Formula): ProvableSig
Checks
invfor being a loop invariant forquestionof the shapeP->[{a;}*]Qor[{a;}*]P. -
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()
-
def
polynomialEquality(a: Sequent, b: Sequent, normalize: Boolean): ProvableSig
Proves polynomial equality between the terms resulting from chasing simple programs in
aandb. -
def
polynomialEquality(a: Formula, b: Formula, normalize: Boolean): ProvableSig
Collects terms and compares for polynomial equality.
Collects terms and compares for polynomial equality. Checks parent operators along the way.
-
def
polynomialEquality(a: Term, b: Term): ProvableSig
Proves polynomial equality of
aandb. -
def
prgEquivalence(a: Program, b: Program): ProvableSig
Checks program equivalence by
[a;]P <-> [b;]P. -
def
prove(s: Sequent, t: BelleExpr): ProvableSig
Generic assessment prover uses tactic
tto prove sequents, aborting aftertimeouttime. -
def
qe(a: Formula, b: Formula, op: (Formula, Formula) ⇒ Formula): ProvableSig
Proves equivalence of
aandbby QE. -
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
syntacticEquality(a: List[Sequent], b: List[Sequent]): ProvableSig
Compares sequents for syntactic equality.
-
def
syntacticEquality(a: Expression, b: Expression): ProvableSig
Compares expressions for syntactic equality.
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
def
valueEquality(a: List[Term], b: List[Term]): ProvableSig
Compares terms in lists
aandbpairwise for the same real value. -
def
valueEquality(a: Term, b: Term): ProvableSig
Compares terms
aandbfor having the same real values. -
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( ... )
- object AskGrader extends Serializable
- object Messages
- object Options
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