Abstract
It is commonly agreed that the success of future proof assistants will rely on their ability to incorporate computations within deduction in order to mimic the mathematician when replacing the proof of a proposition P by the proof of an equivalent proposition P’ obtained from P thanks to possibly complex calculations.
In this paper, we investigate a new version of the calculus of inductive constructions which incorporates arbitrary decision procedures into deduction via the conversion rule of the calculus. The novelty of the problem in the context of the calculus of inductive constructions lies in the fact that the computation mechanism varies along proof-checking: goals are sent to the decision procedure together with the set of user hypotheses available from the current context. Our main result shows that this extension of the calculus of constructions does not compromise its main properties: confluence, subject reduction, strong normalization and consistency are all preserved.
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
Coq-Development-Team: The Coq Proof Assistant Reference Manual - Version 8.0. INRIA, INRIA Rocquencourt, France (2004), http://coq.inria.fr/
Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76(2-3), 95–120 (1988)
Gonthier, G.: The four color theorem in coq. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, Springer, Heidelberg (2006)
Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG-88. LNCS, vol. 417, pp. 50–66. Springer, Heidelberg (1990)
Giménez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 397–408. Springer, Heidelberg (1998)
Barras, B.: Auto-validation d’un systéme de preuves avec familles inductives. PhD thesis, Université de Paris VII (1999)
Blanqui, F.: Definitions by rewriting in the calculus of constructions. Mathematical Structures in Computer Science, Journal version of LICS 2001. 15(1), 37–92 (2005)
Blanqui, F.: Inductive types in the calculus of algebraic constructions. Fundamenta Informaticae, Journal version of TLCA 2003. 65(1-2), 61–86 (2005)
Shostak, R.E.: An efficient decision procedure for arithmetic with function symbols. J. of the Association for Computing Machinery 26(2), 351–360 (1979)
Shankar, N.: Little engines of proof. In: Plotkin, G. (ed.) Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, LICS 2002, IEEE Computer Society Press, Los Alamitos (2002) (Invited Talk)
Corbineau, P.: Démonstration automatique en Théorie des Types. PhD thesis, University of Paris IX (2005)
Stehr, M.: The Open Calculus of Constructions: An equational type theory with dependent types for programming, specification, and interactive theorem proving (part I and II). Fundamenta Informaticae (to appear, 2007)
Oury, N.: Extensionality in the calculus of constructions. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 278–293. Springer, Heidelberg (2005)
Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-five years of constructive type theory. Oxford Logic Guides, vol. 36, pp. 83–111. Oxford University Press, Oxford (1998)
Blanqui, F., Jouannaud, J.P., Strub, P.Y.: A Calculus of Congruent Constructions, 2005 (unpublished draft)
Barendregt, H.: Lambda calculi with types. Handbook of logic in computer science, vol. 2. Oxford University Press, Oxford (1992)
Werner, B.: Une Théorie des Constructions Inductives. PhD thesis, University of Paris VII (1994)
Blanqui, F.: Type Theory and Rewriting. PhD thesis, Université de Paris XI, Orsay, France (2001)
Barthe, G.: The relevance of proof irrelevance. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, Springer, Heidelberg (1998)
Schmidt-Schauß, M.: Unification in a combination of arbitrary disjoint equational theories. J. Symbolic Computation, Special issue on Unification 8, 51–99 (1989)
Baader, F., Schulz, K.: Unification in the union of disjoint equational theories: Combining decision procedures. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol. 607, Springer, Heidelberg (1992)
Strub, P.Y.: Type Theory and Decision Procedures. PhD thesis, École Polytechnique, Palaiseau, France (Work in progress)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blanqui, F., Jouannaud, JP., Strub, PY. (2007). Building Decision Procedures in the Calculus of Inductive Constructions. In: Duparc, J., Henzinger, T.A. (eds) Computer Science Logic. CSL 2007. Lecture Notes in Computer Science, vol 4646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74915-8_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-74915-8_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74914-1
Online ISBN: 978-3-540-74915-8
eBook Packages: Computer ScienceComputer Science (R0)