Related papers: Arithmetic as a theory modulo
Deduction modulo is a way to express a theory using computation rules instead of axioms. We present in this paper an extension of deduction modulo, called Polarized deduction modulo, where some rules can only be used at positive…
We study the termination of rewriting modulo a set of equations in the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. In a previous…
We give a presentation of Simple Type Theory as a clausal rewrite system in Polarized deduction modulo.
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the…
The $\lambda$$\Pi$-calculus modulo theory is an extension of simply typed $\lambda$-calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the…
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 prove the strong normalization of the reduction relation generated by the…
This paper is a survey on Deduction modulo theory
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…
This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined…
Deduction systems and graph rewriting systems are compared within a common categorical framework. This leads to an improved deduction method in diagrammatic logics.
This book is an introductory course to basic commutative algebra with a particular emphasis on finitely generated projective modules. We adopt the constructive point of view, with which all existence theorems have an explicit algorithmic…
An introduction and overview of constructive reverse mathematics.
Inductive and coinductive specifications are widely used in formalizing computational systems. Such specifications have a natural rendition in logics that support fixed-point definitions. Another useful formalization device is that of…
We show how to express intuitionistic Zermelo set theory in deduction modulo (i.e. by replacing its axioms by rewrite rules) in such a way that the corresponding notion of proof enjoys the normalization property. To do so, we first rephrase…
The present paper shows meta-programming turn programming, which is rich enough to express arbitrary arithmetic computations. We demonstrate a type system that implements Peano arithmetics, slightly generalized to negative numbers. Certain…
We develop a general model theoretic semantics to rewriting beyond the usual confluence and termination assumptions. This is based on preordered algebra which is a model theory that extends many sorted algebra. In this framework we…
We develop a rewriting theory suitable for diagrammatic algebras and lay down the foundations of a systematic study of their higher structures. In this paper, we focus on the question of finding bases. As an application, we give the first…
In the former article "Formal mathematical systems including a structural induction principle" we have presented a unified theory for formal mathematical systems including recursive systems closely related to formal grammars, including the…
We give a presentation of Krivine and Parigot's Second-order functional arithmetic in Deduction modulo. Expressing this theory in Deduction modulo sheds light on an original aspect of this theory: the fact that programs are specified, not…
We present a unified theory for formal mathematical systems including recursive systems closely related to formal grammars, including the predicate calculus as well as a formal induction principle. We introduce recursive systems generating…