:- op(500,xfy,&). 
:- op(510,xfy,=>). 
:- op(100,fx,`).

s(S) --> np(VP^S), vp(VP).

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)^all(X,(S1=>S2)) ).
det( a,     (X^S1)^(X^S2)^exists(X,S1&S2) ).

n( program, X^program(X) ).
n( student, X^student(X) ).

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

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

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