(apx:b.1)= # From Predicate Logic to clausal logic # In {numref}`sec: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: ```Prolog % 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 ```Prolog 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: 1. replace implications by disjunction and negation; 1. push negations inside, so that each of them immediately precedes a literal; 1. move quantifiers to the front (the result is said to be in *prenex normal form*); 1. replace existentially quantified variables by Skolem functors; 1. rewrite into *conjunctive normal form*, i.e. a conjunction of disjunctions of literals; 1. rewrite each conjunct to a clause. The main predicate `transform/2` carries out these six steps: ```{swish} swish:transform --- source-text-end: transform-end build-file: true --- ``` Predicates for each of these steps are defined below. +++ The first two predicates contain one clause for each possible form a formula could have. ```Prolog % 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 ```Prolog ?-pnf(forall(X,p(X,X)) & forall(Y,exists(Z,p(Y,Z))),Q,V,B) ``` has the following answers: ```Prolog 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: ```Prolog % 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.) ```Prolog % 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): ```Prolog 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: ```Prolog 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: ```Prolog 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). ```