A New Clausal Class Decidable by Hyperresolution

  • Lilia Georgieva
  • Ullrich Hustadt
  • Renate A. Schmidt
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)


In this paper we define a new clausal class, called \( \mathcal{B}\mathcal{U} \), which can be decided by hyperresolution with splitting. We also consider the model generation problem for \( \mathcal{B}\mathcal{U} \) and show that hyperresolution plus splitting can also be used as a Herbrand model generation procedure for \( \mathcal{B}\mathcal{U} \) and, furthermore, that the addition of a local minimality test allows us to generate only minimal Herbrand models for clause sets in \( \mathcal{B}\mathcal{U} \). In addition, we investigate the relationship of \( \mathcal{B}\mathcal{U} \) to other solvable classes.


Modal Logic Description Logic Predicate Symbol Direct Successor Unit Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    H. Andréka, J. van Benthem, and I. Németi. Back and forth between modal logic and classical logic. Bull. IGPL, 3(5):685–720, 1995.zbMATHCrossRefGoogle Scholar
  2. 2.
    C. Aravindan and P. Baumgartner. Theorem proving techniques for view deletion in databases. J. Symbolic Computat., 29(2):119–147, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    M. Baaz, U. Egly, and A. Leitsch. Normal form transformations. In Handbook of Automated Reasoning, pp. 273–333. Elsevier, 2001.Google Scholar
  4. 4.
    L. Bachmair and H. Ganzinger. Resolution theorem proving. In Handbook of Automated Reasoning, pp. 19–99. Elsevier, 2001.Google Scholar
  5. 5.
    L. Bachmair, H. Ganzinger, and U. Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In Proc. KGC’93, vol. 713 of LNCS, pp. 83–96. Springer, 1993.Google Scholar
  6. 6.
    P. Baumgartner, P. Fröhlich, U. Furbach, and W. Nejdl. Semantically guided theorem proving for diagnosis applications. In Proc. IJCAI’97, pp. 460–465. Morgan Kaufmann, 1997.Google Scholar
  7. 7.
    P. Baumgartner, J. Horton, and B. Spencer. Merge path improvements for minimal model hyper tableaux. In Proc. TABLEAUX’99, vol. 1617 of LNAI. Springer, 1999.Google Scholar
  8. 8.
    F. Bry and A. Yahya. Positive unit hyperresolution tableaux for minimal model generation. J. Automated Reasoning, 25(1):35–82, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    H. de Nivelle. Translation of S4 into GF and 2VAR. Manuscript, 1999.Google Scholar
  10. 10.
    H. de Nivelle, R. A. Schmidt, and U. Hustadt. Resolution-based methods for modal logics. Logic J. IGPL, 8(3):265–292, 2000.zbMATHCrossRefGoogle Scholar
  11. 11.
    C. G. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet. Resolution decision procedures. In Handbook of Automated Reasoning, pp. 1791–1849. Elsevier, 2001.Google Scholar
  12. 12.
    H. Ganzinger and H. de Nivelle. A superposition decision procedure for the guarded fragment with equality. In Proc. LICS’99, pp. 295–303. IEEE Computer Society Press, 1999.Google Scholar
  13. 13.
    L. Georgieva, U. Hustadt, and R. A. Schmidt. Hyperresolution for guarded formulae. To appear in J. Symbolic Computat. Google Scholar
  14. 14.
    L. Georgieva, U. Hustadt, and R. A. Schmidt. Computational space efficiency and minimal model generation for guarded formulae. In Proc. LPAR 2001, vol. 2250 of LNAI, pp. 85–99. Springer, 2001.Google Scholar
  15. 15.
    E. Grädel. On the restraining power of guards. J. Symbolic Logic, 64:1719–1742, 1999.zbMATHCrossRefMathSciNetGoogle Scholar
  16. 16.
    U. Hustadt and R. A. Schmidt. Maslov’s class K revisited. In Proc. CADE-16, vol. 1632 of LNAI, pp. 172–186. Springer, 1999.Google Scholar
  17. 17.
    U. Hustadt and R. A. Schmidt. Issues of decidability for description logics in the framework of resolution. In Automated Deduction in Classical and Non-Classical Logics, vol. 1761 of LNAI, pp. 191–205. Springer, 2000.Google Scholar
  18. 18.
    U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. In SAT 2000: Highlights of Satisfiability Research in the Year 2000, pp. 459–483. IOS Press, Amsterdam, 2000.Google Scholar
  19. 19.
    A. Leitsch. Deciding clause classes by semantic clash resolution. Fundamenta Informaticae, 18:163–182, 1993.zbMATHMathSciNetGoogle Scholar
  20. 20.
    C. Lutz. Complexity of terminological reasoning revisited. In Proc. LPAR’99, vol. 1705 of LNAI, pp. 181–200. Springer, 1999.Google Scholar
  21. 21.
    C. Lutz, U. Sattler, and S. Tobies. A suggestion of an n-ary description logic. In Proc. DL’99, pp. 81–85. Linköping University, 1999.Google Scholar
  22. 22.
    I. Niemelä. A tableau calculus for minimal model reasoning. In Proc. TABLEAUX’96, vol. 1071 of LNAI, pp. 278–294. Springer, 1996.Google Scholar
  23. 23.
    R. A. Schmidt and U. Hustadt. A resolution decision procedure for fluted logic. In Proc. CADE-17, vol. 1831 of LNAI, pp. 433–448. Springer, 2000.Google Scholar
  24. 24.
    M. Schmidt-Schauβ and G. Smolka. Attributive concept descriptions with complements. J. Artificial Intelligence, 48:1–26, 1991.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Lilia Georgieva
    • 1
    • 2
  • Ullrich Hustadt
    • 3
  • Renate A. Schmidt
    • 1
    • 2
  1. 1.Department of Computer ScienceUniversity of ManchesterUK
  2. 2.Max-Planck-Institut für InformatikSaarbrückenGermany
  3. 3.Department of Computer ScienceUniversity of LiverpoolUK

Personalised recommendations