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