11.2. Predicate Completion#
In Section 8.2, we presented Predicate Completion as a technique for explicitly handling negative information. A logic program is viewed as a set of predicate definitions, where the only-if parts are implicitly assumed. Below, a program is given which constructs additional clauses representing the only-if parts.
A program is represented as a list of clauses, where head and body of each clause are lists of atoms, as in the program in the previous section. The output of the Predicate Completion program is a formula in first-order Predicate Logic, which can be transformed to clausal logic by means of the aforementioned program, if desired. Definitions for different predicates are handled separately, so the first step is to partition the program into separate predicate definitions. After completing each of these definitions we add appropriate formulas for each of the undefined predicates.
complete(Program,Comp):-
separate_definitions(Program,Definitions),
complete_definitions(Definitions,CompDefs,Heads),
handle_undefined(Program,Heads,CompDefs,Comp).
separate_definitions([],[]).
separate_definitions([([Head]:-Body)|Clauses],[[([Head]:-Body)|Def]|Defs]):-
get_definition(Clauses,Head,Def,Rest),
separate_definitions(Rest,Defs).
get_definition([],_Head,[],[]).
get_definition([([H]:-B)|Clauses],Head,[([H]:-B)|Def],Rest):-
same_predicate(H,Head),
get_definition(Clauses,Head,Def,Rest).
get_definition([([H]:-B)|Clauses],Head,Def,[([H]:-B)|Rest]):-
not same_predicate(H,Head),
get_definition(Clauses,Head,Def,Rest).
Undefined predicates are those which occur in bodies of clauses without occurring in any head. The list Heads of defined predicates is obtained while completing each predicate definition. Care must be taken to avoid considering not/1 as an undefined predicate, and also to check the negated literal itself. After constructing the list of undefined literals occurring in clause bodies, each of them is transformed into a formula of the form \(\forall\texttt{X1} \ldots \forall\texttt{Xn:} \; \neg \texttt{p(X1,}\ldots\texttt{,Xn)}\):
handle_undefined(Program,Heads,CompDefs,Comp):-
findall(L,
( member((H:-B),Program), % pick a clause body
( (member(L,B),not L=not(X)) % unneg. lit.
; member(not L,B) ), % or a negated one
not member(L,Heads) ), % which is undefined
Undefs),
undef_formulas(Undefs,CompDefs,Comp).
undef_formulas([],Comp,Comp).
undef_formulas([L|Ls],Comp0,Comp):-
quantify(L,F),
undef_formulas(Ls,F & Comp0,Comp).
quantify(L,F):-
L =.. [P|As],
variablise(As,Vs,F,-NewL), % NB. negation symbol!
NewL =.. [P|Vs]. % turn arguments into variables
% add quantifiers
variablise([],[],L,L).
variablise([A|As],[V|Vs],forall(V,F),L):-
variablise(As,Vs,F,L).
The main task in Predicate Completion is the completion of each separate predicate definition. The main steps are
adding explicit unifications to the body of clauses;
adding existential quantifiers for those variables occurring in the body of a clause but not in its head;
combining the clauses into one formula, and adding universal quantifiers for the head variables.
The predicate unifications_and_quantifiers/2 takes care of the first two steps, and the third step is carried out by the predicate complete_formula/3. These predicates are relatively self-explanatory:
% complete_definitions(D,C,H) <- C is the complement of
% definitions D, and H is
% list of variablised heads
complete_definitions([Def],Comp,[Head]):-!,
complete_definition(Def,Comp,Head).
complete_definitions([Def|Defs],Comp & Comps,[H|Hs]):-
complete_definition(Def,Comp,H),
complete_definitions(Defs,Comps,Hs).
complete_definition(Definition,Comp,Head):-
unifications_and_quantifiers(Definition,F),
complete_formula(F,Comp,Head).
unifications_and_quantifiers([],[]).
unifications_and_quantifiers([Clause|Clauses],[C|Cs]):-
unifs_and_quants(Clause,C),
unifications_and_quantifiers(Clauses,Cs).
unifs_and_quants(([Head]:-Body),([NewHead]:-NewBody)):-
Head=..[Pred|Args],
explicit_unifications(Args,NewArgs,Body,TmpBody),
existential_quantifiers(TmpBody,NewArgs,NewBody),
NewHead=..[Pred|NewArgs].
% explicit_unifications(A,NA,B,NB) <- NA is list A with
% non-var. terms replaced by new
% var.s; NB is body B extended
% with explicit unifications
explicit_unifications([],[],Body,Body).
explicit_unifications([T|As],[V|NewAs],B,[V=T|NewB]):-
nonvar(T), % add explicit unification
explicit_unifications(As,NewAs,B,NewB).
explicit_unifications([Var|As],[Var|NewAs],Body,NewBody):-
var(Var), % no expl. unific. needed
explicit_unifications(Args,NewArgs,Body,NewBody).
% existential_quantifiers(B,V,NB) <- NB is conj. of lit.s
% in B, extended by ex. quant.s
% for var.s in B but not in V
existential_quantifiers(Body,HeadVars,NewBody):-
varsin(Body,BodyVars), % built-in predicate
body_form(Body,Conj), % list -> conjunction
body_quants(BodyVars,HeadVars,Conj,NewBody).
body_form([not Lit],-Lit):-!.
body_form([Lit],Lit):-!.
body_form([not Lit|List],-Lit & Conj):-!,
body_form(List,Conj).
body_form([Lit|List],Lit & Conj):-
body_form(List,Conj).
% body_quants(BV,HV,C,QC) <- QC is conj. C extended with
% existential quant.s for all
% variables in BV but not in HV
body_quants([],HeadVars,Conj,Conj).
body_quants([BVar|BVars],HeadVars,Conj,exists(BVar,F)):-
not var_element(BVar,HeadVars),
body_quants(BVars,HeadVars,Conj,F).
body_quants([BVar|BVars],HeadVars,Conj,F):-
var_element(BVar,HeadVars),
body_quants(BVars,HeadVars,Conj,F).
% complete_formula(C,F,H) <- F is disjunction of bodies
% of clauses in C, and univ.
% quantified head H
complete_formula(C,Formula,Head):-
combine_clauses(C,Head,Body),
varsin(Head,HeadVars),
head_quants(HeadVars,Head => Body,Formula).
combine_clauses([([Head]:-Body)],Head,Body):- !.
combine_clauses([([Head]:-Body)|R],Head,Body v RBody):-
combine_clauses(R,Head,RBody).
head_quants([],Formula,Formula).
head_quants([HVar|HVars],Formula,forall(HVar,F)):-
head_quants(HVars,Formula,F).
The following query illustrates the operation of the program, and shows also how it can be combined with the program for conversion to clausal form presented in the previous section.
?-P=[([bird(tweety)]:-[]),
([flies(X)]:-[bird(X),not abnormal(X)])],
complete(P,F),
transform(F,C).
F=forall(Y,-abnormal(Y)) &
forall(Z,bird(Z) => Z=tweety) &
forall(X,flies(X) => bird(X) & -abnormal(X))
C=[([]:-[abnormal(Y)]),
([Z=tweety]:-[bird(Z)]),
([bird(X)]:-[flies(X)]),
([]:-[flies(X),abnormal(X)])]