object Tables extends Tables
Stand-alone Slick data model for immediate use
- Alphabetic
- By Inheritance
- Tables
- Tables
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
-
class
Agendaitems extends scala.slick.driver.JdbcProfile.SimpleQL.Table[AgendaitemsRow]
Table description of table agendaItems.
Table description of table agendaItems. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
AgendaitemsRow(_Id: Option[Int], proofid: Option[Int], stepid: Option[Int], subgoalid: Option[Int], displayname: Option[String]) extends Product with Serializable
Entity class storing rows of table Agendaitems
Entity class storing rows of table Agendaitems
- _Id
Database column _id DBType(INTEGER), PrimaryKey
- proofid
Database column proofId DBType(INTEGER)
- stepid
Database column stepId DBType(INTEGER)
- subgoalid
Database column subgoalId DBType(INTEGER)
- displayname
Database column displayName DBType(STRING)
- Definition Classes
- Tables
-
class
Config extends scala.slick.driver.JdbcProfile.SimpleQL.Table[ConfigRow]
Table description of table config.
Table description of table config. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
ConfigRow(configid: Option[Int], configname: Option[String], key: Option[String], value: Option[String]) extends Product with Serializable
Entity class storing rows of table Config
Entity class storing rows of table Config
- configid
Database column configId DBType(INTEGER), PrimaryKey
- configname
Database column configName DBType(TEXT)
- key
Database column key DBType(TEXT)
- value
Database column value DBType(TEXT)
- Definition Classes
- Tables
-
class
Executables extends scala.slick.driver.JdbcProfile.SimpleQL.Table[ExecutablesRow]
Table description of table executables.
Table description of table executables. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
ExecutablesRow(_Id: Option[Int], belleexpr: Option[String]) extends Product with Serializable
Entity class storing rows of table Executables
Entity class storing rows of table Executables
- _Id
Database column _id DBType(INTEGER), PrimaryKey
- belleexpr
Database column belleExpr DBType(TEXT)
- Definition Classes
- Tables
-
class
Executionsteps extends scala.slick.driver.JdbcProfile.SimpleQL.Table[ExecutionstepsRow]
Table description of table executionSteps.
Table description of table executionSteps. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
ExecutionstepsRow(_Id: Option[Int], proofid: Option[Int], previousstep: Option[Int], branchorder: Int, status: Option[String], executableid: Option[Int], inputprovableid: Option[Int], resultprovableid: Option[Int], localprovableid: Option[Int], userexecuted: Option[String], childrenrecorded: Option[String], rulename: Option[String], numsubgoals: Int, numopensubgoals: Int) extends Product with Serializable
Entity class storing rows of table Executionsteps
Entity class storing rows of table Executionsteps
- _Id
Database column _id DBType(INTEGER), PrimaryKey
- proofid
Database column proofId DBType(INTEGER)
- previousstep
Database column previousStep DBType(INTEGER)
- branchorder
Database column branchOrder DBType(INT)
- status
Database column status DBType(TEXT)
- executableid
Database column executableId DBType(INTEGER)
- inputprovableid
Database column inputProvableId DBType(INTEGER)
- resultprovableid
Database column resultProvableId DBType(INTEGER)
- localprovableid
Database column localProvableId DBType(INTEGER)
- userexecuted
Database column userExecuted DBType(BOOLEAN)
- childrenrecorded
Database column childrenRecorded DBType(BOOLEAN)
- rulename
Database column ruleName DBType(STRING)
- numsubgoals
Database column numSubGoals DBType(INTEGER)
- numopensubgoals
Database column numOpenSubGoals DBType(INTEGER)
- Definition Classes
- Tables
-
class
Lemmas extends scala.slick.driver.JdbcProfile.SimpleQL.Table[LemmasRow]
Table description of table lemmas.
Table description of table lemmas. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
LemmasRow(_Id: Option[Int], lemma: Option[String]) extends Product with Serializable
Entity class storing rows of table Lemmas
Entity class storing rows of table Lemmas
- _Id
Database column _id DBType(INTEGER), PrimaryKey
- lemma
Database column lemma DBType(TEXT)
- Definition Classes
- Tables
-
class
Models extends scala.slick.driver.JdbcProfile.SimpleQL.Table[ModelsRow]
Table description of table models.
Table description of table models. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
ModelsRow(_Id: Option[Int], userid: Option[String], name: Option[String], date: Option[String], description: Option[String], filecontents: Option[String], publink: Option[String], title: Option[String], tactic: Option[String], istemporary: Option[Int]) extends Product with Serializable
Entity class storing rows of table Models
Entity class storing rows of table Models
- _Id
Database column _id DBType(INTEGER), PrimaryKey
- userid
Database column userId DBType(TEXT)
- name
Database column name DBType(TEXT)
- date
Database column date DBType(TEXT)
- description
Database column description DBType(TEXT)
- filecontents
Database column fileContents DBType(TEXT)
- publink
Database column publink DBType(TEXT)
- title
Database column title DBType(TEXT)
- tactic
Database column tactic DBType(TEXT)
- istemporary
Database column isTemporary DBType(INTEGER)
- Definition Classes
- Tables
-
class
Proofs extends scala.slick.driver.JdbcProfile.SimpleQL.Table[ProofsRow]
Table description of table proofs.
Table description of table proofs. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
ProofsRow(_Id: Option[Int], modelid: Option[Int], name: Option[String], description: Option[String], date: Option[String], closed: Option[Int], lemmaid: Option[Int], istemporary: Option[Int], tactic: Option[String]) extends Product with Serializable
Entity class storing rows of table Proofs
Entity class storing rows of table Proofs
- _Id
Database column _id DBType(INTEGER), PrimaryKey
- modelid
Database column modelId DBType(INTEGER)
- name
Database column name DBType(TEXT)
- description
Database column description DBType(TEXT)
- date
Database column date DBType(TEXT)
- closed
Database column closed DBType(INTEGER)
- lemmaid
Database column lemmaId DBType(INTEGER)
- istemporary
Database column isTemporary DBType(INTEGER)
- tactic
Database column tactic DBType(TEXT)
- Definition Classes
- Tables
-
class
Users extends scala.slick.driver.JdbcProfile.SimpleQL.Table[UsersRow]
Table description of table users.
Table description of table users. Objects of this class serve as prototypes for rows in queries.
- Definition Classes
- Tables
-
case class
UsersRow(email: Option[String], hash: Option[String], salt: Option[String], iterations: Option[Int], level: Option[Int]) extends Product with Serializable
Entity class storing rows of table Users
Entity class storing rows of table Users
Database column email DBType(TEXT), PrimaryKey
- hash
Database column hash DBType(TEXT)
- salt
Database column salt DBType(TEXT)
- iterations
Database column iterations DBType(INTEGER)
- level
Database column level DBType(INTEGER)
- Definition Classes
- Tables
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
-
lazy val
Agendaitems: TableQuery[Agendaitems]
Collection-like TableQuery object for table Agendaitems
Collection-like TableQuery object for table Agendaitems
- Definition Classes
- Tables
-
lazy val
Config: TableQuery[Config]
Collection-like TableQuery object for table Config
Collection-like TableQuery object for table Config
- Definition Classes
- Tables
-
lazy val
Executables: TableQuery[Executables]
Collection-like TableQuery object for table Executables
Collection-like TableQuery object for table Executables
- Definition Classes
- Tables
-
lazy val
Executionsteps: TableQuery[Executionsteps]
Collection-like TableQuery object for table Executionsteps
Collection-like TableQuery object for table Executionsteps
- Definition Classes
- Tables
-
implicit
def
GetResultAgendaitemsRow(implicit e0: GetResult[Option[Int]], e1: GetResult[Option[String]]): GetResult[AgendaitemsRow]
GetResult implicit for fetching AgendaitemsRow objects using plain SQL queries
GetResult implicit for fetching AgendaitemsRow objects using plain SQL queries
- Definition Classes
- Tables
-
implicit
def
GetResultConfigRow(implicit e0: GetResult[Option[Int]], e1: GetResult[Option[String]]): GetResult[ConfigRow]
GetResult implicit for fetching ConfigRow objects using plain SQL queries
GetResult implicit for fetching ConfigRow objects using plain SQL queries
- Definition Classes
- Tables
-
implicit
def
GetResultExecutablesRow(implicit e0: GetResult[Option[Int]], e1: GetResult[Option[String]]): GetResult[ExecutablesRow]
GetResult implicit for fetching ExecutablesRow objects using plain SQL queries
GetResult implicit for fetching ExecutablesRow objects using plain SQL queries
- Definition Classes
- Tables
-
implicit
def
GetResultExecutionstepsRow(implicit e0: GetResult[Option[Int]], e1: GetResult[Int], e2: GetResult[Option[String]]): GetResult[ExecutionstepsRow]
GetResult implicit for fetching ExecutionstepsRow objects using plain SQL queries
GetResult implicit for fetching ExecutionstepsRow objects using plain SQL queries
- Definition Classes
- Tables
-
implicit
def
GetResultLemmasRow(implicit e0: GetResult[Option[Int]], e1: GetResult[Option[String]]): GetResult[LemmasRow]
GetResult implicit for fetching LemmasRow objects using plain SQL queries
GetResult implicit for fetching LemmasRow objects using plain SQL queries
- Definition Classes
- Tables
-
implicit
def
GetResultModelsRow(implicit e0: GetResult[Option[Int]], e1: GetResult[Option[String]]): GetResult[ModelsRow]
GetResult implicit for fetching ModelsRow objects using plain SQL queries
GetResult implicit for fetching ModelsRow objects using plain SQL queries
- Definition Classes
- Tables
-
implicit
def
GetResultProofsRow(implicit e0: GetResult[Option[Int]], e1: GetResult[Option[String]]): GetResult[ProofsRow]
GetResult implicit for fetching ProofsRow objects using plain SQL queries
GetResult implicit for fetching ProofsRow objects using plain SQL queries
- Definition Classes
- Tables
-
implicit
def
GetResultUsersRow(implicit e0: GetResult[Option[String]], e1: GetResult[Option[Int]]): GetResult[UsersRow]
GetResult implicit for fetching UsersRow objects using plain SQL queries
GetResult implicit for fetching UsersRow objects using plain SQL queries
- Definition Classes
- Tables
-
lazy val
Lemmas: TableQuery[Lemmas]
Collection-like TableQuery object for table Lemmas
Collection-like TableQuery object for table Lemmas
- Definition Classes
- Tables
-
lazy val
Models: TableQuery[Models]
Collection-like TableQuery object for table Models
Collection-like TableQuery object for table Models
- Definition Classes
- Tables
-
lazy val
Proofs: TableQuery[Proofs]
Collection-like TableQuery object for table Proofs
Collection-like TableQuery object for table Proofs
- Definition Classes
- Tables
-
lazy val
Users: TableQuery[Users]
Collection-like TableQuery object for table Users
Collection-like TableQuery object for table Users
- Definition Classes
- Tables
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
lazy val
ddl: scala.slick.driver.SQLiteDriver.DDL
DDL for all tables.
DDL for all tables. Call .create to execute.
- Definition Classes
- Tables
-
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] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
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()
- val profile: SQLiteDriver.type
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- 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( ... )
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