REMOVING REDUNDANCY FROM A CLAUSE

被引:34
作者
GOTTLOB, G [1 ]
FERMULLER, CG [1 ]
机构
[1] VIENNA TECH UNIV,INST COMP SPRACHEN,A-1040 VIENNA,AUSTRIA
关键词
D O I
10.1016/0004-3702(93)90069-N
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
This paper deals with the problem Of removing redundant literals from a given clause. We first consider condensing, a weak type of redundancy elimination. A clause is condensed if it does not subsume any proper subset of itself. It is often useful (and sometimes necessary) to replace a non-condensed clause C by a condensation, i.e., by a condensed subset of C which is subsumed by C. After studying the complexity of an existing clause condensing algorithm, we present a more efficient algorithm and provide arguments for the optimality of the new method. We prove that testing whether a given clause is condensed is co-NP-complete and show that several problems related to clause condensing belong to complexity classes that are, probably, slightly harder than NP. We also consider a stronger version of redundancy elimination: a clause C is strongly condensed iff it does not contain any proper subset C' such that C logically implies C'. We show that the problem of testing whether a clause is strongly condensed is undecidable.
引用
收藏
页码:263 / 289
页数:27
相关论文
共 28 条
[1]  
[Anonymous], SYMBOLIC LOGIC MECHA
[2]  
[Anonymous], 1990, SURVEYS COMPUTER SCI
[3]  
Clocksin W. F., 1981, PROGRAMMING PROLOG
[4]  
Gallaire Herve, 1978, LOGIC DATA BASES
[5]  
Garey MR., 1979, COMPUTERS INTRACTABI
[6]   ON THE EFFICIENCY OF SUBSUMPTION ALGORITHMS [J].
GOTTLOB, G ;
LEITSCH, A .
JOURNAL OF THE ACM, 1985, 32 (02) :280-295
[7]   SUBSUMPTION AND IMPLICATION [J].
GOTTLOB, G .
INFORMATION PROCESSING LETTERS, 1987, 24 (02) :109-111
[8]   NEW DEVELOPMENTS IN STRUCTURAL COMPLEXITY THEORY [J].
HARTMANIS, J .
THEORETICAL COMPUTER SCIENCE, 1990, 71 (01) :79-93
[9]  
Johnson D. S., 1990, HDB THEORETICAL COMP, VA
[10]  
JOYNER WH, 1976, J ACM, V23, P398, DOI 10.1145/321958.321960