1(* ========================================================================= *) 2(* THE TPTP PROBLEM FILE FORMAT *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Tptp = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* Mapping to and from TPTP variable, function and relation names. *) 11(* ------------------------------------------------------------------------- *) 12 13type mapping 14 15val defaultMapping : mapping 16 17val mkMapping : 18 {functionMapping : {name : Name.name, arity : int, tptp : string} list, 19 relationMapping : {name : Name.name, arity : int, tptp : string} list} -> 20 mapping 21 22val addVarSetMapping : mapping -> NameSet.set -> mapping 23 24(* ------------------------------------------------------------------------- *) 25(* Interpreting TPTP functions and relations in a finite model. *) 26(* ------------------------------------------------------------------------- *) 27 28val defaultFixedMap : Model.fixedMap 29 30val defaultModel : Model.parameters 31 32val ppFixedMap : mapping -> Model.fixedMap Print.pp 33 34(* ------------------------------------------------------------------------- *) 35(* TPTP roles. *) 36(* ------------------------------------------------------------------------- *) 37 38datatype role = 39 AxiomRole 40 | ConjectureRole 41 | DefinitionRole 42 | NegatedConjectureRole 43 | PlainRole 44 | TheoremRole 45 | OtherRole of string; 46 47val isCnfConjectureRole : role -> bool 48 49val isFofConjectureRole : role -> bool 50 51val toStringRole : role -> string 52 53val fromStringRole : string -> role 54 55val ppRole : role Print.pp 56 57(* ------------------------------------------------------------------------- *) 58(* SZS statuses. *) 59(* ------------------------------------------------------------------------- *) 60 61datatype status = 62 CounterSatisfiableStatus 63 | TheoremStatus 64 | SatisfiableStatus 65 | UnknownStatus 66 | UnsatisfiableStatus 67 68val toStringStatus : status -> string 69 70val ppStatus : status Print.pp 71 72(* ------------------------------------------------------------------------- *) 73(* TPTP literals. *) 74(* ------------------------------------------------------------------------- *) 75 76datatype literal = 77 Boolean of bool 78 | Literal of Literal.literal 79 80val negateLiteral : literal -> literal 81 82val functionsLiteral : literal -> NameAritySet.set 83 84val relationLiteral : literal -> Atom.relation option 85 86val freeVarsLiteral : literal -> NameSet.set 87 88(* ------------------------------------------------------------------------- *) 89(* TPTP formula names. *) 90(* ------------------------------------------------------------------------- *) 91 92datatype formulaName = 93 FormulaName of string 94 95val ppFormulaName : formulaName Print.pp 96 97(* ------------------------------------------------------------------------- *) 98(* TPTP formula bodies. *) 99(* ------------------------------------------------------------------------- *) 100 101datatype formulaBody = 102 CnfFormulaBody of literal list 103 | FofFormulaBody of Formula.formula 104 105(* ------------------------------------------------------------------------- *) 106(* TPTP formula sources. *) 107(* ------------------------------------------------------------------------- *) 108 109datatype formulaSource = 110 NoFormulaSource 111 | StripFormulaSource of 112 {inference : string, 113 parents : formulaName list} 114 | NormalizeFormulaSource of 115 {inference : Normalize.inference, 116 parents : formulaName list} 117 | ProofFormulaSource of 118 {inference : Proof.inference, 119 parents : formulaName list} 120 121(* ------------------------------------------------------------------------- *) 122(* TPTP formulas. *) 123(* ------------------------------------------------------------------------- *) 124 125datatype formula = 126 Formula of 127 {name : formulaName, 128 role : role, 129 body : formulaBody, 130 source : formulaSource} 131 132val nameFormula : formula -> formulaName 133 134val roleFormula : formula -> role 135 136val bodyFormula : formula -> formulaBody 137 138val sourceFormula : formula -> formulaSource 139 140val functionsFormula : formula -> NameAritySet.set 141 142val relationsFormula : formula -> NameAritySet.set 143 144val freeVarsFormula : formula -> NameSet.set 145 146val freeVarsListFormula : formula list -> NameSet.set 147 148val isCnfConjectureFormula : formula -> bool 149val isFofConjectureFormula : formula -> bool 150val isConjectureFormula : formula -> bool 151 152(* ------------------------------------------------------------------------- *) 153(* Clause information. *) 154(* ------------------------------------------------------------------------- *) 155 156datatype clauseSource = 157 CnfClauseSource of formulaName * literal list 158 | FofClauseSource of Normalize.thm 159 160type 'a clauseInfo = 'a LiteralSetMap.map 161 162type clauseNames = formulaName clauseInfo 163 164type clauseRoles = role clauseInfo 165 166type clauseSources = clauseSource clauseInfo 167 168val noClauseNames : clauseNames 169 170val noClauseRoles : clauseRoles 171 172val noClauseSources : clauseSources 173 174(* ------------------------------------------------------------------------- *) 175(* TPTP problems. *) 176(* ------------------------------------------------------------------------- *) 177 178type comments = string list 179 180type includes = string list 181 182datatype problem = 183 Problem of 184 {comments : comments, 185 includes : includes, 186 formulas : formula list} 187 188val hasCnfConjecture : problem -> bool 189val hasFofConjecture : problem -> bool 190val hasConjecture : problem -> bool 191 192val freeVars : problem -> NameSet.set 193 194val mkProblem : 195 {comments : comments, 196 includes : includes, 197 names : clauseNames, 198 roles : clauseRoles, 199 problem : Problem.problem} -> problem 200 201val normalize : 202 problem -> 203 {subgoal : Formula.formula * formulaName list, 204 problem : Problem.problem, 205 sources : clauseSources} list 206 207val goal : problem -> Formula.formula 208 209val read : {mapping : mapping, filename : string} -> problem 210 211val write : 212 {problem : problem, 213 mapping : mapping, 214 filename : string} -> unit 215 216val prove : {filename : string, mapping : mapping} -> bool 217 218(* ------------------------------------------------------------------------- *) 219(* TSTP proofs. *) 220(* ------------------------------------------------------------------------- *) 221 222val fromProof : 223 {problem : problem, 224 proofs : {subgoal : Formula.formula * formulaName list, 225 sources : clauseSources, 226 refutation : Thm.thm} list} -> formula list 227 228end 229