×

zbMATH — the first resource for mathematics

Narrowing based inductive proof search. (English) Zbl 1383.03019
Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 216-238 (2013).
Summary: 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.
For the entire collection see [Zbl 1259.03008].

MSC:
03B35 Mechanization of proofs and logical operations
68Q42 Grammars and rewriting systems
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
RRL; SPIKE
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press (1998) · Zbl 0948.68098 · doi:10.1017/CBO9781139172752
[2] Barthe, G., Cirstea, H., Kirchner, C., Liquori, L.: Pure Patterns Type Systems. In: Principles of Programming Languages (POPL 2003), ACM, New Orleans (2003) · Zbl 1321.68137
[3] 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) · doi:10.1007/3-540-61464-8_73
[4] 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) · doi:10.1007/BFb0013087
[5] Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: Meta-Level Guidance for Mathematical Reasoning. Cambridge University Press (2005) · Zbl 1095.68108 · doi:10.1017/CBO9780511543326
[6] Comon, H., Nieuwenhuis, R.: Induction=i-axiomatization+first-order consistency. Inf. Comput. 159(1-2), 151–186 (2000) · Zbl 1046.68640 · doi:10.1006/inco.2000.2875
[7] Deplagne, E.: Système de preuve modulo récurrence. Thèse de doctorat, Université Nancy 1 (November 2002)
[8] Deplagne, E., Kirchner, C.: Induction as deduction modulo. Research report A04-R-468, LORIA (November 2004) · Zbl 1072.68569
[9] 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) · Zbl 1278.68257 · doi:10.1007/978-3-540-45085-6_26
[10] 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) · Zbl 0992.68123 · doi:10.1016/B978-044450813-3/50011-4
[11] Dowek, G.: La part du Calcul. Université de Paris 7, Mémoire d’habilitation (1999)
[12] Dowek, G., Hardin, T., Kirchner, C.: HOL-\(\lambda\)\(\sigma\) an intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science 11(1), 21–45 (2001) · Zbl 0972.03012 · doi:10.1017/S0960129500003236
[13] Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003) · Zbl 1049.03011 · doi:10.1023/A:1027357912519
[14] Ferreira, M.: Termination of Term Rewriting: Well foundedness, Totality and Transformations. PhD thesis, Utrecht University (1995)
[15] 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 · doi:10.1007/3-540-56393-8_17
[16] Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Cambridge Tracts in Theoretical Computer Science, vol. 7. Cambridge University Press (1989) · Zbl 0671.68002
[17] Huet, G.: Constrained Resolution: A Complete Method for Higher Order Logic. PhD thesis, Case Western Reserve University (1972)
[18] 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)
[19] Kapur, D., Zhang, H.: An overview of rewrite rule laboratory (RRL). J. Computer and Mathematics with Applications 29(2), 91–114 (1995) · Zbl 00718813 · doi:10.1016/0898-1221(94)00218-A
[20] Kirchner, C., Kirchner, H.: Rewriting, solving, proving. A preliminary version of a book (1999), http://www.loria.fr/ ckirchne/rsp.ps.gz · Zbl 0955.74027
[21] Kirchner, C., Kirchner, H., Rusinowitch, M.: Deduction with symbolic constraints. Revue d’Intelligence Artificielle 4(3), 9–52 (1990); Special issue on Automatic Deduction
[22] 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) · doi:10.1145/567446.567461
[23] Nahon, F.: Preuve par induction dans le calcul des séquents modulo. PhD thesis, Université Henri Poincaré - Nancy I, Nancy, France, October 26 (2007)
[24] Nahon, F., Kirchner, C., Kirchner, H., Brauner, P.: Inductive Proof Search Modulo. Annals of Mathematics and Artificial Intelligence 55(1-2), 123–154 (2009) · Zbl 1192.68631 · doi:10.1007/s10472-009-9154-5
[25] Steel, G.: Proof by consistency - a literature survey (March 1999)
[26] Wack, B.: Typage et déduction dans le calcul de réécriture. Thèse de doctorat, Université Henri Poincaré - Nancy I, October 7 (2005)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.