Advertisement

System Description: GrAnDe 1.0

  • Stephan Schulz
  • Geoff Sutcliffe
Conference paper
  • 273 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2392)

Abstract

The validity problem for full first-order logic is only semi-decidable. However, there are many interesting problems that, when expressed in clause normal form, have a finite Herbrand universe. They fall into a decidable subclass of first-order logic. Traditionally, such problems have been tackled using conventional first-order techniques. Some implementations, e.g. DCTP [SL01], are decision procedures for this class of problems. An alternative approach, justified by Herbrand’s theorem, is to generate the ground instances of such a problem and use a propositional decision system to determine the satisfiability of the resulting propositional problem. The applicability of the grounding approach has led to these problems being called “effectively propositional” (EPR) problems. The TPTP problem library [SS98] v2.4.1 contains 574 EPR problems. Many of these are group theory problems (101 problems) and CNF translations of formulae in propositional multi-modal logic (206 problems).

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [DIM]
  2. [HS01]
    H. Hoos and T. Stützle. SATLIB: An Online Resource for Research on SAT. In I. Gent, H. van Maaren, and T. Walsh, editors, Proc. of the 3rd Workshop on the Satisfiability Problem, 2001. http://www.satlib.org/.
  3. [LP92]
    S-J. Lee and D.A. Plaisted. Eliminating Duplication with the Hyper-Linking Strategy. Journal of Automated Reasoning, 9(1):25–42, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [MMZ+01]
    M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In D. Blaauw and L. Lavagno, editors, Proc. of the 39th Design Automation Conference, pages 530–535, 2001.Google Scholar
  5. [PZ00]
    D.A. Plaisted and Y. Zhu. Ordered Semantic Hyper-linking. Journal of Automated Reasoning, 25(3):167–217, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  6. [RV99]
    A. Riazanov and A. Voronkov. Vampire. In H. Ganzinger, editor, Proc. of the 16th International Conference on Automated Deduction, number 1632 in Lecture Notes in Artificial Intelligence, pages 292–296. Springer, 1999.Google Scholar
  7. [RV01]
    A. Riazanov and A. Voronkov. Splitting without Backtracking. In B. Nebel, editor, Proc. of the 17th International Joint Conference on Artificial Intelligence, pages 611–617. Morgan Kaufmann, 2001.Google Scholar
  8. [Sch02]
    S. Schulz. A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae. In S. Haller and G. Simmons, editors, Proc. of the 15th Florida Artificial Intelligence Research Symposium. AAAI Press, 2002. To appear.Google Scholar
  9. [SL01]
    G. Stenz and R. Letz. DCTP-A Disconnection Calculus Theorem Prover. In R. Gore, A. Leitsch, and T. Nipkow, editors, Proc. of the International Joint Conference on Automated Reasoning, number 2083 in Lecture Notes in Artificial Intelligence, pages 381–385. Springer, 2001.Google Scholar
  10. [SS98]
    G. Sutcliffe and C.B. Suttner. The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning, 21(2):177–203, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  11. [SSP02]
    G. Sutcliffe, C. Suttner, and J. Pelletier. The IJCAR ATP System Competition. Journal of Automated Reasoning, To appear, 2002.Google Scholar
  12. [Sut01]
    G. Sutcliffe. CASC-JC. http://www.cs.miami.edu/ tptp/CASC/JC/, 2001.
  13. [Wei99]
    C. Weidenbach, et al. SPASS Version 1.0.0. In H. Ganzinger, editor, Proc. of the 16th International Conference on Automated Deduction, number 1632 in Lecture Notes in Artificial Intelligence, pages 378–382. Springer, 1999.Google Scholar
  14. [ZS00]
    H. Zhang and M. Stickel. Implementing the Davis-Putnam Method. Journal of Automated Reasoning, 24(1/2):277–296, 2000.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Stephan Schulz
    • 1
  • Geoff Sutcliffe
    • 2
  1. 1.Institut für InformatikTechnische Universität MünchenGermany
  2. 2.Department of Computer ScienceUniversity of MiamiUSA

Personalised recommendations