Inductive Consequences in the Calculus of Constructions

Autor:	Jacek Chrząszcz, Daria Walukiewicz-Chrząszcz
Rok vydání:	2010
Předmět:	Critical pair TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Type theory TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Proof assistant Calculus of constructions Extensionality Calculus Rewriting Extension (predicate logic) Completeness (statistics) Mathematics
Zdroj:	Interactive Theorem Proving ISBN: 9783642140518 ITP
DOI:	10.1007/978-3-642-14052-5_31
Popis:	Extending the calculus of constructions with rewriting would greatly improve the efficiency of proof assistants such as Coq. In this paper we address the issue of the logical power of such an extension. In our previous work we proposed a procedure to check completeness of user-defined rewrite systems. In many cases this procedure demonstrates that only a basic subset of the rules is sufficient for completeness. Now we investigate the question whether the remaining rules are inductive consequences of the basic subset. We show that the answer is positive for most practical rewrite systems. It is negative for some systems whose critical pair diagrams require rewriting under a lambda. However the positive answer can be recovered when the notion of inductive consequences is modified by allowing a certain form of functional extensionality.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::aeb613319418b268f339fcbc5e672016 https://doi.org/10.1007/978-3-642-14052-5_31 Zobrazit plný text záznamu