Journal of Computer Science and Technology

, Volume 15, Issue 5, pp 409–415 | Cite as

Renaming a set of non-Horn clauses

  • Nie Xumin Email author
  • Guo Qing 


Several extensions of the logic programming language Prolog to non-Horn clauses use case anlaysis to handle non-Horn clauses. In this paper, analytical and empirical evidences are presented to show that, by making a set of clauses less “non-Horn” using predicate renaming, the performance- of these case-analysis based procedures can be improved significantly. In addition, the paper also investigated the problem of efficiently constructing a predicate renaming that reduces the degree of “non-Hornness” of a clause set maximally. It is shown that this problem of finding a predicate renaming to achieve minimal “non-Hornness” is NP-complete.


logic for artificial intelligence (AI) automated theorem proving logic programming Horn and non-Horn sets predicate renaming NP-completeness 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Clocksin W F, Mellish C S. Programming in Prolog. Springer-Verlag, 1981.Google Scholar
  2. [2]
    Lloyd J W. Foundations of Logic Programming. Springer-Verlag, 1987.Google Scholar
  3. [3]
    Kowalski R A. Predicate logic as a programming language. InInformation Processing 74, Jack Rosenfeld (ed.), North-Holland, 1974, pp.569–574.Google Scholar
  4. [4]
    Baumgartner P, Furbach U. Model elimination without contrapositives and its application to PTTP.Journal of Automated Reasoning, 1994, 13(3): 339–359.CrossRefMathSciNetGoogle Scholar
  5. [5]
    Loveland D W. A simplified format for the model elimination theorem-proving procedure.Journal of ACM, 1969, 16(3): 349–363.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [6]
    Loveland D W. Near-Horn Prolog and beyond.Journal of Automated Reasoning, 1991, 7(1): 1–26.zbMATHCrossRefMathSciNetGoogle Scholar
  7. [7]
    Plaisted D A. A simplified problem reduction format.Artificial Intelligence, 1982, 18: 227–261.zbMATHCrossRefMathSciNetGoogle Scholar
  8. [8]
    Plaisted D A. Non-Horn clause logic programming without contrapositives.Journal of Automated Reasoning, 1988, 4(3): 287–325.zbMATHCrossRefMathSciNetGoogle Scholar
  9. [9]
    Reed D W, Loveland D W. Near-Horn Prolog and the ancestry family of procedures.Annals of Mathematics and Artificial Intelligence, 1995, 14.Google Scholar
  10. [10]
    Nie X. Complexities of non-Horn clause logic programming. InMethodologies for Intelligent Systems 5, Ras Z, Zemankova M, Emrich M (eds.), 1990, p.539–544.Google Scholar
  11. [11]
    Nie X. How well are non-Horn clauses handled. InLecture Notes in Computer Science 542, Ras Z, Zemankova M (eds.), Springer-Verlag, 1991, pp.580–588.Google Scholar
  12. [12]
    Nie X. A note on non-Horn clause logic programming.Artificial Intelligence, 1997, 92: 243–258.zbMATHCrossRefMathSciNetGoogle Scholar
  13. [13]
    Reed D W, Loveland D W. A comparison of three Prolog extensions.Journal of Logic Programming, 1992, 12: 25–50.zbMATHCrossRefMathSciNetGoogle Scholar
  14. [14]
    Mitchell D, Selman B, Levesque H. Hard and easy distributions of SAT problems. InProceeding of AAAI-92, San Jose, CA, July 12–16, 1992, pp.459–465.Google Scholar
  15. [15]
    Lewis H R. Renaming a set of clauses as a Horn set.Journal of ACM, 1978, 25(1): 134–135.zbMATHCrossRefGoogle Scholar
  16. [16]
    Mannila H, Mehlhorn K. A fast algorithm for renaming a set of clauses as a Horn set.Information Processing Letter, 1985, 21(5): 269–272.CrossRefGoogle Scholar
  17. [17]
    Garey M R, Johnson D S. Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman Company, 1979.Google Scholar
  18. [18]
    Henschen L, Wos L. Unit refutations and Horn sets.Journal of ACM, 1974, 21(4): 590–605.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 2000

Authors and Affiliations

  1. 1.Department of Computer ScienceWichita State UniversityWichitaUSA
  2. 2.Department of Computer ScienceState University of New York at AlbanyAlbanyUSA

Personalised recommendations