On the Complexity of Clause Condensing

  • Georg Gottlob
Conference paper
Part of the Informatik-Fachberichte book series (INFORMATIK, volume 287)


This paper deals with complexity issues related to the recognition of redundancy and to the removal of redundant literals from a clause. We first consider condensing, a weak type of redundancy elimination. A clause is condensed iff 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 show that the problem of testing whether a given clause is condensed is co-NP-complete. Furthermore, we prove that the problems of identifying clause condensations and of testing whether there exists a condensation of a given cardinality are complete for DP, a complexity class which is likely to properly include both NP and co-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 implies C’. We show that the problem of testing whether a clause is strongly condensed is undecidable.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    L.D. Baxter. The NP-completeness of subsumption. unpublished manuscript, 1977.Google Scholar
  2. [2]
    S. Ceri, G. Gottlob, and L. Tanca. What you always wanted to know about datalog (and never dared to ask). IEEE Transactions on Knowledge and Data Engineering, 1(1), March 1989.Google Scholar
  3. [4]
    C.L. Chang and R.C.T. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.zbMATHGoogle Scholar
  4. [5]
    W.F. Clocksin and C.S. Mellish. Programming in Prolog. Springer Berlin/Heidelberg/New York, 1981.zbMATHGoogle Scholar
  5. [6]
    M. Garey and D.S. Johnson. Computers and Intractability — A Guide to NP-Completeness. W.H.Freeman, New York, 1979.zbMATHGoogle Scholar
  6. [7]
    G. Gottlob. Subsumption and implication. Information Processing Letters, 24:109–111, January 1987.MathSciNetzbMATHCrossRefGoogle Scholar
  7. [8]
    G. Gottlob and A. Leitsch. Fast subsumption algorithms. In Proceedings of the EUROCAL 85 Conference on Computer Algebra, Lecture Notes in Computer Science. Springer Verlag, 1985.Google Scholar
  8. [9]
    G. Gottlob and A. Leitsch. On the efficiency of subsumption algorithms. Journal of the ACM, 32(2):280–295, April 1985.MathSciNetzbMATHCrossRefGoogle Scholar
  9. [10]
    H. Gallaire and J. Minker, editors. Logic and Databases. Plenum Press, New York, 1978.Google Scholar
  10. [11]
    W.H. Joyner. Automatic Theorem Proving and the Decision Problem. PhD thesis, Harvard University, May 1973.Google Scholar
  11. [12]
    W.H. Joyner. Resolution strategies as decision procedures. Journal of the ACM, 23(1):398–417, July 1976.MathSciNetzbMATHCrossRefGoogle Scholar
  12. [13]
    A. Leitsch. Implication algorithms for classes of Horn clauses, in: Informatik+Oekonomie, Berlin, 1988.Google Scholar
  13. [14]
    A. Leitsch and G. Gottlob. Deciding Horn clause implication problems by ordered semantic resolution. In F. Gardin, editor, Computational Intelligence II, Proceedings of the International Symposium, Milan, Italy, 25–27 Sept 1989. North Holland, Amsterdam, 1989.Google Scholar
  14. [15]
    J.W. Lloyd. Foundations of Logic Programming. Springer Verlag, Berlin, 1984, 1987.zbMATHCrossRefGoogle Scholar
  15. [16]
    D. Loveland. Automated Theorem Proving: A Logical Basis. North Holland, Amsterdam, 1978.zbMATHGoogle Scholar
  16. [17]
    C.H. Papadimitriou and D. Wolfe. The complexity of facets resolved. J. Comput. System Sei., 37:2–13, 1988.MathSciNetzbMATHCrossRefGoogle Scholar
  17. [18]
    C.H. Papadimitriou and M. Yannakakis. The complexity of facets (and some facets of complexity). J. Comput. System Sci., 28:244–259, 1984.MathSciNetzbMATHCrossRefGoogle Scholar
  18. [19]
    M. Schmidt-Schauss. Implication of clauses is undecidable. Theoretical Computer Science, 59:287–296, 1988.MathSciNetzbMATHCrossRefGoogle Scholar
  19. [20]
    R.B. Stillman. The concept of weak substitution in theorem proving. Journal of the ACM, 20(4):648–667, October 1973.MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Georg Gottlob
    • 1
  1. 1.Christian Doppler Laboratory for Expert Systems, Institut für InformationssystemeTechnical University of ViennaAustria

Personalised recommendations