package lemma
Nonsoundnesscritical implementation of the lemma mechanism.
Lemma Mechanism
An implementation of a lemma data base using files edu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB. A factory edu.cmu.cs.ls.keymaerax.lemma.LemmaDBFactory provides instances of lemma databases.
LemmaDBFactory.setLemmaDB(new FileLemmaDB) val lemmaDB = LemmaDBFactory.lemmaDB
, // 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")) ) // use a lemma LookupLemma(lemmaDB, lemmaID)
The lemma database returned by the factory can be configured.
 Alphabetic
 By Inheritance
 lemma
 AnyRef
 Any
 Hide All
 Show All
 Public
 All
Type Members

class
CachedLemmaDB extends LemmaDB with Logging
Extends an arbitrary LemmaDB with caching functionality to reduce the cost of repeated accesses to the same Lemma within a given KeYmaeraX session.
Extends an arbitrary LemmaDB with caching functionality to reduce the cost of repeated accesses to the same Lemma within a given KeYmaeraX session.
Created by bbohrer on 8/3/16.

class
FileLemmaDB extends LemmaDBBase with Logging
Filebased lemma DB implementation.
Filebased lemma DB implementation. Stores one lemma per file in the user's KeYmaera X home directory under cache/lemmadb/. Lemma file names are created automatically and in a threadsafe manner.
 Note
Prefer LemmaDBFactory.lemmaDB over instantiating directly to get an instance of a lemma database and ensure thread safety. Created by smitsch on 4/27/15.

trait
LemmaDB extends AnyRef
Store and retrieve lemmas from a lemma database.
Store and retrieve lemmas from a lemma database. Use edu.cmu.cs.ls.keymaerax.lemma.LemmaDBFactory.lemmaDB to get an instance of a lemma database.
Storing and using a lemma
import edu.cmu.cs.ls.keymaerax.lemma.LemmaDBFactory val lemmaDB = LemmaDBFactory.lemmaDB // prove a lemma val proved = TactixLibrary.proveBy( Sequent(IndexedSeq(), IndexedSeq("true  x>5".asFormula)), orR(1) & close ) // store a lemma val evidence = ToolEvidence(immutable.Map("input" > proved.toString, "output" > "true")) :: Nil)) val lemmaID = lemmaDB.add( Lemma(proved, evidence, Some("Lemma test")) ) // use a lemma LookupLemma(lemmaDB, lemmaID)
 See also
Lemma
Example: 
abstract
class
LemmaDBBase extends LemmaDB
Common Lemma Database implemented from stringbased storage primitives.
Common Lemma Database implemented from stringbased storage primitives. Common logic shared by most lemma DB implementations. Most lemma DB's can (and should) be implemented by extending this class and implementing the abstract methods for basic storage operations.
Created by bbohrer on 8/3/16.
Value Members

object
LemmaDBFactory
Returns lemma database instances.
Returns lemma database instances. Prefer using this factory over instantiating lemma databases directly.
val lemmaDB = LemmaDBFactory.lemmaDB
Created by smitsch on 9/1/15.
Example:
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 structuresedu.cmu.cs.ls.keymaerax.core.Expression
 Differential dynamic logic expressionsedu.cmu.cs.ls.keymaerax.core.Sequent
 Sequents of formulasedu.cmu.cs.ls.keymaerax.core.Rule
 Proof rulesedu.cmu.cs.ls.keymaerax.core.Provable
 Proof certificateedu.cmu.cs.ls.keymaerax.btactics
 Tactic language libraryedu.cmu.cs.ls.keymaerax.btactics.TactixLibrary
 Main tactic libraryedu.cmu.cs.ls.keymaerax.btactics.HilbertCalculus
 Hilbert Calculus for differential dynamic logicedu.cmu.cs.ls.keymaerax.btactics.SequentCalculus
 Sequent Calculus for propositional and firstorder logicedu.cmu.cs.ls.keymaerax.btactics.UnifyUSCalculus
 Unificationbased Uniform Substitution Calculusedu.cmu.cs.ls.keymaerax.bellerophon
 Bellerophon tactic language and tactic interpreteredu.cmu.cs.ls.keymaerax.bellerophon.BelleExpr
 Tactic language expressionsedu.cmu.cs.ls.keymaerax.bellerophon.SequentialInterpreter
 Sequential tactic interpreteredu.cmu.cs.ls.keymaerax.parser
 Parser and pretty printer with concrete syntax and notation for differential dynamic logic.edu.cmu.cs.ls.keymaerax.parser.KeYmaeraXParser
 Parser for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXPrettyPrinter
 Pretty printer for concrete KeYmaera X syntaxedu.cmu.cs.ls.keymaerax.parser.KeYmaeraXProblemParser
 Parser for KeYmaera X problem files.kyx
edu.cmu.cs.ls.keymaerax.lemma
 Lemma mechanismedu.cmu.cs.ls.keymaerax.lemma.FileLemmaDB
 Lemma database stored in filesedu.cmu.cs.ls.keymaerax.tools
 Arithmetic backendsedu.cmu.cs.ls.keymaerax.tools.Mathematica
 Mathematica interface for real arithmetic and ODE solver etc.edu.cmu.cs.ls.keymaerax.tools.Z3
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.Polya
 Polya interface for real arithmetic.Additional entry points and usage points for KeYmaera X API:
edu.cmu.cs.ls.keymaerax.launcher.KeYmaeraX
 Commandline launcher for KeYmaera X supports commandline argumenthelp
to obtain usage informationedu.cmu.cs.ls.keymaerax.btactics.DerivationInfo
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface info.References
Full references are provided elsewhere 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. 219265, 2017.
2. Nathan Fulton, Stefan Mitsch, JanDavid 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, LNCS. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018.