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