Normal Forms -- 6.3

6.3 Convert first-order logic expressions to normal form

This section of Logic Topics presents a Prolog program that translates well-formed formulas (wff's) of first-order logic into so-called normal program clauses. The next section of Logic Topics presents a Prolog-like meta-interpreter (in XSB Prolog) for normal programs.

Wffs

The well-formed formulas will be Prolog terms formed according to the following recursive characterization. Each of the following kinds of terms in the left column of the table are wffs, provided that W, A, and B are also wffs.

`any predicate term p(...)`	atomic formula	"simple" statements
`~W`	negation	not
`A /\ B`	conjunction	and
`A \/ B`	disjunction	or
`A xor B`	exclusive disjunction	or...but not both
`A => B`	implication	if...then...
`A <=> B`	equivalence	...if, and only if...,
`all(X,W)`	universal quantification	every, each...
`exists(X,W)`	existential quantification	some...

Table 1

and provided that variable X (in the last two expressions) does not occur in W inside an expression of the form all(X,---) or exists(X,---).

Here are some logical English expressions and corresponding wffs. There is, of course, not a uniquely determined wff corresponding to every natural language sentence. The author has chosen symbolic expression for the nouns, verbs, etc., and provided an "intuitive" translation to a wff. These translations might not be sufficiently detailed for purposes of inference in larger contexts of meaning. The numbering of the examples will be for later reference.

1. Every room has a door.

all(R,room(R) => exists(D, door(D) /\ has(R,D))).

2. Nobody has a dollar.

all(P, person(P) => ~exists(D, dollar(D) /\ has(P,D))).

3. Bill goes to the party if either Jane or Sandra goes, but not if they both go.

goes(jane) xor goes(sandra) => goes(bill).

4. Somebody has a car.

exists(P, exists(C, person(P) /\ car(C) /\ has(P,C)).

5. Not everyone has a car.

~all(P,person(P) => exists(C, car(C) /\ has(P,C)).

6. Someone does not have a car

exists(P, person(P) /\ all(C, car(C) => ~has(P,C))).

7. If it rains tuesday then I will wear rain gear or carry my ubrella, but not both.

rains_tuesday => wear_rain_gear xor carry_umbrella.

8. Either Sam and Bill or else Sally and Nancy will go.

( go(sam) /\ go(bill) ) \/ ( go(sally) /\ go(nancy) ).

9. Sam will go, either Bill or Sally will go, and also Nancy will go.

go(sam) /\ ( go(bill) \/ go(sally) ) /\ go(nancy).

10. Some courses have two midterms

exists(C, course(C) /\ exists(MT1, midterm(C,MT1) /\ exists(MT2, midterm(C,MT2) /\ different(MT1,MT2)))).

11. Some courses have no midterms.

exists(C, course(C) /\ ~exists(MT, midterm(C,MT)).

Some things to notice about the examples.

Care has been taken to use different variables for different quantifications (e.g., 1,2,4,5,6,10,11).
Logical variable are capitalized, as for Prolog variables.
Proper names have been translated as Prolog constants in lower case.
Parentheses sometimes make wffs easier to read, although logical operator precedence would produce the same grouping (e.g. 8).
Sometimes parenthese are needed to override operator precedence (e.g., 9).

Here are the Prolog logical operator declarations:

:- op(300,fx,'~').
:- op(400,yfx,'/\').
:- op(500,yfx,'\/').
:- op(600,xfx,'=>').
:- op(650,xfx,'<=>').
:- op(350,xfx,'xor').

For example, note that

a \/ b \/ c means a \/ (b \/ c)
a /\ b \/ c means (a /\ b) \/ c
a => b <=> c means (a => b) <=> c
a => b => c is meaningless -- need parens

according to the op rules. Notice again that bigger Prolog op-precedence means that the operator has less power to grab surrounding terms. Most of this relative precendece ordering is standard in logic and programming. When in doubt, use parentheses.

Normal clauses

Recall that a Prolog clause can be characterized as having the form

A :- B1, B2, ... Bn .

where A and each Bi is a Prolog predicate expression and where n >= 0. When n = 0 the convention is to write the Prolog clause in the simplified "fact" form

A .

For example, for n = 2, A = mother(X,Y), B1 = parent(X,Y), B2 = female(X), the clause would be

mother(X,Y) :- parent(X,Y), female(X).

Normal clauses have a more generalized form than Prolog clauses, but we use a notation which is in many ways quite similar to the Prolog clause notation. A normal clause has one of the following forms

A1 | A2 | ... | Am :- B1, B2, ... Bn .

where each Ai and each Bj are positive predicate terms and where m,n >= 0, but not both m = 0 and n = 0. A positive predicate term is one like p(X,Y), whereas the predicate expression ~p(X,Y) is considered as negative. When m= 0 (and consequently n >= 1) the convention will be to write the normal clause in the "denial" form

false :- B1, B2, ... Bn .

where false is a special reserved term that can only occur in this special context. When n = 0 (and consequently m >= 1) the convention will be to write the normal clause in the "state" form

A1 | A2 | ... | Am .

The "denial" form is intended to say that B1, B2, ..., Bn cannot all be true together. The "state" form is intended to say that at least one of A1, A2, ..., Am is true.

As with Prolog clauses, a normal clause has a head (to left of ':-') and a body (to the right of ':-'). The special falsehead is equivalent to an empty clause head.

Wff to Normal clause converter

Every wff can be convert to a "semi-equivalent" collection of normal clauses. The terminolgy "semi-equivalent" will be explained later. First, let us look at the normal clauses produced by the Prolog converter for the eleven examples given above. The converter program will be discussed later in this section.

Wff	Normal Clauses
`1` `all(R,room(R) => exists(D, door(D) /\ has(R,D))).`	`has(G1204, sk9(G1204)) :- room(G1204).` `door(sk9(G1204)) :- room(G1204).`
`2` `all(P, person(P) => ~exists(D, dollar(D) /\ has(P,D))).`	`false :- person(G1276), dollar(G1284), has(G1276, G1284).`
`3` `goes(jane) xor goes(sandra) => goes(bill).`	`goes(jane) \| goes(bill) :- goes(sandra).` `goes(sandra) \| goes(bill) :- goes(jane).`
`4` `exists(P, exists(C, person(P) /\ car(C) /\ has(P,C)).`	`person(sk10).` `car(sk11).` `has(sk10, sk11).`
`5` `~all(P,person(P) => exists(C, car(C) /\ has(P,C)).`	`person(sk12).` `false :- car(G3188), has(sk12, G3188).`
`6` `exists(P, person(P) /\ all(C, car(C) => ~has(P,C))).`	`person(sk17).` `false :- car(G1236), has(sk17, G1236).`
`7` `rains_tuesday => wear_rain_gear xor carry_umbrella.`	`wear_rain_gear \| carry_umbrella :- rains_tuesday.` `false :- rains_tuesday, wear_rain_gear, carry_umbrella.`
`8` `(go(sam) /\ go(bill)) \/ (go(sally) /\ go(nancy)).`	`go(sam) \| go(sally).` `go(sam) \| go(nancy).` `go(bill) \| go(sally).` `go(bill) \| go(nancy).`
`9` `go(sam) /\ ( go(bill) \/ go(sally) ) /\ go(nancy).`	`go(sam).` `go(bill) \| go(sally).` `go(nancy).`
`10` `exists(C, course(C) /\ exists(MT1, midterm(C,MT1) /\ exists(MT2, midterm(C,MT2) /\ different(MT1,MT2)))).`	`course(sk18).` `midterm(sk18, sk19).` `midterm(sk18, sk20).` `different(sk19, sk20).`
`11` `exists(C, course(C) /\ ~exists(MT, midterm(C,MT)).`	`course(sk21).` `false :- midterm(sk21, G3428).`

Table 2

In the first example, Every room has a door,

all(R,room(R) => exists(D, door(D) /\ has(R,D))).

the conversion algorithm uses a so-called Skolem function to posit the existence of a door which may be dependent upon the room ...

has(G1204, sk9(G1204)) :- room(G1204).
door(sk9(G1204)) :- room(G1204).

Skolem functions are automatically generated by the conversion program.

In the fourth example, Somebody has a car,

exists(P, exists(C, person(P) /\ car(C) /\ has(P,C)).

the conversion uses a Skolem constants to posit the existence of the someone who has a car, and for the car.

person(sk10).
car(sk11).
has(sk10, sk11).

In the second example, Nobody has a dollar, the conversion produces a normal clause with empty or false head.

false :- person(G1276), dollar(G1284), has(G1276, G1284).

Examples 5, 6 and 11 also produce a normal clause with false head.

The conversion algorithm is part of the folklore of symbolic logic. The algorithm can be described in terms of certain subprocedures which successively transform the original input wff into new forms, ultimately producing the collection of normal clauses.

Step 1. Move negation inward

Step 2. Eliminate Quantifiers

From outside to inside,

drop universal quantifiers, remembering the variable in a list

drop existential quantifiers by substuting a Skolem function made to be dependent upon the current list of universal variables

Step 3. Eliminate xor, =>, <=> in favor of ~, /\ and \/

Step 4. Distribute \/ over /\ to produce CNF (conjunctive normal form).

Step 5. Translate CNF to normal program clauses.

The Prolog program combines Steps 1, 2 , and 3 recursively:

  %%----- drive negation inward --------------
conVert(~(~X),Uvars,Y) :-             %% double negation
   !,
   conVert(X,Uvars,Y).
conVert(~(X /\ Y),Uvars,A) :-         %% De Morgan
   !,
   conVert((~X \/ ~Y), Uvars,A).
conVert(~(X \/ Y),Uvars,A) :-         %% De Morgan
   !,
   conVert((~X /\ ~Y),Uvars,A).
conVert(~(X => Y),Uvars,A) :- 
   !,
   conVert((X /\ ~Y),Uvars,A).
conVert(~(X <=> Y),Uvars,A) :- 
   !,
   conVert((X /\ ~Y) \/ (~X /\ Y),Uvars,A).
conVert(~exists(X,P),Uvars,A) :- 
   !,
   conVert(all(X,~P),Uvars,A).
conVert(~all(X,P),Uvars,A) :- 
   !,
   conVert(exists(X,~P),Uvars,A).
conVert(~(X xor Y),Uvars,A) :-
   !,
   conVert((X /\ Y) \/ (~X /\ ~Y), Uvars, A).
  %%----- quantifiers -----------------------
conVert(all(X,P),Uvars,Q) :-
   !,
   not occurs(X,Uvars),       %% MUST use separate variables
   conVert(P,[X|Uvars],Q).
conVert(exists(X,P),Uvars,Q) :-
   !,
   not occurs(X,Uvars),       %% MUST use separate variables
   genskolem(SK),
   X=..[SK|Uvars],
   conVert(P,Uvars,Q). 
  %%----- connectives ------------------------
conVert((X <=> Y),Uvars,(A /\ B)) :-
   !,
   conVert((X -> Y),Uvars,A),
   conVert((Y -> X),Uvars,B).
conVert((X => Y),Uvars,Q) :-
   !,
   conVert((~X \/ Y),Uvars,Q).
conVert((X /\ Y),Uvars,(A /\ B)) :-
   !,
   conVert(X,Uvars,A),
   conVert(Y,Uvars,B).
conVert((X \/ Y),Uvars,(A \/ B)) :-
   !,
   conVert(X,Uvars,A),
   conVert(Y,Uvars,B).
conVert((X xor Y),Uvars,(A \/ B) /\ (~A \/ ~B)) :-
   !,
   conVert(X,Uvars,A),
   conVert(Y,Uvars,B).
  %%----- logically atomic --------------------
conVert(X,_,X).

Step 4 is performed as follows ...

%%----- distribute --------------------------
distriBute((X /\ Y) \/ Z, 
            (X \/ Z) /\ (Y \/ Z),true) :- !.
distriBute(X \/ (Y /\ Z),
             (X \/ Y) /\ (X \/ Z),true) :- !.
distriBute(X,X,fail).


%%----- conjunctive normal form --------------
cnF((X /\ Y),(A /\ B)) :-
   !,
   cnF(X,A),
   cnF(Y,B).
cnF((X \/ Y),G) :-
   !,
   cnF(X,A),
   cnF(Y,B),
   distriBute((A \/ B),F,Flag),
   (Flag -> cnF(F,G)  %% More work may be needed


             ;
            G = F ).
cnF(X,X).

For example,

?- distriBute((a /\ d) \/ (b /\ c), F, V).
V = true
F = (a \/ b /\ c) /\ (d \/ b /\ c)
Yes

(What is the implied grouping of the two inner expressions? See the operator declarations up near the top of this section.) But F is not the CNF, whereas

?- cnF((a /\ d) \/ (b /\ c), CNF).
CNF = (a \/ b) /\ (a \/ c) /\ (d \/ b) /\ (d \/ c)
Yes

finishes the "distribution" producing the CNF.

Here is a another sample, combining Steps 1-4:

?- conVert(all(X, p(X) \/ q(X) -> exists(Y, r(X,Y))),[],F),
   cnf(F, CNF).
CNF = (~ p(G1944) \/ r(G1944, sk14(G1944))) /\ (~ q(G1944) \/ r(G1944, sk14(G1944)))
F = ~ p(G1944) /\ ~ q(G1944, sk14(G1944))
Y = sk14(G1944)
X = G1944
Yes

Note that the CNF consists of two disjunctive expressions

~ p(G1944) \/ r(G1944, sk14(G1944))
~ q(G1944) \/ r(G1944, sk14(G1944))

In general the disjunctive expressions in the CNF can be arranged so that each has the form

~Q1 \/ ~Q2 \/ ... \/ ~Qh \/ P1 \/ P2 \/ ... \/ Pk

where the Qi and the Pj are positive, h >= 0 , k >= 0 but not both 0. Such a disjunctive expression is rewritten to form the following normal program clause

Q1 | Q2 | ... | Qh :- P1, P2, ..., Pk

However, if h = 0 then the rewrite produces

false :- P1, P2, ..., Pk

and if k = 0 then the rewrite produces

Q1 | Q2 | ... | Qh .

Here is the Prolog code that translates the CNF to normal program clauses:

%%----- normalize(+Wff,-NormalClauses) ------
normalize(Wff,NormalClauses) :- 
   conVert(Wff,[],S),
   cnF(S,T),
   flatten_and(T,U),
   make_clauses(U,NormalClauses).

%%-----  make a sequence out of a conjunction -----
flatten_and(X /\ Y, F) :-
   !,
   flatten_and(X,A),
   flatten_and(Y, B),
   sequence_append(A,B,F).
flatten_and(X,X).

%%-----  make a sequence out of a disjunction -----
flatten_or(X \/ Y, F) :-
   !,
   flatten_or(X,A),
   flatten_or(Y,B),
   sequence_append(A,B,F).
flatten_or(X,X).


%%----- append two sequences -------------------------------
sequence_append((X,R),S,(X,T)) :- !, sequence_append(R,S,T).
sequence_append((X),S,(X,S)).

%%----- separate into positive and negative literals -----------
separate((A,B),P,N) :- 
   !,
   (A = ~X -> N=[X|N1],
               separate(B,P,N1)
             ;
               P=[A|P1],
               separate(B,P1,N) ).
separate(A,P,N) :-
   (A = ~X -> N=[X],
               P = []
            ;
               P=[A],
               N = [] ).

%%----- tautology ----------------------------
tautology(P,N) :- some_occurs(N,P).

some_occurs([F|R],B) :-
   occurs(F,B) | some_occurs(R,B).

occurs(A,[F|_]) :-
   A == F,
   !.
occurs(A,[_|R]) :-
   occurs(A,R).

make_clauses((A,B),C) :-
   !,
   flatten_or(A,F),
   separate(F,P,N),
   (tautology(P,N) -> 
      make_clauses(B,C)
          ;
      make_clause(P,N,D),
      C = [D|R],
      make_clauses(B,R) ).
make_clauses(A,C) :-
   flatten_or(A,F),
   separate(F,P,N),
   (tautology(P,N) ->
       C = []
        ;
       make_clause(P,N,D),
       C = [D] ).

make_clause([],N, false :- B) :-
   !,
   make_sequence(N,B,',').
make_clause(P,[],H) :-
   !,
   make_sequence(P,H,'|').
make_clause(P,N, H :- T) :-
   make_sequence(P,H,'|'),
   make_sequence(N,T,',').

make_sequence([A],A,_) :- !.
make_sequence([F|R],(F|S),'|') :-
   make_sequence(R,S,'|').
make_sequence([F|R],(F,S),',') :-
   make_sequence(R,S,',').

write_list([F|R]) :- 
   write(F), write('.'), nl,
   write_list(R).
write_list([]).

For example,

?- normalize(all(X,p(X) \/ q(X) => exists(Y,r(X,Y))), N).
N = [(r(G1584, sk1(G1584)) :- p(G1584)),(r(G1584,sk1(G1584)) :- q(G1584))]
Y = sk1(G1584)
X = G1584

The normalizer does check to see if a normal clause is a tautology, and if so it excludes that normal clause. For example,

?- normalize(p \/ ~p,N).
N = []
Yes

However, the normalizer does not do some other desireable things, such as factor. For example,

?- normalize(p \/ p,N).
N = [(p '|' p)]
Yes

Exercise 1. Add factoring to the normalize program. That is, eliminate multiple factors (repeated literals) in the head or in the body of a clause.

Exercise 2. Modify the normalize program so that it will read in a file of Wffs and produce a file of normal program clauses. Make sure that if the file of Wffs contains an ill-formed input then no output file is produced but that your program reports about the error.

Exercise 3. As it is, the normalize program does not check to see that the input Wff does not contain true or false. These should not be allowed. Modifiy the normalize program so that it will not accept Wffs that contain true or false.

XSB Prolog Code for this section.
SWI Prolog Code for this section.
{The two files are almost identical - except lines 25,26,69,73.}
Prolog Tutorial Contents