The Completeness of Propositional Resolution
A Simple and Constructive Proof
Jean Gallier嫔妃侍寝
Department of Computer and Information Science
University of Pennsylvania
Philadelphia,PA19104,USA
jean@saul.cis.upenn.edu
September25,2006
Abstract.It is well known that the resolution method(for propositional logic)is complete. However,completeness proofs found in the literature u an argument by contradiction showing that if a t of claus is unsatisfiable,then it must have a resolution refutation.As a conquence,none of the proofs actually gives an algorithm for producing a resolution refutation from an unsatisfiable t o
f claus.In this note,we give a simple and constructive proof of the completeness of propositional resolution which consists of an algorithm together with a proof of its correctness.
1
1Introduction
The resolution method for(propositional)logic due to J.A.Robinson[4](1965)is well-known to be a sound and complete procedure for checking the unsatisfiability of a t of claus. However,it appears that the completeness proofs that can be found in the literature(for instance,Chang and Lee[1],Lewis and Papadimitriou[3],Robinson[5])are existence proofs that proceed by contradiction to show that if a t of claus is unsatisfiable,then it must have a resolution refutation becau otherwi a satisfying assignment can be obtained. In particular,none of the proofs yields(directly)an algorithm producing a resolution refutation from an unsatisfiable t of claus.In that n,the proofs are nonconstructive. In Gallier[2](1986),we gave a completeness proof bad on an algorithm for converting a Gentzen-like proof(using quents)into a resolution DAG(e Chapter4).Such a method is more constructive than the others but,we found later on that it is possible to give a simple and constructive proof of the completeness of propositional resolution whic
h consists of an algorithm together with a proof of its correctness.This algorithm and its correctness are the object of this note.
It should be noted that Judith Underwood gave other constructive proof procedures in her Ph.D.thesis,notably for the intuitionistic propositional calculus[6].
2Review of Propositional Resolution
Recall that a literal,L,is either a propositional letter,P,or the negation,¬P,of a propo-sitional letter.A clau is afinite t of literals,{L1,...,L k},interpreted as the disjunc-tion L1∨···∨L k(when k=0,this is the empty clau denoted).A t of claus,Γ={C1,...,C n},is interpreted as the conjunction C1∧···∧C n.For short,we write Γ=C1,...,C n.
The resolution method(J.A.Robinson[4])is a procedure for checking whether a t of claus,Γ,is unsatisfiable.The resolution method consists in building a certain kind of labeled DAG who leaves are labeled with claus inΓand who interior nodes are labeled according to the resolution rule.Given two claus C=A∪{P}and C =B∪{¬P}(where P is a propositional letter,P/∈A and¬P/∈B),the resolvent of C and C is the clau
R=A∪B
obtained by cancelling out P and¬P.A resolution DAG forΓis a DAG who leaves are labeled with claus fromΓand such that every interior node n has exactly two predecessors, n1and n2so that n is labeled with the resolvent of the claus labeling n1and n2.In a resolution step involving the nodes,n1,n2and n,as above,we say that the two claus C and C labeling the nodes n1and n2are the parent claus of the resolvent clau,R,labeling the node n.In a resolution DAG,D,a clau,C is said to be a descendant of a clau,C, iffthere is a(directed)path from some node labeled with C to a node labeled with C .A resolution refutation forΓis a resolution DAG with a single root who label is the empty
2
clau.(For more details on the resolution method,resolution DAGs,etc.,one may consult Gallier[2],Chapter4,or any of the books cited in Section1.)
Here is an example of a resolution refutation for the t of claus
Γ={{P,Q},{P,¬Q},{¬P,Q},{¬P,¬Q}}:
{P,Q}{P,¬Q}{¬P,Q}{¬P,¬Q}
{P}{Q}
{¬P}
3Completeness of Propositional Resolution: An Algorithm and its Correctness
LetΓbe a t of claus.Thus,Γis either the empty clau,,or it is a conjunction of claus,Γ=C1,...,C n.We define the complexity,c(C),of a clau,C,as the number of disjunction symbols in ,if C consists of a single ,C={L},for some literal, L),then c(C)=0,el if C={L1,...,L m}(with m≥2)where the L i’s are literals,then c(C)=m−1(we also t c()=0).IfΓis a conjunction of claus,Γ=C1,...,C n,then we t
c(Γ)=c(C1)+···+c(C n).
We now give a recursive algorithm,buildresol,for constructing a resolution DAG from any t of claus and then prove its correctness,namely,that if the input t of claus is unsatisfiable,then the output resolution DAG is a resolution refutation.This establishes the completeness of propositional resolution constructively.
分泌胆汁的器官Our algorithm makes u of two functions,percolate,and graft.
1.The function percolate(D,A,L)
The inputs are:a resolution DAG,D,some lected leaf of D labeled with a clau,A, and some literal,L.This function adds the literal L to the clau A to form the clau A∪{L}and then“percolates”L down to the root of D.More precily,we construct the resolution DAG,D ,who underlying unlabeled DAG is identical to D,as follows:Since D and D have the same unlabeled DAG we refer to two nodes of D of D as corresponding nodes if they are identical in the underlying unlabeled DAG.Consider any resolution step of D.If both parent claus are not descendants of the premi A,then the corresponding resolution step of D is the same.If the parent claus in D are C and C where C is a descendant of the premi A(resp.C is a descendant of the premi A)and if R is the
3
resolvent ot C and C in D,then the corresponding parent nodes in D are labeled with C and C ∪{L}and their resolvent node with R∪{L}(resp.the corresponding parent nodes in D are labeled with C∪{L}and C and their resolvent node wih R∪{L}).If both parent claus C and C in D are descendant of the premi A,then the corresponding parent nodes in D are labeled with C∪{L}and C ∪{L}and their resolvent node with R∪{L}.
极言Obrve that if∆∪{A}is the t of premis of D,thenΓ=∆∪{A∪{L}}is the t of premis of percolate(D,A,L).
For example,if D is the resolution DAG shown below(in fact,a resolution refutation)
{P,Q}{¬P,Q}A={¬Q}
{Q}
头像美女Figure1:Resolution DAG D
then adding L=¬P to A={¬Q}in D yields the resolution DAG D produced by percolate(D,A,L):
{P,Q}{¬P,Q}{¬P,¬Q}
{Q}
P}
Figure2:Resolution DAG D =percolate(D,A,L)
2.The function graft(D1,D2)
Its inputs are two resolution DAGs,D1and D2,where the clau,C,labeling the root of D1is identical to one of the premis of D2.Then,this function combines D1and D2 by connecting the links to the premi labeled C in D2to the root of D1,also labeled C, obtaining the resolution DAG graft(D1,D2).
For example,if D1and D2are the resolution refutation DAGs shown below
{P,Q}{¬P,Q}{¬P,¬Q}
{Q}
P}
Figure3:Resolution DAG D1
4
{P,Q}{P,¬Q}{¬P}
{P}
跳来跳去的女人Figure4:Resolution DAG D2
we obtain the resolution DAG
{P,Q}{P,¬Q}{¬P,Q}{¬P,¬Q}
{P}{Q}
{¬P}
Figure5:Resolution DAG graft(D1,D2)
where the edges coming from D2are indicated with thicker lines.The algorithm buildresol is shown below.
3.The algorithm buildresol(Γ)
The input to buildresol is a t of claus,Γ.
function buildresol(Γ)
begin
if all claus inΓare literals then
ifΓcontains complementary literals L and¬L,
then return a resolution refutation with leaves L and¬L
el abort
endif
el lect any nonliteral clau,C,inΓand lect any literal,L,in C;
let C=A∪{L};letΓ=∆∪{C};
D1=buildresol(∆∪{A});D2=buildresol(∆∪{L});D 1=percolate(D1,A,L);
if D 1is a resolution DAG
then return D 1
烫伤起泡了怎么办el D=graft(D 1,D2);return D
endif
endif
end
5
Finally,we prove the correctness of our recursive algorithm buildresol .
Theorem 3.1For every conjunction of claus,Γ,if Γis unsatisfiable,then the algorithm builresol outputs a resolution refutation for Γ.Therefore,propositional resolution is com-plete.
Proof .We prove the correctness of the algorithm buildresol by induction on c (Γ).Let Γ=C
调春1,...,C n .We may assume Γ=,since the ca Γ=is trivial.We proceed by induction on c (Γ).
If c (Γ)=0,then every clau,C i ,contains a single literal and if Γis unsatisfiable,then there must be two complementary claus,C i ={P }and C j ={¬P },in Γ.Thus,we instantly get a resolution refutation by applying the resolution rule to {P }and {¬P }.
Otherwi,c (Γ)>0,so there is some clau in Γthat contains at least two literals.Pick any such clau,C ,and pick any literal,L ,in C .Write C =A ∪{L }with A =and write
Γ=∆,C (∆can’t be empty since Γis unsatisfiable).As Γ=∆,A ∪{L }is unsatisfiable,both ∆,A and ∆,L must be unsatisfiable.However,obrve that
c (∆,A )<c (Γ)an
d c (∆,L )<c (Γ).
Therefore,by the induction hypothesis,the algorithm buildresol produces two resolution refutations,D 1and D 2,with ts of premis ∆,A and ∆,L ,respectively.Now,consider the
resolution DAG,D 1=percolate (D 1,A,L ),obtained from D 1by adding L to the clau A and letting L percolate down to the root.
Obrve that in D 1,every clau that is a descendant of the premi A ∪{L }is of the form C ∪{L },where C is the corresponding clau in D 1.Therefore,the root of the new
DAG D
画口罩简笔画1obtained from D 1is either labeled (this may happen when the other clau in a resolution step involving a descendent of the clau A already contains L )or L .In the first ca,D 1is already a resolution refutation for Γand we are done.In the cond ca,we can combine D 1and D 2using graft (D 1,D 2)since the root of D 1is also labeled L ,one of the premis of D
2.Clearly,we obtain a resolution refutation for Γ.
As an illustration of our algorithm,consider the t of claus
Γ={{P,Q },{P,¬Q },{¬P,Q },{¬P,¬Q }}
as above and pick C ={¬P,¬Q },L =¬P and A ={¬Q }.After the two calls
buildresol (∆∪{A })and buildresol (∆∪{L }),we get the resolution refutations D 1:
{P,Q }{¬P,Q }
{¬Q }
{Q }Figure 6:Resolution DAG D 1=buildresol (∆∪{A })
6
