11.1. From Predicate Logic to clausal logic#
In Section 2.5 we discussed a method for transforming a formula in Predicate Logic to an ‘almost’ equivalent set of clauses (reread this section if you don’t recall in what sense the clauses differ from the Predicate Logic formula). Below, a Prolog program implementing this method is given.
The logical symbols used in Predicate Logic formulas are defined as operators:
% logical symbols used in Predicate Logic formulas
:-op(900,xfx,'=>'). % implication
:-op(800,xfy,&). % conjunction
:-op(800,xfy,v). % disjunction
:-op(400,fy,-). % negation
In addition, a universally quantified formula of the form \(\forall \; \texttt{X:F}\) is represented by the term forall(X,F). For instance, the formula
is represented by
forall(S,student_of(peter)=>likes(peter,S)).
Likewise, an existentially quantified formula of the form \(\exists \; \texttt{X:F}\) is represented by the term exists(X,F).
The transformation from Predicate Logic to clausal logic requires six steps:
replace implications by disjunction and negation;
push negations inside, so that each of them immediately precedes a literal;
move quantifiers to the front (the result is said to be in prenex normal form);
replace existentially quantified variables by Skolem functors;
rewrite into conjunctive normal form, i.e. a conjunction of disjunctions of literals;
rewrite each conjunct to a clause.
The main predicate transform/2 carries out these six steps:
transform(Formula,Clauses):-
rewrite_implications(Formula,F1),
negations_inside(F1,F2),
prenex_normal_form(F2,F3),
skolemise(F3,F4),
conjunctive_normal_form(F4,F5),
clausal_form(F5,Clauses).
Predicates for each of these steps are defined below.
The first two predicates contain one clause for each possible form a formula could have.
% rewrite_implications(F1,F2) <- F2 is a PL formula
% without implications,
% log. equivalent with F1
rewrite_implications(A,A):- % base case
literal(A).
rewrite_implications(A => B, -C v D):- % implication
rewrite_implications(A,C),
rewrite_implications(B,D).
rewrite_implications(A & B, C & D):- % no change;
rewrite_implications(A,C), % try rest of
rewrite_implications(B,D). % formula
rewrite_implications(A v B, C v D):-
rewrite_implications(A,C),
rewrite_implications(B,D).
rewrite_implications(-A,-C):-
rewrite_implications(A,C).
rewrite_implications(forall(X,B), forall(X,D)):-
rewrite_implications(B,D).
rewrite_implications(exists(X,B), exists(X,D)):-
rewrite_implications(B,D).
% negations_inside(F1,F2) <- F2 is a PL formula with
% negs. only preceding literals
% log. equivalent with F1
negations_inside(A,A):- % base case
literal(A).
negations_inside(-(A & B), C v D):- % De Morgan (1)
negations_inside(-A,C),
negations_inside(-B,D).
negations_inside(-(A v B), C & D):- % De Morgan (2)
negations_inside(-A,C),
negations_inside(-B,D).
negations_inside(-(-A),B):- % double negation
negations_inside(A,B).
negations_inside(-exists(X,A),forall(X,B)):- % quantifiers
negations_inside(-A,B).
negations_inside(-forall(X,A),exists(X,B)):-
negations_inside(-A,B).
negations_inside(A & B, C & D):- % no change;
negations_inside(A,C), % try rest of
negations_inside(B,D). % formula
negations_inside(A v B, C v D):-
negations_inside(A,C),
negations_inside(B,D).
negations_inside(exists(X,A),exists(X,B)):-
negations_inside(A,B).
negations_inside(forall(X,A),forall(X,B)):-
negations_inside(A,B).
In step 3, the quantifiers found at different positions in the formula are moved to the front, preserving their order. This is achieved by means of an auxiliary predicate pnf/4, which separates the quantifiers from the rest of the formula (referred to below as the Body). An additional argument V acts as a pointer to the place of the body in the quantifier structure. For instance, the query
?-pnf(forall(X,p(X,X)) & forall(Y,exists(Z,p(Y,Z))),Q,V,B)
has the following answers:
Q = forall(X,forall(Y,exists(Z,V)))
B = p(X,X)&p(Y,Z)
Unifying V with B gives the required formula in prenex normal form:
% prenex_normal_form(F1,F2) <- F2 is a PL formula
% with all quant.s in front,
% log. equivalent with F1
prenex_normal_form(F,PNF):-
pnf(F,PNF,B,B).
pnf(A,V,V,A):- % base case
literal(A).
pnf(forall(X,F),forall(X,Quants),V,Body):-
pnf(F,Quants,V,Body).
pnf(exists(X,F),exists(X,Quants),V,Body):-
pnf(F,Quants,V,Body).
pnf(A & B,Quants,V,BodyA & BodyB):-
pnf(A,Quants,QB,BodyA),
pnf(B,QB,V,BodyB).
pnf(A v B,Quants,V,BodyA v BodyB):-
pnf(A,Quants,QB,BodyA),
pnf(B,QB,V,BodyB).
Step 4 is called Skolemisation. It involves introducing a Skolem functor for each existentially quantified variable. The Skolem functors are named sk1, sk2, etc. The arguments of the Skolem functors are given by the universally quantified variables found before the existentially quantified one. Since all remaining variables are universally quantified, the universal quantifiers can be dropped. (Strictly speaking, the formula is now neither in Predicate Logic form, nor in clausal form.)
% skolemise(F1,F2) <- F2 is obtained from F1 by replacing
% all existentially quantified
% variables by Skolem terms
skolemise(F1,F2):-
skolemise(F1,[],1,F2).
skolemise(forall(X,F1),VarList,N,F2):-!, % remove univ.
skolemise(F1,[X|VarList],N,F2). % quantifier
skolemise(exists(X,F1),VarList,N,F2):-!,
skolem_term(X,VarList,N), % unify with
N1 is N+1, % Skolem term
skolemise(F1,VarList,N1,F2).
skolemise(F,V,N,F). % copy rest of formula
skolem_term(X,VarList,N):-
C is N+48, % number -> character
name(Functor,[115,107,C]), % Skolem functor skN
X =.. [Functor|VarList].
We now have a formula containing only conjunction, disjunction and positive and negative literals. Such a formula can uniquely be rewritten to a conjunction of disjunctions of literals, by distributing disjunction over conjunction. The result is said to be in conjunctive normal form (CNF):
conjunctive_normal_form(A,A):- % base case
disjunction_of_literals(A),!.
conjunctive_normal_form((A & B) v C, D & E ):-!,
conjunctive_normal_form(A v C,D), % distribution
conjunctive_normal_form(B v C,E).
conjunctive_normal_form(A v (B & C), D & E ):- !,
conjunctive_normal_form(A v B,D), % distribution
conjunctive_normal_form(A v C,E).
conjunctive_normal_form(A & B,C & D):- % conjuction
conjunctive_normal_form(A,C),
conjunctive_normal_form(B,D).
conjunctive_normal_form(A v B,E):- % other cases
conjunctive_normal_form(A,C),
conjunctive_normal_form(B,D),
conjunctive_normal_form(C v D,E).
Finally, the CNF-formula is rewritten to a list of clauses. For simplicity, body and head of each clause are represented by lists:
clausal_form(A,[Clause]):-
disjunction_of_literals(A),
make_clause(A,Clause).
clausal_form(A & B,Clauses):-
clausal_form(A,ClausesA),
clausal_form(B,ClausesB),
append(ClausesA,ClausesB,Clauses).
make_clause(P,([P]:-[])):-
logical_atom(P).
make_clause(-N,([]:-[N])):-
logical_atom(N).
make_clause(A v B,(HeadAB:-BodyAB)):-
make_clause(A,(HeadA:-BodyA)),
make_clause(B,(HeadB:-BodyB)),
append(HeadA,HeadB,HeadAB),
append(BodyA,BodyB,BodyAB).
The program is completed by a number of simple utility predicates:
disjunction_of_literals(A):-
literal(A).
disjunction_of_literals(C v D):-
disjunction_of_literals(C),
disjunction_of_literals(D).
literal(A):-
logical_atom(A).
literal(-A):-
logical_atom(A).
logical_atom(A):-
functor(A,P,N),
not logical_symbol(P).
logical_symbol(=>).
logical_symbol(<=>).
logical_symbol(-).
logical_symbol(&).
logical_symbol(v).
logical_symbol(exists).
logical_symbol(forall).