System Description: GrAnDe 1.0
- 273 Downloads
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).
Unable to display preview. Download preview PDF.
- [DIM]DIMACS. Satisfiability Suggested Format. ftp://dimacs.rutgers.edu/ pub/challenge/satisfiability/doc/satformat.tex.
- [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/.
- [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
- [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
- [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
- [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
- [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
- [SSP02]G. Sutcliffe, C. Suttner, and J. Pelletier. The IJCAR ATP System Competition. Journal of Automated Reasoning, To appear, 2002.Google Scholar
- [Sut01]G. Sutcliffe. CASC-JC. http://www.cs.miami.edu/ tptp/CASC/JC/, 2001.
- [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