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

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

n(LF) --> [N], {n(N, LF)}.
n(program, X^program(X)).
n(student, X^student(X)).

pn(E) --> [PN], {pn(PN, E)}.
pn(terry, terry).
pn(shrdlu, shrdlu).

tv(LF) --> [TV], {tv(TV, LF)}.
tv(wrote, X^Y^wrote(X, Y)).

iv(LF) --> [IV], {iv(IV, LF)}.
iv(halts, X^halts(X)).