Abstract : The main novelty of this paper is to consider an extension of the Calculus of Constructions where predicates can be defined with a general form of rewrite rules. We prov...
act Completion (Full Version) Guillaume Burel Claude Kirchner August 6, 2007 Deduction Modulo implements Poincar´e’s principle by identifying deduction and computation as diff...