2:- module(drs2fol,[drs2fol/2,symbol/4,timex/2]). 3
4:- use_module(semlib(errors),[warning/2]). 5:- use_module(semlib(options),[option/2]). 6:- use_module(library(lists),[append/3]). 7
8
12
13drs2fol(B,some(W,and(possible_world(W),F))):-
14 option('--modal',true), !,
15 drsfol(B,W,F).
16
17drs2fol(B,F):-
18 option('--modal',false), !,
19 drsfol(B,F).
20
21
25
26drsfol(lab(_,B),Form):- !, drsfol(B,Form).
27
28drsfol(sub(B1,B2),Form):- !, drsfol(merge(B1,B2),Form).
29
30drsfol(sdrs([B],_),Form):- !, drsfol(B,Form).
31
32drsfol(sdrs([B|L],C),Form):- !, drsfol(merge(B,sdrs(L,C)),Form).
33
34drsfol(alfa(_,B1,B2),Form):- !, drsfol(merge(B1,B2),Form).
35
36drsfol(drs([],[Cond]),Formula):- !, cond2fol(Cond,Formula).
37
38drsfol(drs([],[Cond1,Cond2|Conds]),and(Formula1,Formula2)):- !,
39 cond2fol(Cond1,Formula1), drsfol(drs([],[Cond2|Conds]),Formula2).
40
41drsfol(drs([Indexed|Referents],Conds),Formula):-
42 nonvar(Indexed), !, Indexed=_:Var,
43 drsfol(drs([Var|Referents],Conds),Formula).
44
45drsfol(drs([X|Referents],Conds),some(X,and(some(Y,member(Y,X)),Formula))):-
46 option('--plural',true), !,
47 drsfol(drs(Referents,Conds),Formula).
48
49drsfol(drs([X|Referents],Conds),some(X,Formula)):-
50 option('--plural',false), !,
51 drsfol(drs(Referents,Conds),Formula).
52
53drsfol(merge(B1,B2),Formula):- !,
54 drsfolGap(B1,Gap^Formula), drsfol(B2,Gap).
55
56drsfol(X,_):-
57 warning('drsfol/2 failed for: ~p',[X]), fail.
58
59
63
64drsfol(lab(_,B),W,Form):- !, drsfol(B,W,Form).
65
66drsfol(sub(B1,B2),W,Form):- !, drsfol(merge(B1,B2),W,Form).
67
68drsfol(sdrs([B],_),W,Form):- !, drsfol(B,W,Form).
69
70drsfol(sdrs([B|L],C),W,Form):- !, drsfol(merge(B,sdrs(L,C)),W,Form).
71
72drsfol(alfa(_,B1,B2),W,Form):- !, drsfol(merge(B1,B2),W,Form).
73
74drsfol(drs([],[Cond]),W,Formula):- !, cond2fol(Cond,W,Formula).
75
76drsfol(drs([],[Cond1,Cond2|Conds]),W,and(Formula1,Formula2)):- !,
77 cond2fol(Cond1,W,Formula1), drsfol(drs([],[Cond2|Conds]),W,Formula2).
78
79drsfol(drs([Indexed|Referents],Conds),W,Formula):-
80 nonvar(Indexed), !, Indexed=_:Var,
81 drsfol(drs([Var|Referents],Conds),W,Formula).
82
83drsfol(drs([X|Referents],Conds),W,some(X,Formula)):- !,
84 drsfol(drs(Referents,Conds),W,Formula).
85
86drsfol(merge(B1,B2),W,Form):- !,
87 drsfolGap(B1,W,Gap^Form), drsfol(B2,W,Gap).
88
89drsfol(X,_,_):-
90 warning('drsfol/3 failed for: ~p',[X]), fail.
91
92
99
100drsfolGap(sdrs([B],_),F):- !, drsfolGap(B,F).
101
102drsfolGap(sdrs([B|L],C),F):- !, drsfolGap(merge(B,sdrs(L,C)),F).
103
104drsfolGap(lab(_,B),F):- !, drsfolGap(B,F).
105
106drsfolGap(sub(B1,B2),F):- !, drsfolGap(merge(B1,B2),F).
107
108drsfolGap(alfa(_,B1,B2),Gap^F):- !, drsfolGap(merge(B1,B2),Gap^F).
109
110drsfolGap(merge(B1,B2),Gap2^F):- !,
111 drsfolGap(B1,Gap1^F), drsfolGap(B2,Gap2^Gap1).
112
113drsfolGap(drs([Indexed|Refs],Conds),F):-
114 nonvar(Indexed), !, Indexed=_:Ref,
115 drsfolGap(drs([Ref|Refs],Conds),F).
116
117drsfolGap(drs([X],[]),Gap^some(X,and(some(Y,member(Y,X)),Gap))):-
118 option('--plural',true), !.
119
120drsfolGap(drs([X|Dom],Conds),Gap^some(X,and(some(Y,member(Y,X)),F))):-
121 option('--plural',true), !,
122 drsfolGap(drs(Dom,Conds),Gap^F).
123
124drsfolGap(drs([X],[]),Gap^some(X,Gap)):-
125 option('--plural',false), !.
126
127drsfolGap(drs([X|Dom],Conds),Gap^some(X,F)):-
128 option('--plural',false), !,
129 drsfolGap(drs(Dom,Conds),Gap^F).
130
131drsfolGap(drs([],Conds),Gap^and(F,Gap)):- !,
132 drsfol(drs([],Conds),F).
133
134drsfolGap(X,_):-
135 warning('drsfolGap/2 failed for: ~p',[X]), fail.
136
137
144
145drsfolGap(sdrs([B],_),W,F):- !, drsfolGap(B,W,F).
146
147drsfolGap(sdrs([B|L],C),W,F):- !, drsfolGap(merge(B,sdrs(L,C)),W,F).
148
149drsfolGap(lab(_,B),W,F):- !, drsfolGap(B,W,F).
150
151drsfolGap(sub(B1,B2),W,F):- !, drsfolGap(merge(B1,B2),W,F).
152
153drsfolGap(alfa(_,B1,B2),W,Gap^F):- !, drsfolGap(merge(B1,B2),W,Gap^F).
154
155drsfolGap(merge(B1,B2),W,Gap2^F):- !,
156 drsfolGap(B1,W,Gap1^F), drsfolGap(B2,W,Gap2^Gap1).
157
158drsfolGap(drs([Indexed|Referents],Conds),W,Formula):-
159 nonvar(Indexed), !, Indexed=_:Var,
160 drsfolGap(drs([Var|Referents],Conds),W,Formula).
161
162drsfolGap(drs([X],[]),_,Gap^some(X,Gap)):- !.
163
164drsfolGap(drs([X|Dom],Conds),W,Gap^some(X,F)):- !,
165 drsfolGap(drs(Dom,Conds),W,Gap^F).
166
167drsfolGap(drs([],Conds),W,Gap^and(F,Gap)):- !,
168 drsfol(drs([],Conds),W,F).
169
170drsfolGap(X,_,_):-
171 warning('drsfolGap/3 failed for: ~p',[X]), fail.
172
173
177
178cond2fol(_:C,F):- !,
179 cond2fol(C,F).
180
181cond2fol(not(Drs),not(Formula)):- !,
182 drsfol(Drs,Formula).
183
184cond2fol(prop(_,Drs),Formula):- !,
185 drsfol(Drs,Formula).
186
187cond2fol(or(Drs1,Drs2),or(Formula1,Formula2)):- !,
188 drsfol(Drs1,Formula1),
189 drsfol(Drs2,Formula2).
190
191cond2fol(whq(Drs1,Drs2),F):- !,
192 cond2fol(imp(Drs1,Drs2),F).
193
194cond2fol(duplex(most,Drs1,X,Drs2),and(F1,all(Z,imp(F3,F4)))):- !,
195 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:not(drs([[]:Y],[[]:rel(Y,X,g,1)]))]))),F1),
196 197 drs2fol(merge(Drs1,drs([],[[]:eq(X,Z),[]:not(Drs2)])),F3),
198 199 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:rel(Z,X,g,1)]))),F4).
200
201cond2fol(duplex(two,Drs1,X,Drs2),some(A,some(B,and(not(eq(A,B)),and(all(Z,imp(F0,or(eq(Z,A),eq(Z,B)))),and(F1,F2)))))):- !,
202 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:eq(X,A)]))),F1),
203 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:eq(X,B)]))),F2),
204 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:eq(X,Z)]))),F0).
205
206cond2fol(duplex(three,Drs1,X,Drs2),some(A,some(B,some(C,and(not(eq(A,B)),and(not(eq(A,C)),and(not(eq(B,C)),and(all(Z,imp(F0,or(eq(Z,A),or(eq(Z,B),eq(Z,C))))),and(F1,and(F2,F3)))))))))):- !,
207 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:eq(X,A)]))),F1),
208 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:eq(X,B)]))),F2),
209 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:eq(X,C)]))),F3),
210 drs2fol(merge(Drs1,merge(Drs2,drs([],[[]:eq(X,Z)]))),F0).
211
212cond2fol(duplex(_,Drs1,_,Drs2),F):- !,
213 cond2fol(imp(Drs1,Drs2),F).
214
215cond2fol(imp(B1,B2),Formula):- !,
216 cond2fol(not(merge(B1,drs([],[not(B2)]))),Formula).
217
218cond2fol(card(X,1,eq),one(X)):- option('--plural',true), !.
219
220cond2fol(card(X,2,eq),two(X)):- option('--plural',true), !.
221
222cond2fol(card(X,3,eq),three(X)):- option('--plural',true), !.
223
224cond2fol(card(X,C,_),some(Y,and(card(X,Y),and(F1,F2)))):-
225 integer(C), C > 0,
226 symbol(c,number,C,S1),
227 symbol(n,numeral,1,S2), !,
228 F1=..[S1,Y],
229 F2=..[S2,Y].
230
231cond2fol(card(X,_,_),some(Y,and(card(X,Y),F2))):-
232 symbol(n,numeral,1,S2), !,
233 F2=..[S2,Y].
234
235cond2fol(named(X,N1,Type,Sense),F):-
236 symbol(Type,N1,Sense,N2), !,
237 F=..[N2,X].
238
239cond2fol(timex(X,D1),F):-
240 timex(D1,D2),
241 F=..[D2,X], !.
242
243cond2fol(eq(X),eq(X,X)):- !.
244
245cond2fol(eq(X,Y),eq(X,Y)):- !.
246
247cond2fol(pred(X,Sym1,Type,Sense),all(Y,imp(member(Y,X),F))):-
248 option('--plural',true),
249 symbol(Type,Sym1,Sense,Sym2), !,
250 F=..[Sym2,Y].
251
252cond2fol(pred(X,Sym1,Type,Sense),F):-
253 option('--plural',false),
254 symbol(Type,Sym1,Sense,Sym2), !,
255 F=..[Sym2,X].
256
257cond2fol(rel(X,Y,Sym1,Sense),all(A,imp(member(A,X),all(B,imp(member(B,Y),F))))):-
258 option('--plural',true),
259 symbol(r,Sym1,Sense,Sym2), !,
260 F=..[Sym2,A,B].
261
262cond2fol(rel(X,Y,Sym1,Sense),F):-
263 option('--plural',false),
264 symbol(r,Sym1,Sense,Sym2), !,
265 F=..[Sym2,X,Y].
266
267cond2fol(role(X,Y,Sym1,1),F):-
268 symbol(r,Sym1,1,Sym2), !,
269 F=..[Sym2,X,Y].
270
271cond2fol(role(X,Y,Sym1,-1),F):-
272 symbol(r,Sym1,1,Sym2), !,
273 F=..[Sym2,Y,X].
274
275cond2fol(X,_):-
276 warning('cond2fol/2 failed for ~p',[X]), fail.
277
278
282
283cond2fol(_:C,W,F):- !,
284 cond2fol(C,W,F).
285
286cond2fol(not(Drs),W,not(Formula)):- !,
287 drsfol(Drs,W,Formula).
288
289cond2fol(nec(Drs),_,all(V,imp(possible_world(V),Formula))):- !,
290 drsfol(Drs,V,Formula).
291
292cond2fol(pos(Drs),_,some(V,and(possible_world(V),Formula))):- !,
293 drsfol(Drs,V,Formula).
294
295cond2fol(prop(V,Drs),_,Formula):- !,
296 drsfol(Drs,V,Formula).
297
298cond2fol(or(Drs1,Drs2),W,or(Formula1,Formula2)):- !,
299 drsfol(Drs1,W,Formula1),
300 drsfol(Drs2,W,Formula2).
301
302cond2fol(whq(Drs1,Drs2),W,F):- !,
303 cond2fol(imp(Drs1,Drs2),W,F).
304
305cond2fol(duplex(_,Drs1,_,Drs2),W,F):- !,
306 cond2fol(imp(Drs1,Drs2),W,F).
307
308cond2fol(imp(B1,B2),W,Formula):- !,
309 cond2fol(not(merge(B1,drs([],[not(B2)]))),W,Formula).
310
311cond2fol(card(X,C,_),W,some(Y,and(card(W,X,Y),and(F1,F2)))):-
312 integer(C), C > 0,
313 symbol(c,number,C,S1),
314 symbol(n,numeral,1,S2), !,
315 F1=..[S1,W,Y],
316 F2=..[S2,W,Y].
317
318cond2fol(card(X,_,_),W,some(Y,and(card(W,X,Y),F2))):-
319 symbol(n,numeral,1,S2), !,
320 F2=..[S2,W,Y].
321
322cond2fol(named(X,N1,Type,Sense),W,F):-
323 symbol(Type,N1,Sense,N2), !,
324 F=..[N2,W,X].
325
326cond2fol(timex(X,D1),W,F):-
327 timex(D1,D2),
328 F=..[D2,W,X], !.
329
330cond2fol(eq(X,Y),_,eq(X,Y)):- !.
331
332cond2fol(eq(X),W,eq(W,X)):- !.
333
334cond2fol(pred(X,Sym1,Type,Sense),W,F):-
335 symbol(Type,Sym1,Sense,Sym2), !,
336 F=..[Sym2,W,X].
337
338cond2fol(rel(X,Y,Sym1,Sense),W,F):-
339 symbol(r,Sym1,Sense,Sym2), !,
340 F=..[Sym2,W,X,Y].
341
342cond2fol(role(X,Y,Sym1,1),W,F):-
343 symbol(r,Sym1,1,Sym2), !,
344 F=..[Sym2,W,X,Y].
345
346cond2fol(role(X,Y,Sym1,-1),W,F):-
347 symbol(r,Sym1,1,Sym2), !,
348 F=..[Sym2,W,Y,X].
349
350cond2fol(X,_,_):-
351 warning('cond2fol/2 failed for ~p',[X]), fail.
352
353
357
358symbol(t,D,_Sense,F):- !, timex(D,F).
359
360symbol(Type,F1,0,F2):- !, symbol(Type,F1,1,F2). 361
362symbol(Type,F1,Sense,F2):-
363 atom_codes(Type,A0),
364 ( number(Sense), !, number_codes(Sense,A1); atom_codes(Sense,A1) ),
365 append(A0,A1,A2),
366 ( atom(F1), !, atom_codes(F1,A3)
367 ; number(F1), number_codes(F1,A3) ),
368 normSymbol(A3,A4),
369 append(A2,A4,A5),
370 maxLen(A5,A6),
371 atom_codes(F2,A6).
372
373
377
378maxLen(In,Out):-
379 In = [A0,A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,B0,C1,C2,C3,C4,C5,C6,C7,C8,C9,C0,D1,_|_], !,
380 Out = [A0,A1,A2,A3,A4,A5,A6,A7,A8,A9,B1,B2,B3,B4,B5,B6,B7,B8,B9,B0,C1,C2,C3,C4,C5,C6,C7,C8,C9,C0,D1],
381 atom_codes(Symbol1,In),
382 atom_codes(Symbol2,Out),
383 warning('symbol ~p too long, cut to ~p',[Symbol1,Symbol2]).
384
385maxLen(L,L).
386
387
391
392normSymbol([],[]):- !.
393
394normSymbol([95|L1],[95|L2]):- !, normSymbol(L1,L2).
395
396normSymbol([X|L1],[X|L2]):- X > 64, X < 91, !, normSymbol(L1,L2).
397
398normSymbol([X|L1],[X|L2]):- X > 96, X < 123, !, normSymbol(L1,L2).
399
400normSymbol([X|L1],[X|L2]):- X > 47, X < 58, !, normSymbol(L1,L2).
401
402normSymbol([X|L1],L3):-
403 number_codes(X,Codes),
404 append([67|Codes],L2,L3),
405 normSymbol(L1,L2).
406
407
411
412timex(date(_:_,_:Y,_:M,_:D),Timex):- !,
413 timex(date(Y,M,D),Timex).
414
415timex(date(_:Y,_:M,_:D),Timex):- !,
416 timex(date(Y,M,D),Timex).
417
418timex(time(_:H,_:M,_:S),Timex):- !,
419 timex(time(H,M,S),Timex).
420
421timex(date(Y,M,D),Timex):-
422 year(Y,[Y1,Y2,Y3,Y4]),
423 month(M,[M1,M2]),
424 day(D,[D1,D2]),
425 name(Timex,[116,95,Y1,Y2,Y3,Y4,M1,M2,D1,D2]).
426
427timex(time(H,M,S),Timex):-
428 hour(H,[H1,H2]),
429 minute(M,[M1,M2]),
430 second(S,[S1,S2]),
431 name(Timex,[116,95,H1,H2,M1,M2,S1,S2]).
432
433
437
438year(Y,C):- variable(Y), !, name('XXXX',C).
439year(Y,C):- name(Y,C).
440
441
445
446month(Y,C):- variable(Y), !, name('XX',C).
447month(Y,C):- name(Y,C).
448
449
453
454day(Y,C):- variable(Y), !, name('XX',C).
455day(Y,C):- name(Y,C).
456
457
461
462hour(A,C):- day(A,C).
463minute(A,C):- day(A,C).
464second(A,C):- day(A,C).
465
466
470
471variable(X):- var(X), !.
472variable(X):- functor(X,'$VAR',1), !