1(* ========================================================================= *)
2(* INTERFACE TO TPTP PROBLEM FILES                                           *)
3(* Copyright (c) 2001-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibTptp =
7sig
8
9type term    = mlibTerm.term
10type formula = mlibTerm.formula
11
12(* Maintaining different relation and function names in TPTP problems *)
13val renaming : {tptp : string, fol : string, arity : int} list ref
14
15(* Reading from a TPTP file in CNF/FOF format: pass in a filename *)
16val read : {filename : string} -> formula
17
18(* Writing to a TPTP file in CNF format: pass in a formula and filename *)
19val write : {filename : string} -> formula -> unit
20
21(* Making TPTP formulas more palatable *)
22val prettify : formula -> formula
23
24end
25