Abstract
We define a proof procedure that allows for a limited form of inductive reasoning. The first argument of a function symbol is allowed to belong to an inductive type. We will call such an argument an index. We enhance the standard superposition calculus with a loop detection rule, in order to encode a particular form of mathematical induction. The satisfiability problem is not semi-decidable, but some classes of clause sets are identified for which the proposed procedure is complete and/or terminating.
This work has been partly funded by the project ASAP of the French Agence Nationale de la Recherche (ANR-09-BLAN-0407-01).
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Aravantinos, V., Caferra, R., Peltier, N.: Decidability and undecidability results for propositional schemata. Journal of Artificial Intelligence Research 40, 599–656 (2011)
Aravantinos, V., Caferra, R., Peltier, N.: Linear Temporal Logic and Propositional Schemata, Back and Forth. In: TIME 2011 (18th International Symposium on Temporal Representation and Reasoning) (2011)
Aravantinos, V., Echenim, M., Peltier, N.: A resolution calculus for first-order schemata. In: Fundamenta Informaticae (to appear 2013) (accepted for publication)
Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation 183(2), 140–164 (2003)
Baaz, M., Hetzl, S., Leitsch, A., Richter, C., Spohr, H.: CERES: An analysis of Fürstenberg’s proof of the infinity of primes. Theor. Comput. Sci. 403(2-3), 160–175 (2008)
Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 3(4), 217–247 (1994)
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierachic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)
Baelde, D., Miller, D., Snow, Z.: Focused inductive theorem proving. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 278–292. Springer, Heidelberg (2010)
Bouhoula, A., Kounalis, E., Rusinowitch, M.: SPIKE, an automatic theorem prover. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 460–462. Springer, Heidelberg (1992)
Bundy, A.: The automation of proof by mathematical induction. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 845–911. Elsevier and MIT Press (2001)
Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: meta-level guidance for mathematical reasoning. Cambridge University Press, New York (2005)
Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 14, pp. 913–962. North-Holland (2001)
Comon, H., Lescanne, P.: Equational problems and disunification. Journal of Symbolic Computation 7, 371–475 (1989)
Gupta, A., Fisher, A.L.: Parametric circuit representation using inductive boolean functions. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 15–28. Springer, Heidelberg (1993)
Horbach, M., Weidenbach, C.: Deciding the inductive validity of ∀ ∃ * queries. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 332–347. Springer, Heidelberg (2009)
Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Trans. Comput. Logic 11(4), 1–35 (2010)
Kapur, D., Musser, D.: Proof by consistency. Artificial Intelligence 31 (1987)
Kersani, A., Peltier, N.: Completeness and Decidability Results for First-order Clauses with Indices (long version), Research Report (2013), http://membres-lig.imag.fr/peltier/kp13.pdf
Leitsch, A.: Deciding clause classes by semantic clash resolution. Fundamenta Informaticae 18, 163–182 (1993)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371–443. Elsevier and MIT Press (2001)
Peltier, N.: Some Techniques for Proving Termination of the Hyperresolution Calculus. Journal of Automated Reasoning 35, 391–427 (2006)
Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. North-Holland (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kersani, A., Peltier, N. (2013). Completeness and Decidability Results for First-Order Clauses with Indices. In: Bonacina, M.P. (eds) Automated Deduction – CADE-24. CADE 2013. Lecture Notes in Computer Science(), vol 7898. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38574-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-38574-2_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38573-5
Online ISBN: 978-3-642-38574-2
eBook Packages: Computer ScienceComputer Science (R0)