author | blanchet |
Fri, 17 Sep 2010 01:56:19 +0200 | |
changeset 39501 | aaa7078fff55 |
parent 39444 | beabb8443ee4 |
child 39502 | cffceed8e7fa |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* THE TPTP PROBLEM FILE FORMAT *) |
|
39501
aaa7078fff55
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet
parents:
39444
diff
changeset
|
3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the MIT 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 |