Abstract
We present in this paper a narrowing-based proof search method for inductive theorems. It has the specificity to be grounded on deduction modulo and to yield a direct translation from a successful proof search derivation to a proof in the sequent calculus. The method is shown to be sound and refutationally correct in a proof theoretical way.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press (1998)
Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure Patterns Type Systems. In: Principles of Programming Languages (POPL 2003), ACM, New Orleans (2003)
Berregeb, N., Bouhoula, A., Rusinowitch, M.: SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 428–431. Springer, Heidelberg (1996)
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., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press (2005)
Comon, H., Nieuwenhuis, R.: Induction=i-axiomatization+first-order consistency. Inf. Comput. 159(1-2), 151–186 (2000)
Deplagne, E.: Système de preuve modulo récurrence. Thèse de doctorat, Université Nancy 1 (November 2002)
Deplagne, E., Kirchner, C.: Induction as deduction modulo. Research report A04-R-468, LORIA (November 2004)
Deplagne, E., Kirchner, C., Kirchner, H., Nguyen, Q.-H.: Proof Search and Proof Check for Equational and Inductive Theorems. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol. 2741, pp. 297–316. Springer, Heidelberg (2003)
Dershowitz, N., Plaisted, D.A.: Rewriting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 9, pp. 535–610. Elsevier Science (2001)
Dowek, G.: La part du Calcul. Université de Paris 7, Mémoire d’habilitation (1999)
Dowek, G., Hardin, T., Kirchner, C.: HOL-λσ an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science 11(1), 21–45 (2001)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)
Ferreira, M.: Termination of Term Rewriting: Well foundedness, Totality and Transformations. PhD thesis, Utrecht University (1995)
Ganzinger, H., Stuber, J.: Inductive theorem proving by consistency for first-order clauses. In: Rusinowitch, M., Remy, J.-L. (eds.) CTRS 1992. LNCS, vol. 656, pp. 226–241. Springer, Heidelberg (1992); Published in 1993
Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press (1989)
Huet, G.: Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University (1972)
Hullot, J.-M.: Canonical Forms and Unification. In: Bibel, W., Kowalski, R. (eds.) Proceedings 5th International Conference on Automated Deduction. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)
Kapur, D., Zhang, H.: An overview of rewrite rule laboratory (RRL). J. Computer and Mathematics with Applications 29(2), 91–114 (1995)
Kirchner, C., Kirchner, H.: Rewriting, solving, proving. A preliminary version of a book (1999), http://www.loria.fr/~ckirchne/rsp.ps.gz
Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue d’Intelligence Artificielle 4(3), 9–52 (1990); Special issue on Automatic Deduction
Musser, D.: On proving inductive properties of abstract data types. In: Proceedings, Symposium on Principles of Programming Languages, vol. 7, Association for Computing Machinery (1980)
Nahon, F.: Preuve par induction dans le calcul des séquents modulo. PhD thesis, Université Henri Poincaré - Nancy I, Nancy, France, October 26 (2007)
Nahon, F., Kirchner, C., Kirchner, H., Brauner, P.: Inductive Proof Search Modulo. Annals of Mathematics and Artificial Intelligence 55(1-2), 123–154 (2009)
Steel, G.: Proof by consistency - a literature survey (March 1999)
Wack, B.: Typage et déduction dans le calcul de réécriture. Thèse de doctorat, Université Henri Poincaré - Nancy I, October 7 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Kirchner, C., Kirchner, H., Nahon, F. (2013). Narrowing Based Inductive Proof Search. In: Voronkov, A., Weidenbach, C. (eds) Programming Logics. Lecture Notes in Computer Science, vol 7797. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37651-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-37651-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37650-4
Online ISBN: 978-3-642-37651-1
eBook Packages: Computer ScienceComputer Science (R0)