Translating English Sentences Into Logic Formulae


KEY
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 by satisfying the goal
            | ?- sentence(P,[every,man,that,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(300,xfx,:).

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].