:- op(500,xfy,&). 
:- op(510,xfy,=>). 
:- op(100,fx,`).
s(T) --> np(VP^S), vp(VP), {pull(S, T)}.

np(NP) --> 
   det(N2^NP), n(N1), optrel(N1^N2).
np((E^S)^S) --> pn(E).

vp(X^S) --> tv(X^IV), np(IV^S).
vp(IV) --> iv(IV).

optrel((X^S1)^(X^(S1 & S2))) --> [that], vp(X^S2).
optrel(N^N) --> [].

det(LF) --> [D], {det(D, LF)}.
n(LF)   --> [N], {n(N, LF)}.
pn(E) --> [PN], {pn(PN, E)}.
iv(LF) --> [IV], {iv(IV, LF)}.
tv(LF) --> [TV], {tv(TV, LF)}.

det( every, (X^S1)^(X^S2)^q(P^Q^all(X,P=>Q),S1,S2) ).
det( a,     (X^S1)^(X^S2)^q(P^Q^exists(X,P&Q),S1,S2) ).

n( book,      X^(`book(X))      ).
n( professor, X^(`professor(X)) ).
n( program,   X^(`program(X))   ).
n( student,   X^(`student(X))   ).

pn( terry,  terry  ).
pn( shrdlu, shrdlu ).

tv( ran,   X^Y^(`ran(X,Y))   ).
tv( wrote, X^Y^(`wrote(X,Y)) ).

iv( halts, X^(`halts(X)) ).