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