Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-14052-5_31 | ITP |
Keywords | Field | DocType |
critical pair diagram,functional extensionality,positive answer,logical power,certain form,remaining rule,basic subset,previous work,proof assistant,inductive consequence | Discrete mathematics,Extensionality,Computer science,Algorithm,Type theory,Critical pair,Calculus of constructions,Rewriting,Completeness (statistics),Calculus,Proof assistant | Conference |
Volume | ISSN | ISBN |
6172 | 0302-9743 | 3-642-14051-3 |
Citations | PageRank | References |
1 | 0.38 | 13 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daria Walukiewicz-Chrząszcz | 1 | 26 | 3.35 |
| Jacek Chrząszcz | 2 | 2 | 1.11 |