Abstract
We consider a proof procedure aiming at refuting clause sets containing arithmetic constants (or parameters), interpreted as natural numbers. The superposition calculus is enriched with a loop detection rule encoding a form of mathematical induction on the natural numbers (by “descente infinie”). This calculus and its theoretical properties are described in [2,16]. In the present paper, we focus on more practical aspects. We provide algorithms to apply the loop detection rule in an automatic and efficient way. We describe a research prototype implementing our technique and provide some preliminary experimental results.
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
References
Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 84–99. Springer, Heidelberg (2009)
Aravantinos, V., Echenim, M., Peltier, N.: A resolution calculus for first-order schemata. Fundamenta Informaticae (accepted for publication, to appear, 2013)
Baaz, M., Leitsch, A.: Towards a clausal analysis of cut-elimination. J. Symb. Comput. 41(3-4), 381–410 (2006)
Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierachic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193–212 (1994)
Barthe, G., Stratulat, S.: Validation of the javacard platform with implicit induction techniques. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 337–351. Springer, Heidelberg (2003)
Baumgartner, P., Tinelli, C.: Model Evolution with Equality Modulo Built-in Theories. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 85–100. Springer, Heidelberg (2011)
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)
Comon, H.: Inductionless induction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 14, pp. 913–962. North-Holland (2001)
Dunchev, T.: Automation of cut-elimination in proof schemata. PhD thesis, T.U. Vienna (2012)
Dunchev, T., Leitsch, A., Rukhaia, M., Weller, D.: Ceres for first-order schemata, Research Report (2013), http://arxiv.org/abs/1303.4257
Falke, S., Kapur, D.: Rewriting induction + linear arithmetic = decision procedure. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 241–255. Springer, Heidelberg (2012)
Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306–320. Springer, Heidelberg (2009)
Giesl, J., Kapur, D.: Decidable classes of inductive theorems. In: Goré, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 469–484. Springer, Heidelberg (2001)
Giesl, J., Kapur, D.: Deciding inductive validity of equations. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 17–31. Springer, Heidelberg (2003)
Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Trans. Comput. Logic 11(4), 1–35 (2010)
Kersani, A., Peltier, N.: Completeness and Decidability Results for First-Order Clauses with Indices. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 58–75. Springer, Heidelberg (2013)
McCune, W.: Prover9 and mace4 (2005–2010), http://www.cs.unm.edu/~mccune/prover9/
Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. North-Holland (2001)
Rukhaia, M.: CERES in Proof Schemata. PhD thesis, T.U. Vienna (2012)
Stratulat, S.: Automatic ‘Descente infinie’ induction reasoning. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol. 3702, pp. 262–276. Springer, Heidelberg (2005)
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). Combining Superposition and Induction: A Practical Realization. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds) Frontiers of Combining Systems. FroCoS 2013. Lecture Notes in Computer Science(), vol 8152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40885-4_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-40885-4_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40884-7
Online ISBN: 978-3-642-40885-4
eBook Packages: Computer ScienceComputer Science (R0)