package dolmen

You can search for identifiers within the package.

in-package search v0.2.0

package dolmen

dolmen
- Dolmen
  - Intf
dolmen.class
- Dolmen_class
  - Logic
    
    Make
    
    I
    
    L
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    T
dolmen.dimacs
- Dolmen_dimacs
  - Make
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.icnf
- Dolmen_icnf
  - Make
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.intf
- Dolmen_intf
  - Id
    
    Logic
  - Language
    
    S
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
  - Lex
    
    S
  - Location
    
    S
  - Parse
    
    S
    
    Incremental
    
    MenhirInterpreter
  - Stmt
    
    Logic
  - Term
    
    Logic
dolmen.line
- Dolmen_line
dolmen.smtlib
- Dolmen_smtlib
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.std
- Dolmen_std
  - Id
  - Misc
  - Normalize
    
    Smtlib
    
    Tptp
  - ParseLocation
  - Statement
  - Term
  - Transformer
    
    Make
    
    Lex
    
    Loc
    
    Parse
    
    Incremental
    
    MenhirInterpreter
    
    Ty
dolmen.tptp
- Dolmen_tptp
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term
dolmen.zf
- Dolmen_zf
  - Id
  - Make
    
    I
    
    L
    
    Lexer
    
    Parser
    
    Incremental
    
    MenhirInterpreter
    
    S
    
    T
  - Statement
  - Term

Legend:
Library
Module
Module type
Parameter
Class
Class type

Implementation requirement for the TPTP format.

type t

The type of statements.

type id

The type of identifiers

type term

The type of terms used in statements.

type location

The type of locations attached to statements.

val annot : ?loc:location -> term -> term list -> term

Terms as annotations for statements.

val include_ : ?loc:location -> string -> id list -> t

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

val tpi : ?loc:location -> ?annot:term -> id -> string -> term -> t

val thf : ?loc:location -> ?annot:term -> id -> string -> term -> t

val tff : ?loc:location -> ?annot:term -> id -> string -> term -> t

val fof : ?loc:location -> ?annot:term -> id -> string -> term -> t

val cnf : ?loc:location -> ?annot:term -> id -> string -> term -> 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