package dolmen

  1. Overview
  2. Docs
A parser library

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (11)

Authors

  1. G
    Guillaume Bury

Maintainers

  1. G
    guillaume.bury@gmail.com

Sources

dolmen-0.4.1.tar.gz
md5=55a97ff61dd8398e38570272ae7e3964
sha512=83f71037eb568d5449ff2d968cb50a0b105c9712e0bd29497d1f95683698f394860a11d4dee2a2a41163504e395ef068c3974901fca11894d671684fe438fc51

doc/dolmen.tptp/Dolmen_tptp/Make/argument-4-S/index.html

Parameter Make.S

type t

The type of statements.

val annot : ?loc:L.t -> T.t -> T.t list -> T.t

Terms as annotations for statements.

val include_ : ?loc:L.t -> string -> I.t list -> t

Include directive. Given the filename, and a list of names to import (an empty list means import everything).

val tpi : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val thf : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val tff : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val fof : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t
val cnf : ?loc:L.t -> ?annot:T.t -> I.t -> string -> T.t -> t

TPTP statements, used for instance as tff ~loc ~annot name role t. Instructs the prover to register a new directive with the given name, role and term. Current tptp roles are:

  • "axiom", "hypothesis", "definition", "lemma", "theorem" acts as new assertions/declartions

  • "assumption", "conjecture" are proposition that need to be proved, and then can be used to prove other propositions. They are equivalent to the following sequence of smtlib statements:

    • push 1
    • assert (not t)
    • check_sat
    • pop 1
    • assert t
  • "negated_conjecture" is the same as "conjecture", but the given proposition is false (i.e its negation is the proposition to prove).
  • "type" declares a new symbol and its type
  • "plain", "unknown", "fi_domain", "fi_functors", "fi_predicates" are valid roles with no specified semantics
  • any other role is an error