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.
// 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.
, LemmaDBFactory.setLemmaDB(new FileLemmaDB) val lemmaDB = LemmaDBFactory.lemmaDB
 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.

trait
Evidence extends AnyRef
"Weak" Correctness evidence for lemmas

class
FileLemmaDB extends LemmaDBBase with Logging
Filebased lemma DB implementation.
Filebased lemma DB implementation. Stores one lemma per file in the user's home directory under
.keymaerax/cache/lemmadb/
directory. 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.

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 soundnesscritical part in a lemma is its provable fact, which can only be obtained from the prover core.
// 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 soundnesscritical so constructor is not private, because Provables can only be constructed by prover core.
 See also
ProvableSig.proveArithmeticLemma
Example: 
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 DBs can (and should) be implemented by extending this class and implementing the abstract methods for basic storage operations.
Value Members

object
Lemma extends Serializable
Facility for reading lemmas back in from their string representation.

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 structuresExpression
 Differential dynamic logic expressions:Term
,Formula
,Program
Sequent
 Sequents of formulasProvable
 Proof certificates transformed by rules/axiomsRule
 Proof rules as well asUSubstOne
for (onepass) 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.kyx
filesDLParser
 Combinator parser reading concrete KeYmaera X syntaxDLArchiveParser
 Combinator parser reading KeYmaera X model and proof archive.kyx
filesedu.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 firstorder logicHybridProgramCalculus
 Hybrid Program Calculus for differential dynamic logicDifferentialEquationCalculus
 Differential Equation Calculus for differential dynamic logicUnifyUSCalculus
 Unificationbased 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 backend solversMathematicaQETool
 Mathematica interface for real arithmetic.Z3QETool
 Z3 interface for real arithmetic.edu.cmu.cs.ls.keymaerax.tools.ext
 Extended backends 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
 Commandline launcher for KeYmaera X supports commandline argumenthelp
to 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
 Metainformation on all derivation steps (axioms, derived axioms, proof rules, tactics) with userinterface 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. 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, volume 9195 of LNCS, pp. 527538. Springer, 2015.
3. André Platzer. Logical Foundations of CyberPhysical Systems. Springer, 2018. Videos