A Resolution Calculus for First-order Schemata

• Autorzy: Aravantinos V. , Echenim M. , Peltier N.
• Języki publikacji: EN

Abstrakty

EN

We devise a resolution calculus that tests the satisfiability of infinite families of clause sets, called clause set schemata. For schemata of propositional clause sets, we prove that this calculus is sound, refutationally complete, and terminating. The calculus is extended to first-order clauses, for which termination is lost, since the satisfiability problem is not semi-decidable for nonpropositional schemata. The expressive power of the considered logic is strictly greater than the one considered in our previous work.

Słowa kluczowe

EN

first-order logic; propositional logic; resolution calculus; schemata

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 125, nr 2
• Strony: 101--133
• Opis fizyczny: Bibliogr. 22 poz., wykr.

Twórcy

autor

Aravantinos V.

• LIG/CNRS, Grenoble, France

autor

Echenim M.

• LIG/Grenoble INP-Ensimag, France

autor

Peltier N.

• LIG/CNRS, Grenoble, France

Bibliografia

• [1] Althaus, E., Kruglov, E., Weidenbach, C.: Superposition Modulo Linear Arithmetic SUP(LA), FroCoS 2009 (S. Ghilardi, R. Sebastiani, Eds.), 5749, Springer, 2009.
• [2] Aravantinos, V., Caferra, R., Peltier, N.: A DPLL Proof Procedure for Propositional Iterated Schemata, Workshop “Structures and Deduction 2009" (ESSLI), 2009.
• [3] Aravantinos, V., Caferra, R., Peltier, N.: A Schemata Calculus For Propositional Logic, TABLEAUX 09 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), 5607, Springer, 2009.
• [4] Aravantinos, V., Caferra, R., Peltier, N.: A Decidable Class of Nested Iterated Schemata, IJCAR 2010 (International Joint Conference on Automated Reasoning), LNCS, Springer, 2010.
• [5] Aravantinos, V., Caferra, R., Peltier, N.: RegSTAB: a SAT-Solver for Propositional Schemata, IJCAR 2010 (International Joint Conference on Automated Reasoning), LNCS, Springer, 2010.
• [6] Aravantinos, V., Caferra, R., Peltier, N.: Decidability and Undecidability Results for Propositional Schemata, Journal of Artificial Intelligence Research, 40, 2011, 599-656.
• [7] Aravantinos, V., Peltier, N.: Schemata of SMT problems, TABLEAUX 11 (International Conference on Automated Reasoning with Analytic Tableaux and Related Methods), LNCS, Springer, 2011.
• [8] Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: An analysis of Furstenberg’s proof of the infinity of primes, Theor. Comput. Sci., 403(2-3), 2008, 160-175.
• [9] Bachmair, L., Ganzinger, H.: Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, 3(4), 1994, 217-247.
• [10] Bachmair, L., Ganzinger, H.: Resolution Theorem Proving, in: Handbook of Automated Reasoning (J. A. Robinson, A. Voronkov, Eds.), Elsevier and MIT Press, 2001, 19-99.
• [11] Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational Theorem Proving for Hierachic First-Order Theories, Appl. Algebra Eng. Commun. Comput., 5, 1994, 193-212.
• [12] Comon, H., Lescanne, P.: Equational Problems and Disunification, Journal of Symbolic Computation, 7, 1989, 371-475.
• [13] Cooper, D.: Theorem Proving in Arithmetic without Multiplication, in: Machine Intelligence 7 (B. Meltzer, D. Michie, Eds.), chapter 5, Edinburgh University Press, 1972, 91-99.
• [14] Fermuller, C., Leitsch, A., Tammet, T., Zamov, N.: Resolution Methods for the Decision Problem, LNAI 679, Springer, 1993.
• [15] Gupta, A., Fisher, A. L.: Parametric Circuit Representation Using Inductive Boolean Functions, CAV (C. Courcoubetis, Ed.), 697, Springer, 1993, ISBN 3-540-56922-7.
• [16] Horbach, M., Weidenbach, C.: Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries, CSL (E. Gradel, R. Kahle, Eds.), 5771, Springer, 2009, ISBN 978-3-642-04026-9.
• [17] Horbach, M., Weidenbach, C.: Superposition for fixed domains, ACM Trans. Comput. Logic, 11(4), 2010, 1-35, ISSN 1529-3785.
• [18] Korovin, K., Voronkov, A.: Integrating Linear Arithmetic into Superposition Calculus, CSL 2007 (J. Duparc, T. A. Henzinger, Eds.), 4646, Springer, 2007.
• [19] Leitsch, A.: The resolution calculus, Springer. Texts in Theoretical Computer Science, 1997.
• [20] Presburger, M.: Uber die Vollstandigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchen die Addition als einzige Operation hervortritt, Comptes Rendus du I congrśs de Mathśmaticiens des Pays Slaves, 1929.
• [21] Robinson, J. A.: A machine-oriented logic based on the resolution principle, J. Assoc. Comput. Mach., 12, 1965, 23-41.
• [22] Waldmann, U.: Superposition and Chaining for Totally Ordered Divisible Abelian Groups, IJCAR, 2001.