Packages

trait LemmaDB extends AnyRef

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.

Example:
  1. 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

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. LemmaDB
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. type LemmaID = String

    Identifies a lemma.

Abstract Value Members

  1. abstract def add(lemma: Lemma): LemmaID

    Adds a new lemma to this lemma DB, with a unique name or None, which will automatically assign a name.

    Adds a new lemma to this lemma DB, with a unique name or None, which will automatically assign a name.

    lemma

    The lemma whose Provable will be inserted under its name.

    returns

    Internal lemma identifier.

  2. abstract def contains(lemmaID: LemmaID): Boolean

    Indicates whether or not this lemma DB contains a lemma with the specified ID.

    Indicates whether or not this lemma DB contains a lemma with the specified ID.

    lemmaID

    Identifies the lemma.

    returns

    True, if this lemma DB contains a lemma with the specified ID; false otherwise.

  3. abstract def deleteDatabase(): Unit

    Delete the whole lemma database

  4. abstract def get(lemmaIDs: List[LemmaID]): Option[List[Lemma]]

    Returns the lemmas with IDs lemmaIDs or None if any of the lemmaIDs does not exist.

    Returns the lemmas with IDs lemmaIDs or None if any of the lemmaIDs does not exist.

    lemmaIDs

    Identifies the lemmas.

    returns

    The list of lemmas, if all lemmaIDs exist. None otherwise.

  5. abstract def remove(name: LemmaID): Unit

    Delete the lemma of the given identifier, throwing exceptions if that was unsuccessful.

    Delete the lemma of the given identifier, throwing exceptions if that was unsuccessful.

    name

    Identifies the lemma.

  6. abstract def removeAll(folder: String): Unit

    Removes all lemmas in folder.

  7. abstract def version(): String

    Returns the version of this lemma database.

Concrete Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  7. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  8. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  9. def get(lemmaID: LemmaID): Option[Lemma]

    Returns the lemma with the given name or None if non-existent.

    Returns the lemma with the given name or None if non-existent.

    lemmaID

    Identifies the lemma.

    returns

    The lemma, if found under the given lemma ID. None otherwise.

  10. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  13. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  15. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  16. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  17. def toString(): String
    Definition Classes
    AnyRef → Any
  18. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  19. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  20. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped