Translating English Sentences into Logic Formulae

The following example of a definite clause grammar defines in a formal way the traditional mapping of simple English sentences into formulae of classical logic. By way of illustration, if the sentence

Every man that lives loves a woman.

is parsed as a sentence by the call

     | ?- phrase(sentence(P), [every,man,that,lives,loves,a,woman]).
     

then P will get instantiated to

     all(X):(man(X)&lives(X) => exists(Y):(woman(Y)&loves(X,Y)))
     

where :, & and => are infix operators defined by

     :- op(900, xfx, =>).
     :- op(800, xfy, &).
     :- op(550, xfy, :). /* predefined */
     

The grammar follows:

     sentence(P) --> noun_phrase(X, P1, P), verb_phrase(X, P1).
     
     noun_phrase(X, P1, P) -->
             determiner(X, P2, P1, P), noun(X, P3), rel_clause(X, P3, P2).
     noun_phrase(X, P, P) --> name(X).
     
     verb_phrase(X, P) --> trans_verb(X, Y, P1), noun_phrase(Y, P1, P).
     verb_phrase(X, P) --> intrans_verb(X, P).
     
     rel_clause(X, P1, P1&P2) --> [that], verb_phrase(X, P2).
     rel_clause(_, P, P) --> [].
     
     determiner(X, P1, P2, all(X):(P1=>P2)) --> [every].
     determiner(X, P1, P2, exists(X):(P1&P2)) --> [a].
     
     noun(X, man(X)) --> [man].
     noun(X, woman(X)) --> [woman].
     
     name(john) --> [john].
     
     trans_verb(X, Y, loves(X,Y)) --> [loves].
     intrans_verb(X, lives(X)) --> [lives].