/*========================================================================
File Search Paths
========================================================================*/
file_search_path(semlib, 'src/prolog/lib').
file_search_path(nutcracker, 'src/prolog/nutcracker').
file_search_path(boxer, 'src/prolog/boxer').
file_search_path(knowledge, 'src/prolog/boxer/knowledge').
/*========================================================================
Load other libraries
========================================================================*/
:- use_module(library(lists),[select/3,append/3]).
:- use_module(boxer(slashes)).
:- use_module(boxer(printDrs),[printDrs/2]).
:- use_module(nutcracker(callInference),[callTPandMB/7]).
:- use_module(semlib(options),[option/2,parseOptions/2,setOption/3,
showOptions/1,setDefaultOptions/1]).
:- dynamic chart/5.
/* ----------------------------------------------------------------------------------
Simple Lexicon
---------------------------------------------------------------------------------- */
lex(every, (s/(s\np))/n, (x1-C)-((((x1-B)-drs([],[imp(drs([[]:x1],[pos(C)]),B)]))-D)-D) ).
lex(two, (s/(s\np))/n, (x1-C)-((((x1-B)-drs([[]:x2],[pred(x2,two,n,1),imp(drs([[]:x1],[rel(x1,x2,member,1)]),C),imp(drs([[]:x1],[rel(x1,x2,member,1)]),B)]))-D)-D) ).
lex(three, (s/(s\np))/n, (x1-C)-((((x1-B)-drs([[]:x2],[pred(x2,three,n,1),imp(drs([[]:x1],[rel(x1,x2,member,1)]),C),imp(drs([[]:x1],[rel(x1,x2,member,1)]),B)]))-D)-D) ).
lex(four, (s/(s\np))/n, (x1-C)-((((x1-B)-drs([[]:x2],[pred(x2,four,n,1),imp(drs([[]:x1],[rel(x1,x2,member,1)]),C),imp(drs([[]:x1],[rel(x1,x2,member,1)]),B)]))-D)-D) ).
lex(a, np/n, (x1-C)-((x1-B)-drs([[]:x1],[pos(C),pos(B)])) ).
lex(big, n/n, (x1-B)-(x1-drs([],[pred(x1,big,a,0),pos(B)])) ).
lex(man, n, x1-drs([],[pred(x1,man,n,0)]) ).
lex(men, n, x1-drs([],[pred(x1,man,n,0)]) ).
lex(woman, n, x1-drs([],[pred(x1,woman,n,0)]) ).
lex(someone, np, (x1-B)-drs([[]:x1],[pred(x1,person,n,1),pos(B)]) ).
lex(herself, np, (x1-B)-drs([],[pred(x1,female,n,0),pos(B)]) ).
lex(mia, np, (x1-B)-drs([[]:x1],[named(x1,mia,per,0),pos(B)]) ).
lex(lou, np, (x1-B)-drs([[]:x1],[named(x1,lou,per,0),pos(B)]) ).
lex(andy, np, (x1-B)-drs([[]:x1],[named(x1,andy,per,0),pos(B)]) ).
lex(mia, s/(s\np), ((x1-B)-drs([[]:x1],[named(x1,mia,per,0),pos(B)])-C)-C ).
lex(everyone, s/(s\np), ((x1-B)-drs([],[imp(drs([[]:x1],[pred(x1,person,n,1)]),B)])-C)-C ).
lex(slowly, (s\np)\(s\np), ((x2-drs([],[pred(x2,slow,a,0),pos(C)]))-B)-((x2-C)-B) ).
lex(slowly, s\s, ((x2-drs([],[pred(x2,slow,a,0),pos(C)]))-B)-((x2-C)-B) ).
lex(smokes, s\np, (((x1-drs([[]:x2],[pred(x2,smoke,v,0),rel(x2,x1,theme,0),pos(B)]))-C)-((x2-B)-C)) ).
lex(smoke, s\np, (((x1-drs([[]:x2],[pred(x2,smoke,v,0),rel(x2,x1,theme,0),pos(B)]))-C)-((x2-B)-C)) ).
lex(saw, (s\np)/np, ((x1-drs([],[rel(x2,x1,theme,0),pos(D)]))-B)-(((x1-drs([[]:x2],[pred(x2,see,v,0),rel(x2,x1,agent,0),pos(B)]))-C)-((x2-D)-C)) ).
lex(and, (np/np)\np, ((x1-drs([],[rel(x1,x2,member,1)]))-B1)-(((x1-drs([],[rel(x1,x2,member,1)]))-B2)-((x1-B)-drs([[]:x2],[pos(B1),pos(B2),imp(drs([[]:x1],[rel(x1,x2,member,1)]),B)])))).
lex('.', t\s, ((x2-drs([],[pred(x2,event,v,0)]))-B)-B ).
/* ----------------------------------------------------------------------------------
Combinatory Rules
---------------------------------------------------------------------------------- */
combine(A,B,C,D,E,fa(D,E)):- fa(A,B,C).
combine(A,B,C,D,E,ba(D,E)):- ba(A,B,C).
combine(A,B,C,D,E,fc(D,E)):- fc(A,B,C).
/* ----------------------------------------------------------------------------------
CCG
---------------------------------------------------------------------------------- */
fa((A/B):X-Y, B:X, A:Y).
ba(A:X, (B\A):X-Y, B:Y).
fc((A/B):X-Y, (B/C):Z-X, (A/C):Z-Y).
/* ----------------------------------------------------------------------------------
Examples
---------------------------------------------------------------------------------- */
example( 1, [mia,smokes,'.']).
example( 2, [two,men,smoke,'.']).
example( 3, [every,man,smokes,'.']).
example( 4, [a,woman,smokes,'.']).
example( 5, [mia,saw,a,man,'.']).
example( 6, [every,big,man,smokes,'.']).
example( 7, [every,big,man,saw,a,big,man,'.']).
example( 8, [two,men,saw,a,woman,'.']).
example( 9, [three,men,saw,a,woman,'.']).
example(10, [four,men,saw,a,woman,'.']).
example(20, [lou,and,andy,smoke,'.']).
example(21, [lou,and,andy,saw,a,woman,'.']).
example(31, [two,men,smoke,'.']).
example(32, [a,man,smokes,'.']).
example(33, [three,men,smoke,'.']).
example(41, [mia,smokes,slowly,'.']).
example(42, [a,man,smokes,slowly,'.']).
example(43, [every,man,smokes,slowly,'.']).
example(44, [mia,saw,a,man,slowly,'.']).
example(45, [every,woman,saw,a,man,slowly,'.']).
example(101,[smokes,mia,'.']).
example(102,[mia,saw,every,man,'.']).
/* ----------------------------------------------------------------------------------
Test
---------------------------------------------------------------------------------- */
example(Example):-
setDefaultOptions(nutcracker),
example(Example,Sentence),
retractall(chart(_,_,_,_,_)),
initChart(Sentence,0,N),
parse(1,1,N,_), !.
test(Sentence):-
setDefaultOptions(nutcracker),
retractall(chart(_,_,_,_,_)),
initChart(Sentence,0,N),
parse(1,1,N,_), !.
/* ----------------------------------------------------------------------------------
RTE
---------------------------------------------------------------------------------- */
rte(E1,E2):-
setDefaultOptions(nutcracker),
setOption(nutcracker,'--tp',vampire),
setOption(nutcracker,'--mb',paradox3),
example(E1,S1),
retractall(chart(_,_,_,_,_)),
initChart(S1,0,N1),
parse(1,1,N1,F1),
example(E2,S2),
retractall(chart(_,_,_,_,_)),
initChart(S2,0,N2),
parse(1,1,N2,F2),
inference(not(imp(F1,F2))).
/* ----------------------------------------------------------------------------------
Chart Init
---------------------------------------------------------------------------------- */
initChart([],X,X).
initChart([Token|L],X,N):-
Y is X + 1,
lex(Token,Cat,Sem),
assert(chart(X,Y,Cat,Sem,lex(Cat,Token))),
initChart(L,Y,N).
/* ----------------------------------------------------------------------------------
Parsing (CYK)
---------------------------------------------------------------------------------- */
parse(Start,K,End,FOL):-
K > End,
chart(Start,End,Cat,Sem,Der), !,
write(chart(Start,End,Cat,Sem,Der)),nl,
output(Cat,Sem,Der,FOL).
parse(M,K,L,F):-
L is M+K, !,
parse(M,L),
KInc is K+1,
parse(0,KInc,L,F).
parse(M,K,L,F):-
N is M+K,
parse(M,N),
MInc is M+1,
parse(MInc,K,L,F).
/* ----------------------------------------------------------------------------------
Output
---------------------------------------------------------------------------------- */
output(Cat,Sem,Der,FOL):-
write(cat:Cat),nl,
write(sem:Sem),nl,
reduce(Sem,Drs), !,
printDrs(user_output,Drs),
write(der:Der),nl,
drs2fol(Drs,FOL),
inference(FOL).
/* ----------------------------------------------------------------------------------
Combine
---------------------------------------------------------------------------------- */
parse(M,L):-
chart(M,X,Cat1,Sem1,Der1),
chart(X,L,Cat2,Sem2,Der2),
combine(Cat1:Sem1,Cat2:Sem2,Cat3:Sem3,Der1,Der2,Der3), !,
assert(chart(M,L,Cat3,Sem3,Der3)).
parse(_,_).
/* ----------------------------------------------------------------------------------
Inference
---------------------------------------------------------------------------------- */
inference(FOL):-
MaxDomSize=20,
A10 = all(X,all(Y,imp(member(X,Y),and(individual(X),collection(Y))))),
A11 = all(B,imp(two(B),and(some(A,firstmember(A,B)),some(A,secondmember(A,B))))),
A12 = all(B,imp(three(B),and(some(A,firstmember(A,B)),and(some(A,secondmember(A,B)),some(A,thirdmember(A,B)))))),
A13 = all(B,imp(four(B),and(some(A,firstmember(A,B)),and(some(A,secondmember(A,B)),and(some(A,thirdmember(A,B)),some(A,fourthmember(A,B))))))),
A14 = all(X,all(Y,imp(firstmember(X,Y),member(X,Y)))),
A15 = all(X,all(Y,imp(secondmember(X,Y),member(X,Y)))),
A16 = all(X,all(Y,imp(thirdmember(X,Y),member(X,Y)))),
A17 = all(X,all(Y,imp(fourthmember(X,Y),member(X,Y)))),
% A15 = all(X,imp(and(individual(X),some(Y,and(individual(Y),not(eq(X,Y))))),some(Y,and(two(Y),member(X,Y))))),
% A15 = all(X,all(Y,imp(and(individual(X),and(individual(Y),not(eq(X,Y)))),some(Z,and(two(Z),and(member(X,Z),member(Y,Z))))))),
% A16 = all(X,all(Y,imp(and(two(Y),member(X,Y)),or(firstmember(X,Y),secondmember(X,Y))))),
% A1 = and(A10,and(A11,and(A12,and(A13,and(A14,and(A15,and(A16,and(A17,and(A18,A19))))))))),
A1 = and(A10,and(A11,and(A12,and(A13,and(A14,and(A15,and(A16,A17))))))),
A21 = all(X,imp(individual(X),not(collection(X)))),
A22 = all(X,imp(individual(X),not(event(X)))),
A23 = all(X,imp(collection(X),not(event(X)))),
A24 = all(X,imp(man(X),not(woman(X)))),
A25 = all(X,imp(man(X),human(X))),
A26 = all(X,imp(woman(X),human(X))),
A27 = all(X,imp(human(X),individual(X))),
A28 = all(X,imp(smoke(X),event(X))),
A29 = all(X,imp(see(X),event(X))),
A2 = and(A21,and(A22,and(A23,and(A24,and(A25,and(A26,and(A27,and(A28,A29)))))))),
A31 = all(X,imp(two(X),collection(X))),
A32 = all(X,imp(three(X),collection(X))),
A33 = all(X,imp(four(X),collection(X))),
A3 = and(A31,and(A32,A33)),
A40 = all(X,imp(two(X),not(some(Y,and(firstmember(Y,X),secondmember(Y,X)))))),
A41 = all(X,imp(three(X),not(some(Y,and(firstmember(Y,X),thirdmember(Y,X)))))),
A42 = all(X,imp(three(X),not(some(Y,and(secondmember(Y,X),thirdmember(Y,X)))))),
A43 = all(X,imp(three(X),not(some(Y,and(firstmember(Y,X),secondmember(Y,X)))))),
A44 = all(X,imp(four(X),not(some(Y,and(firstmember(Y,X),secondmember(Y,X)))))),
A45 = all(X,imp(four(X),not(some(Y,and(firstmember(Y,X),thirdmember(Y,X)))))),
A46 = all(X,imp(four(X),not(some(Y,and(firstmember(Y,X),fourthmember(Y,X)))))),
A47 = all(X,imp(four(X),not(some(Y,and(secondmember(Y,X),thirdmember(Y,X)))))),
A48 = all(X,imp(four(X),not(some(Y,and(secondmember(Y,X),fourthmember(Y,X)))))),
A49 = all(X,imp(four(X),not(some(Y,and(thirdmember(Y,X),fourthmember(Y,X)))))),
A4 = and(A40,and(A41,and(A42,and(A43,and(A44,and(A45,and(A46,and(A47,and(A48,A49))))))))),
A51 = all(X,imp(lou(X),not(andy(X)))),
A52 = all(X,imp(lou(X),man(X))),
A53 = all(X,imp(andy(X),man(X))),
A54 = all(X,imp(mia(X),woman(X))),
A5 = and(A51,and(A52,and(A53,A54))),
A60 = all(X,imp(and(individual(X),some(Y,and(individual(Y),not(eq(Y,X))))),some(Y,and(two(Y),member(X,Y))))),
A61 = all(X,imp(and(individual(X),some(Y,and(two(Y),not(member(X,Y))))),some(Y,and(three(Y),member(X,Y))))),
A62 = all(X,imp(and(individual(X),some(Y,and(three(Y),not(member(X,Y))))),some(Y,and(four(Y),member(X,Y))))),
A63 = all(X,imp(two(X),all(Y,imp(member(Y,X),or(firstmember(Y,X),secondmember(Y,X)))))),
A64 = all(X,imp(three(X),all(Y,imp(member(Y,X),or(firstmember(Y,X),or(secondmember(Y,X),thirdmember(Y,X))))))),
A65 = all(X,imp(four(X),all(Y,imp(member(Y,X),or(firstmember(Y,X),or(secondmember(Y,X),or(thirdmember(Y,X),fourthmember(Y,X)))))))),
A66 = all(X,all(Y,imp(some(C,and(firstmember(X,C),firstmember(Y,C))),eq(X,Y)))),
A67 = all(X,all(Y,imp(some(C,and(secondmember(X,C),secondmember(Y,C))),eq(X,Y)))),
A68 = all(X,all(Y,imp(some(C,and(thirdmember(X,C),thirdmember(Y,C))),eq(X,Y)))),
A69 = all(X,all(Y,imp(some(C,and(fourthmember(X,C),fourthmember(Y,C))),eq(X,Y)))),
A6 = and(A60,and(A61,and(A62,and(A63,and(A64,and(A65,and(A66,and(A67,and(A68,A69))))))))),
BK = and(A1,and(A2,and(A3,and(A4,and(A5,A6))))),
F = and(BK,FOL),
callTPandMB([],not(F),F,1,MaxDomSize,Model,Engine),
write(engine:Engine),nl,
printModel(Model,user_output),nl.
/* ----------------------------------------------------------------------------------
POS reduction
---------------------------------------------------------------------------------- */
reduce(drs(D,Conds),Reduced):-
select(pos(drs([],C1)),Conds,C2), !,
append(C1,C2,C3),
reduce(drs(D,C3),Reduced).
reduce(drs(D,C1),drs(D,C2)):- !,
reduce(C1,C2).
reduce([],[]):- !.
reduce([pos(B1)|L1],[pos(B2)|L2]):- !,
reduce(B1,B2),
reduce(L1,L2).
reduce([imp(A1,B1)|L1],[imp(A2,B2)|L2]):- !,
reduce(A1,A2),
reduce(B1,B2),
reduce(L1,L2).
reduce([or(A1,B1)|L1],[or(A2,B2)|L2]):- !,
reduce(A1,A2),
reduce(B1,B2),
reduce(L1,L2).
reduce([C|L1],[C|L2]):- !,
reduce(L1,L2).
/* ----------------------------------------------------------------------------------
drs2fol
---------------------------------------------------------------------------------- */
drs2fol(drs([],[Cond]),Formula):- !, cond2fol(Cond,Formula).
drs2fol(drs([],[Cond1,Cond2|Conds]),and(Formula1,Formula2)):- !,
cond2fol(Cond1,Formula1), drs2fol(drs([],[Cond2|Conds]),Formula2).
drs2fol(drs([_:X|Referents],Conds),some(V,Formula)):-
ref2var(X,V),
drs2fol(drs(Referents,Conds),Formula).
/* ========================================================================
Referents to variable
=========================================================================*/
ref2var(x1,'X'):- !.
ref2var(x2,'Y'):- !.
/* ========================================================================
Translate DRS-Conditions into FOL formulas
=========================================================================*/
cond2fol(_:C,F):- !,
cond2fol(C,F).
cond2fol(not(Drs),not(Formula)):- !,
drs2fol(Drs,Formula).
cond2fol(pos(Drs),Formula):- !,
drs2fol(Drs,Formula).
cond2fol(or(Drs1,Drs2),or(Formula1,Formula2)):- !,
drs2fol(Drs1,Formula1),
drs2fol(Drs2,Formula2).
cond2fol(imp(drs(D,C),B),Formula):- !,
cond2fol(not(drs(D,[not(B)|C])),Formula).
cond2fol(named(X,N1,Type,Sense),F):-
symbol(Type,N1,Sense,N2), !,
ref2var(X,V),
F=..[N2,V].
cond2fol(eq(X,Y),eq(V1,V2)):-
ref2var(X,V1),
ref2var(Y,V2).
cond2fol(pred(X,Sym1,Type,Sense),F):-
symbol(Type,Sym1,Sense,Sym2), !,
ref2var(X,V), F=..[Sym2,V].
cond2fol(rel(X,Y,Sym1,Sense),F):-
symbol(r,Sym1,Sense,Sym2), !,
ref2var(X,V1), ref2var(Y,V2), F=..[Sym2,V1,V2].
/*========================================================================
Ensure F is a number or atom
========================================================================*/
symbol(Type,F1,0,F2):- !, symbol(Type,F1,1,F2).
symbol(_Type,F1,_Sense,F2):- F1=F2.
/* =======================================================================
Print Model
========================================================================*/
printModel(model(D,[]),Stream):- !,
format(Stream,'model(~p, [])',[D]).
printModel(model(D,[F]),Stream):- !,
format(Stream,'model(~p,~n [~p])',[D,F]).
printModel(model(D,[X,Y|F]),Stream):- !,
sort([X,Y|F],[First|Sorted]),
format(Stream,'model(~p,~n [~p,~n',[D,First]),
printModel(Sorted,Stream).
printModel([Last],Stream):- !,
format(Stream,' ~p])',[Last]).
printModel([X|L],Stream):- !,
format(Stream,' ~p,~n',[X]),
printModel(L,Stream).
printModel(Model,Stream):-
write(Stream,Model).