Abstract
Superdeduction is a systematic way to extend a deduction system like the sequent calculus by new deduction rules computed from the user theory. We show how this could be done in a systematic, correct and complete way. We prove in detail the strong normalisation of a proof term language that models appropriately superdeduction. We finaly examplify on several examples, including equality and noetherian induction, the usefulness of this approach which is implemented in the \(\sf{lemurid{\ae}}\) system, written in TOM.
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
Alvarado, C.: Reflection for rewriting in the calculus of inductive constructions. In: Proceedings of TYPES 2000, Durham, United Kingdom (December 2000)
Andreoli, J.-M., Maieli, R.: Focusing and proof-nets in linear and non-commutative logic. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705, pp. 321–336. Springer, Heidelberg (1999)
Andreoli, J.-M.: Logic programming with focusing proofs in linear logic. Journal of Logic and Computation 2(3), 297–347 (1992)
Andreoli, J.-M.: Focussing and proof construction. Annals Pure Applied Logic 107(1-3), 131–163 (2001)
Brauner, P., Dowek, G., Wack, B.: Normalization in supernatural deduction and in deduction modulo (2007), Available at http://hal.inria.fr/inria-00141720
Bezem, M., Hendriks, D., de Nivelle, H.: Automated proof construction in type theory using resolution. Journal of Automated Reasoning 29(3-4), 253–275 (2002)
Brauner, P., Houtmann, C., Kirchner, C.: Principles of superdeduction. In: Proceedings of LICS (July 2007)
Blanqui, F., Jouannaud, J.-P., Okada, M.: Inductive Data Type Systems. Theoretical Computer Science 272(1-2), 41–68 (2002)
Brauner, P.: Un calcul des séquents extensible. Master’s thesis, Université Henri Poincaré – Nancy 1 (2006)
Burel, G.: Unbounded proof-length speed-up in deduction modulo. Technical report, INRIA Lorraine (2007), Available at http://hal.inria.fr/inria-00138195
Cousineau, D., Dowek, G.: Embedding pure type systems in the lambda-pi-calculus modulo. In: TLCA 2007. LNCS, vol. 4583. Springer, Heidelberg (to appear, 2007)
Curien, P.-L., Herbelin, H.: The duality of computation. In: ICFP ’00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pp. 233–243. ACM Press, New York, NY, USA (2000)
Cirstea, H., Kirchner, C.: The rewriting calculus — Part I and II. Logic Journal of the Interest Group in Pure and Applied Logics 9(3), 427–498 (2001)
Cirstea, H., Liquori, L., Wack, B.: Rewriting calculus with fixpoints: Untyped and first-order systems. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, Springer, Heidelberg (2004)
Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning 31(1), 33–72 (2003)
Dowek, G., Miquel, A.: Cut elimination for Zermelo’s set theory. Available on author’s web page (2007)
Dowek, G.: Proof normalization for a first-order formulation of higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 105–119. Springer, Heidelberg (1997)
Dowek, G., Werner, B.: Proof normalization modulo. Journal of Symbolic Logic 68(4), 1289–1316 (2003)
Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 423–437. Springer, Heidelberg (2005)
Herbelin, H.: Séquents qu’on calcule. PhD thesis, Université Paris 7 (January 1995)
University of Cambridge, DSTO, SRI Internatioal. Description of the HOL-System (1993)
Houtmann, C.: Cohérence de la déduction surnaturelle. Master’s thesis, École Normale Supérieure de Cachan (2006)
Jouannaud, J.-P.: Higher-order rewriting: Framework, confluence and termination. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R.C. (eds.) Processes, Terms and Cycles, pp. 224–250 (2005)
Kirchner, F.: A finite first-order theory of classes (2006) http://www.lix.polytechnique.fr/Labo/Florent.Kirchner/
Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: Automatic combinability of rewriting-based satisfiability procedures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 542–556. Springer, Heidelberg (2006)
Lengrand, S.: Call-by-value, call-by-name, and strong normalization for the classical sequent calculus. Electronic Notes in Theoretical Computer Science, vol. 86(4) (2003)
Meng, J., Quigley, C., Paulson, L.C.: Automation for interactive proof: First prototype. Information and Computation 204(10), 1575–1596 (2006)
Moreau, P.-E., Reilles, A.: The tom home page (2006) http://tom.loria.fr
Nguyen, Q.-H., Kirchner, C., Kirchner, H.: External rewriting for skeptical proof assistants. Journal of Automated Reasoning 29(3-4), 309–336 (2002)
Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)
Paulson, L.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Heidelberg (1994)
Prawitz, D.: Natural Deduction. A Proof-Theoretical Study, vol. 3 of Stockholm Studies in Philosophy. Almqvist & Wiksell, Stockholm (1965)
Prevosto, V.: Certified mathematical hierarchies: the focal system. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs, number 05021 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany (2005)
Rudnicki, P.: An overview of the Mizar project. Notes to a talk at the workshop on Types for Proofs and Programs (June 1992)
The Coq development team. The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)
Urban, C., Bierman, G.M.: Strong normalisation of cut-elimination in classical logic. Fundam. Inform. 45(1-2), 123–155 (2001)
Urban, C.: Classical Logic and Computation. PhD thesis, University of Cambridge, (October 2000)
Urban, C.: Strong normalisation for a gentzen-like cut-elimination procedure. In: Abramsky, S. (ed.) TLCA 2001. LNCS, vol. 2044, pp. 415–430. Springer, Heidelberg (2001)
Visser, E., Benaissa, Z.-e.-A.: A core language for rewriting. In: Kirchner, C., Kirchner, H. (eds.) WRLA, Pont-à-Mousson, France, September 1998. Electronic Notes in Theoretical Computer Science, vol. 15, Elsevier, North-Holland (1998)
van Bakel, S., Lengrand, S., Lescanne, P.: The language χ: circuits, computations and classical logic. In: van Bakel, S., Lengrand, S., Lescanne, P. (eds.) ICTCS 2005. Proceedings of Ninth Italian Conference on Theoretical Computer Science. LNCS, vol. 3701, pp. 81–96. Springer, Heidelberg (2005)
Wack, B.: Typage et déduction dans le calcul de réécriture. PhD thesis, Université Henri Poincaré, Nancy 1 (October 2005)
Wadler, P.: Call-by-value is dual to call-by-name. In: ICFP ’03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, September 2003, pp. 189–201. ACM Press, New York (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Brauner, P., Houtmann, C., Kirchner, C. (2007). Superdeduction at Work. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds) Rewriting, Computation and Proof. Lecture Notes in Computer Science, vol 4600. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73147-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-73147-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73146-7
Online ISBN: 978-3-540-73147-4
eBook Packages: Computer ScienceComputer Science (R0)