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

\[ \forall \; \texttt{S: student_of(S,peter)} \rightarrow \texttt{likes(peter,S)} \]

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

Simply Logical

From Predicate Logic to clausal logic

11.1. From Predicate Logic to clausal logic#