Constructing Decision Procedures in Equational Clausal Logic

• Autorzy: Peltier N.
• Języki publikacji: EN

Abstrakty

EN

A method is proposed to construct decision procedures for various subclasses of first-order logic with equality. We define a notion of complexity of first-order terms and equations, and we propose semantic and syntactic criteria ensuring that existing refinements of the paramodulation calculus terminate on the considered clause sets. These refinements use reduction orderings, selection functions and simplification rules. Since they are sound and refutationally complete, the corresponding classes of formulae are decidable. Moreover, the automatic extraction of models from saturated clause sets is also possible. A discussion and detailed comparisons with existing works in the field are provided, together with numerous examples and some undecidability results.

Słowa kluczowe

EN

first-order logic; equational clausal logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 54, nr 1
• Strony: 17--65
• Opis fizyczny: bibliogr. 33 poz.

Twórcy

autor

Peltier N.

• LEIBNIZ - IMAG, 46 avenue Félix Viallet, 38031 Grenoble Cedex, France,

Bibliografia

• [1] L. Bachmair and H. Ganzinger. Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation, 3(4):217-247, 1994.
• [2] L. Bachmair, H. Ganzinger, and U. Waldmann. Superposition with simplification as a decision procedure for the monadic class with equality. In Computational Logic and Proof Theory, KGC 93, pages 83-96. Springer, LNCS 713, 1993.
• [3] E. Börger, E. Gr¨adel, and Y. Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997.
• [4] B. Dreben and W. D. Goldfarb. The Decision Problem, Solvable Classes of Quantificational Formulas. Addison-Wesley, 1979.
• [5] C. Fermüller and A. Leitsch. Decision procedures and model building in equational clause logic. Journal of the IGPL, 6(1):17-41, 1998.
• [6] C. Fermüller, A. Leitsch, U. Hustadt, and T. Tammet. Resolution decision procedures. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, chapter 25, pages 1791-1850. Elsevier, 2001.
• [7] C. Fermüller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Methods for the Decision Problem. LNAI 679. Springer, 1993.
• [8] C. G. Fermüller. Deciding Some Horn Clause Sets by Resolution. In Yearbook of the Kurt Gödel Society, pages 60-73, 1990.
• [9] M. Fitting. First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer-Verlag, 1990.
• [10] H. Ganzinger and H. d. Nivelle. A superposition decision procedure for the guarded fragment with equality. In Proc. 14th IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, 1999.
• [11] L. Georgieva, U. Hustadt, and R. A. Schmidt. Hyperresolution for guarded formulae. In P. Baumgartner and H. Zhang, editors, Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000), volume 5/2000 of Fachberichte Informatik, pages 101-112, Koblenz, Germany, 2000. Institut für Informatik, Universit¨at Koblenz-Landau.
• [12] J. Hsiang and M. Rusinowitch. A new method for establishing refutational completeness in theorem proving. In Proceeding of CADE’86, pages 141-152, 1986.
• [13] J. Hsiang and M. Rusinowitch. Proving refutational completeness of theorem proving strategies: The transfinite semantic tree method. Journal of the ACM, 38(3):559-587, July 1991.
• [14] U. Hustadt and R. A. Schmidt. Maslov’s class K revisited. In H. Ganzinger, editor, Automated Deduction—CADE-16, volume 1632 of Lecture Notes in Artificial Intelligence, pages 172-186. Springer, 1999.
• [15] U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. Journal of Automated Reasoning, 28(2):205-232, Feb. 2002.
• [16] J. Jouannaud and C. Kirchner. Solving equations in abstract algebras: a rule based survey of unification. In J.-L. Lassez and G. Plotkin, editors, Essays in Honor of Alan Robinson, pages 91-99. The MIT-Press, 1991.
• [17] W. Joyner. Resolution strategies as decision procedures. Journal of the ACM, 23:398-417, 1976.
• [18] D. Knuth and P. Bendix. Simple word problems in universal algebra. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263-297. Pergamon Press, 1970.
• [19] T. Langholm. A Strong Version of Herbrand’s Theorem for Introvert Sentences. Journal of Symbolic Logic, 63:555-569, 1998.
• [20] A. Leitsch. Deciding clause classes by semantic clash resolution. Fundamenta Informaticae, 18:163-182, 1993.
• [21] D. W. Loveland. Automated Theorem Proving: A Logical Basis, volume 6 of Fundamental Studies in Computer Science. North Holland, 1978.
• [22] R. Manthey and F. Bry. SATCHMO: A theorem prover implemented in Prolog. In Proc. of CADE-9, pages 415-434. Springer, LNCS 310, 1988.
• [23] W. McCune. A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical report, Argonne National Laboratory, 1994.
• [24] H. d. Nivelle. A resolution decision procedure for the guarded fragment. In Automated Deduction - CADE-15, volume 1421 of LNCS, 1998.
• [25] N. Peltier. On the decidability of the PVD class with equality. Logic Journal of the IGPL, 9(4):601-624, 2001. N. Peltier / Constructing Decision Procedures 65
• [26] M. Presburger. ¨Uber die vollst¨andigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt. In Comptes Rendus du I congres de Mathématiciens des Pays Slaves, pages 92-101, 1929.
• [27] J. Robinson. Automatic deduction with hyperresolution. Intern. Journal of Computer Math., 1:227-234, 1965.
• [28] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach., 12:23-41, 1965.
• [29] T. Rudlof. SHR tableaux - A Framework for Automated Model Generation. Journal of Logic and Computation, 10(6):107-155, 2000.
• [30] M. Rusinowitch. D´emonstration automatique par des techniques de réécriture. Th`ese déetat 1987, Nancy 1-France. Also available as textbook (Inter Editions, Paris 1989), 1987.
• [31] R. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 24(4):529-543, 1977.
• [32] R. Shostak. An algorithm for reasoning about equality. Communications of the Association for Computing Machine, 2:583-585, 1978.
• [33] J. R. Slagle. Automatic theorem proving with renamable and semantic resolution. Journal of the ACM, 14(4):687-697, October 1967.