package tptp

  1. Overview
  2. Docs
package tptp
Legend:
Library
Module
Module type
Parameter
Class
Class type

AST for FOF and CNF formulas.

type tptp_input =
  1. | Fof_anno of fof_formula annotated_formula
  2. | Cnf_anno of cnf_formula annotated_formula
  3. | Include of file_name * formula_name list
    (*

    Empty list means that no selection was specified.

    *)
  4. | Comment of comment_line
and 't annotated_formula = {
  1. af_name : formula_name;
  2. af_role : formula_role;
  3. af_formula : 't;
  4. af_annos : annotations option;
}
and annotations = {
  1. a_source : gterm;
  2. a_useful_info : gterm list;
}

Note: TPTP can distinguish between no useful info and empty useful info. But here are both represented by the empty list.

and formula_role =
  1. | R_axiom
  2. | R_hypothesis
  3. | R_definition
  4. | R_assumption
  5. | R_lemma
  6. | R_theorem
  7. | R_corollary
  8. | R_conjecture
  9. | R_negated_conjecture
  10. | R_plain
  11. | R_fi_domain
  12. | R_fi_functors
  13. | R_fi_predicates
  14. | R_type
  15. | R_unknown
and fof_formula =
  1. | Sequent of formula list * formula list
  2. | Formula of formula
and formula =
  1. | Binop of binop * formula * formula
  2. | Not of formula
  3. | Quant of quant * var * formula
  4. | Atom of atom
and binop =
  1. | Equiv
  2. | Implies
  3. | Implies_rev
  4. | Xor
  5. | Nor
  6. | Nand
  7. | Or
  8. | And
and quant =
  1. | All
  2. | Exists
and cnf_formula =
  1. | Clause of literal list
and literal =
  1. | Lit of sign * atom
and sign =
  1. | Pos
  2. | Neg
and atom =
  1. | Equals of term * term
  2. | Pred of atomic_word * term list
and term =
  1. | Var of var
  2. | Func of atomic_word * term list
  3. | Number of Q.t
  4. | String of tptp_string
and atomic_word =
  1. | Plain_word of plain_word
  2. | Defined_word of defined_word
  3. | System_word of system_word

Note: Type atomic_word has no equivalent in TPTP. Type plain_word correspons to atomic_word from TPTP.

Alphanumeric characters include lowercase ('a'..'z') and uppercase ('A'..'Z') letters, digits ('0'..'9') and underscore.

and var = private string

Uppercase letter followed by zero or more alphanumeric characters.

In TPTP: variable.

and plain_word = private string

Nonempty string which consists of ASCII characters from space to tilde.

In TPTP: atomic_word.

and defined_word = private string

Dollar followed by lowercase letter and zero or more alphanumeric characters. Keywords ($fof, $cnf, $fot) are not allowed.

In TPTP: atomic_defined_word.

and system_word = private string

Two dollars followed by lowercase letter and zero or more alphanumeric characters.

In TPTP: atomic_system_word.

and tptp_string = private string

ASCII characters from space to tilde (empty string allowed).

In TPTP: distinct_object.

and comment_line = private string

Printable ASCII characters (code >= 32 && code <= 126) or tabs (empty string allowed).

and formula_name =
  1. | N_word of plain_word
  2. | N_integer of Z.t

In TPTP: name.

and file_name = plain_word
and gterm =
  1. | G_data of gdata
  2. | G_cons of gdata * gterm
  3. | G_list of gterm list
and gdata =
  1. | G_func of plain_word * gterm list
  2. | G_var of var
  3. | G_number of Q.t
  4. | G_string of tptp_string
  5. | G_formula of gformula
and gformula =
  1. | G_fof of fof_formula
  2. | G_cnf of cnf_formula
  3. | G_fot of term
val to_var : string -> var

Raises Failure when the string is invalid.

val to_plain_word : string -> plain_word

Raises Failure when the string is invalid.

val to_defined_word : string -> defined_word

Raises Failure when the string is invalid.

val to_system_word : string -> system_word

Raises Failure when the string is invalid.

val to_tptp_string : string -> tptp_string

Raises Failure when the string is invalid.

val to_comment_line : string -> comment_line

Raises Failure when the string is invalid.

val tptp_input_equal : tptp_input -> tptp_input -> bool

Useful when (=) causes stack overflow.