14
15:- module(drs_to_tptp, [
16 drs_to_tptp/2,
17 drs_to_tptplist/2,
18 tptp_pp/1,
19 tptplist_pp/1
20 ]). 21
22:- use_module(drs_to_drslist, [
23 drs_to_drslist/2
24 ]).
65drs_to_tptplist(Drs, TptpList) :-
66 drs_to_drslist(Drs, DrsList),
67 maplist(drs_to_tptp, DrsList, TptpList).
75drs_to_tptp(drs([], [question(drs(Dom, Conds))]), fof(conjecture, Expr)) :-
76 !,
77 drs_to_tptp_x(drs(Dom, Conds), Expr).
78
79drs_to_tptp(drs(Dom, Conds), fof(axiom, Expr)) :-
80 drs_to_tptp_x(drs(Dom, Conds), Expr).
81
82
83drs_to_tptp_x(drs(Dom, Conds), Expr) :-
84 conds_tptp(Dom, Conds, NDom, NConds),
85 get_quantifier_expression('?', NDom, NConds, Expr).
90conds_tptp(Dom, [Cond], NDom, NCond) :-
91 tptp(Dom, Cond, NDom, NCond).
92
93conds_tptp(Dom, [Cond1, Cond2 | Tail], NDom, '&'(NCond1, NTail)) :-
94 tptp(Dom, Cond1, NDomTmp, NCond1),
95 conds_tptp(NDomTmp, [Cond2 | Tail], NDom, NTail).
100get_quantifier_expression(_, [], Expr, Expr) :- !.
101get_quantifier_expression('?', Vars, Expr, ':'('?'(Vars), Expr)).
102get_quantifier_expression('!', Vars, Expr, ':'('!'(Vars), Expr)).
107tptp(
108 UpperDom,
109 '=>'(drs(Dom1, Conds1), drs(Dom2, Conds2)),
110 UpperDom,
111 Expr
112) :-
113 !,
114 conds_tptp(Dom1, Conds1, NDom1, NConds1),
115 conds_tptp(Dom2, Conds2, NDom2, NConds2),
116 get_quantifier_expression('?', NDom2, NConds2, Expr2),
117 get_quantifier_expression('!', NDom1, '=>'(NConds1, Expr2), Expr).
118
119tptp(
120 UpperDom,
121 'v'(drs(Dom1, Conds1), drs(Dom2, Conds2)),
122 UpperDom,
123 Expr
124) :-
125 !,
126 conds_tptp(Dom1, Conds1, NDom1, NConds1),
127 conds_tptp(Dom2, Conds2, NDom2, NConds2),
128 get_quantifier_expression('?', NDom2, NConds2, Expr2),
129 get_quantifier_expression('?', NDom1, '|'(NConds1, Expr2), Expr).
130
131tptp(
132 UpperDom,
133 '-'(drs(Dom, Conds)),
134 UpperDom,
135 '~'(QExpr)
136) :-
137 !,
138 conds_tptp(Dom, Conds, NDom, NConds),
139 get_quantifier_expression('?', NDom, NConds, QExpr).
140
141tptp(Dom, predicate(X, be, A, B)-_, NDom, '='(NA, NB)) :-
142 !,
143 exclude(==(X), Dom, NDom),
144 arg_to_tptp(A, NA),
145 arg_to_tptp(B, NB).
146
147tptp(Dom, object(_, Lemma, _, _, _, _)-_, Dom, $true) :-
148 is_thing(Lemma),
149 !.
150
151tptp(Dom, object(Var, Lemma, _, _, eq, 1)-_, Dom, Pred) :-
152 !,
153 Pred =.. [Lemma, Var].
154
156tptp(Dom, Cond-_, Dom, Tptp) :-
157 !,
158 cond_to_tptp(Cond, Tptp).
159
160tptp(_, Term, _, _) :-
161 functor(Term, Functor, _),
162 concat_atom(['DRS condition not supported', Functor], ': ', Message),
163 throw(error(Message, context(tptp/4, Term))).
169cond_to_tptp(formula(R1, Symbol, R2), Pred) :-
170 arg_to_tptp(R1, NR1),
171 arg_to_tptp(R2, NR2),
172 atom(Symbol),
173 member(Symbol, ['<', '>', '=', '\\=', '>=', '=<']),
174 Pred =.. [Symbol, NR1, NR2].
175
176cond_to_tptp(object(A, B, C, D, E, F), object(A, B, C, D, E, F)).
177
178cond_to_tptp(modifier_adv(R, Lexem, Degree), modifier_adv(R, Lexem, Degree)) :-
179 var(R),
180 atom(Degree),
181 member(Degree, [pos, comp, sup]),
182 atom(Lexem).
183
184cond_to_tptp(modifier_pp(R1, Prep, R2), modifier_pp(R1, Prep, NR2)) :-
185 var(R1),
186 atom(Prep),
187 arg_to_tptp(R2, NR2).
188
189cond_to_tptp(property(R, Lexem, Comp), property1(R, Lexem, Comp)) :-
190 var(R),
191 atom(Comp),
192 member(Comp, [pos, comp, sup]),
193 atom(Lexem).
194
195cond_to_tptp(property(R1, Lexem, Comp, R2), property2(R1, Lexem, Comp, NR2)) :-
196 var(R1),
197 arg_to_tptp(R2, NR2),
198 atom(Comp),
199 member(Comp, [pos, pos_as, comp, comp_than, sup]),
200 atom(Lexem).
201
202cond_to_tptp(property(R1, Lexem, R2, Comp, SubjObj, R3), property3(R1, Lexem, NR2, Comp, SubjObj, NR3)) :-
203 var(R1),
204 arg_to_tptp(R2, NR2),
205 arg_to_tptp(R3, NR3),
206 atom(Comp),
207 member(Comp, [pos_as, comp_than]),
208 atom(SubjObj),
209 member(SubjObj, [subj, obj]),
210 atom(Lexem).
211
212cond_to_tptp(predicate(R1, Lexem, R2), predicate1(R1, Lexem, NR2)) :-
213 var(R1),
214 arg_to_tptp(R2, NR2),
215 atom(Lexem).
216
217cond_to_tptp(predicate(R1, Lexem, R2, R3), predicate2(R1, Lexem, NR2, NR3)) :-
218 var(R1),
219 arg_to_tptp(R2, NR2),
220 arg_to_tptp(R3, NR3),
221 atom(Lexem).
222
223cond_to_tptp(predicate(R1, Lexem, R2, R3, R4), predicate3(R1, Lexem, NR2, NR3, NR4)) :-
224 var(R1),
225 arg_to_tptp(R2, NR2),
226 arg_to_tptp(R3, NR3),
227 arg_to_tptp(R4, NR4),
228 atom(Lexem).
229
230cond_to_tptp(relation(R1, of, R2), relation(R1, of, NR2)) :-
231 var(R1),
232 arg_to_tptp(R2, NR2).
233
234cond_to_tptp(has_part(R1, R2), has_part(R1, NR2)) :-
235 var(R1),
236 arg_to_tptp(R2, NR2).
237
238cond_to_tptp(query(R, Lexem), _) :-
239 throw(error('DRS query/2 not supported', context(cond_to_tptp/2, query(R, Lexem)))).
245arg_to_tptp(Arg, Arg) :-
246 var(Arg),
247 !.
248
249arg_to_tptp(named(Arg), Arg) :-
250 atom(Arg).
251
252arg_to_tptp(int(Arg), Arg) :-
253 integer(Arg).
254
255arg_to_tptp(real(Arg), Arg) :-
256 float(Arg).
257
258arg_to_tptp(int(Arg, Unit), int(Arg, Unit)) :-
259 integer(Arg),
260 atom(Unit).
261
262arg_to_tptp(real(Arg, Unit), real(Arg, Unit)) :-
263 float(Arg),
264 atom(Unit).
265
266arg_to_tptp(string(Arg), string(Arg)) :-
267 atomic(Arg).
268
269arg_to_tptp(list(List), _) :-
270 throw(error('DRS function list/1 not supported', context(arg_to_tptp/2, list(List)))).
271
272arg_to_tptp(set(Set), _) :-
273 throw(error('DRS function set/1 not supported', context(arg_to_tptp/2, set(Set)))).
274
275arg_to_tptp(expr('&', Arg1, Arg2), _) :-
276 throw(error('DRS operator \'&\' not supported', context(arg_to_tptp/2, expr('&', Arg1, Arg2)))).
277
278arg_to_tptp(expr(Op, Arg1, Arg2), Expr) :-
279 arg_to_tptp(Arg1, NArg1),
280 arg_to_tptp(Arg2, NArg2),
281 atom(Op),
282 member(Op, ['+', '-', '*', '/']),
283 Expr =.. [Op, NArg1, NArg2].
289is_thing(somebody).
290is_thing(something).
300tptplist_pp(TptpList) :-
301 tptplist_pp(1, f, TptpList).
314tptplist_pp(_, _, []).
315
316tptplist_pp(Index, Prefix, [Tptp]) :-
317 tptp_pp(Index, Prefix, Tptp).
318
319tptplist_pp(Index, Prefix, [Tptp1, Tptp2 | Rest]) :-
320 tptp_pp(Index, Prefix, Tptp1),
321 nl, nl,
322 NewIndex is Index + 1,
323 tptplist_pp(NewIndex, Prefix, [Tptp2 | Rest]).
327tptp_pp(Index, Prefix, fof(Role, Expr)) :-
328 concat_atom([Prefix, Index], Name),
329 tptp_pp(fof(Name, Role, Expr)).
336tptp_pp(fof(Role, Expr)) :-
337 tptp_pp(fof(name, Role, Expr)).
338
339tptp_pp(fof(Name, Role, Expr)) :-
340 format("fof(~w, ~w, (~n", [Name, Role]),
341 numbervars(Expr, 0, _),
342 tptp_pp_(Expr),
343 format(")).", []),
344 fail ; true.
345
346tptp_pp_(':'('?'(Vars), F)) :-
347 !,
348 write_term('?', [quoted(true)]),
349 write(' '),
350 write_term(Vars, [numbervars(true), quoted(true)]),
351 write(' : '),
352 tptp_pp_wrap(F).
353
354tptp_pp_(':'('!'(Vars), F)) :-
355 !,
356 write_term('!', [quoted(true)]),
357 format(" ", []),
358 write_term(Vars, [numbervars(true), quoted(true)]),
359 format(" : ", []),
360 tptp_pp_wrap(F).
361
362tptp_pp_('=>'(A, B)) :-
363 !,
364 tptp_pp_wrap(A),
365 format("~n=> ", []),
366 tptp_pp_wrap(B).
367
368tptp_pp_('|'(A, B)) :-
369 !,
370 tptp_pp_wrap(A),
371 format("~n| ", []),
372 tptp_pp_wrap(B).
373
374tptp_pp_('&'(A, B)) :-
375 !,
376 tptp_pp_wrap(A),
377 format(" &~n", []),
378 tptp_pp_wrap(B).
379
380tptp_pp_('~'(A)) :-
381 !,
382 write('~'),
383 tptp_pp_wrap(A).
384
385tptp_pp_(A) :-
386 write_term(A, [numbervars(true), quoted(true)]).
387
388
389tptp_pp_wrap(A) :-
390 write('('),
391 tptp_pp_(A),
392 write(')')
DRS to TPTP converter
Converts DRSs to fof-axioms, except for yes/no question-conditions which are converted to fof-conjectures. Some DRS conditions are not supported, causing an exception to be thrown if encountered.
TODO
: