Arithmetic as a theory modulo
Logic in Computer Science
2023-10-17 v1
Abstract
We present constructive arithmetic in Deduction modulo with rewrite rules only.
Cite
@article{arxiv.2310.10326,
title = {Arithmetic as a theory modulo},
author = {Gilles Dowek and Benjamin Werner},
journal= {arXiv preprint arXiv:2310.10326},
year = {2023}
}
Related papers
View all related →
Logic in Computer Science · Computer Science
What is a Theory ?
Gilles Dowek
2023-05-26
Logic in Computer Science · Computer Science
Rewriting modulo in Deduction modulo
Frédéric Blanqui
2016-08-16
Logic in Computer Science · Computer Science
Simple Type Theory as a Clausal Theory
Gilles Dowek
2023-04-27
Logic in Computer Science · Computer Science
Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo
Guillaume Burel
2019-03-14
Logic in Computer Science · Computer Science
From Rewrite Rules to Axioms in the $\lambda$$\Pi$-Calculus Modulo Theory
Valentin Blot, Gilles Dowek, Thomas Traversié, Théo Winterhalter
2024-02-15
Logic in Computer Science · Computer Science
Definitions by Rewriting in the Calculus of Constructions
Frédéric Blanqui
2016-08-16
Logic in Computer Science · Computer Science
Deduction modulo theory
Gilles Dowek
2015-01-27
Logic in Computer Science · Computer Science
Building Decision Procedures in the Calculus of Inductive Constructions
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
2007-07-10
Logic in Computer Science · Computer Science
Definitions by rewriting in the Calculus of Constructions
Frédéric Blanqui
2016-08-16
Logic in Computer Science · Computer Science
Deduction as Reduction
Dominique Duval
2010-11-10
Commutative Algebra · Mathematics
Commutative algebra: Constructive methods. Finite projective modules
Henri Lombardi, Claude Quitté
2024-09-20
Logic · Mathematics
Constructive Reverse Mathematics
Hannes Diener
2020-04-07
Logic in Computer Science · Computer Science
Combining Deduction Modulo and Logics of Fixed-Point Definitions
David Baelde, Gopalan Nadathur
2012-04-30
Logic in Computer Science · Computer Science
Cut elimination for Zermelo set theory
Gilles Dowek, Alexandre Miquel
2023-11-01
Computation and Language · Computer Science
Type Arithmetics: Computation based on the theory of types
Oleg Kiselyov
2007-05-23
Logic · Mathematics
Non-determinsitic algebraic rewriting as adjunction
Răzvan Diaconescu
2022-04-27
Representation Theory · Mathematics
Rewriting modulo in diagrammatic algebras and application to categorification
Léo Schelstraete
2025-02-06
Logic · Mathematics
Further results and examples for formal mathematical systems with structural induction
Matthias Kunik
2022-01-21
Logic in Computer Science · Computer Science
Specifying programs with propositions and with congruences
Gilles Dowek
2023-04-27
Logic · Mathematics
Formal Mathematical Systems including a Structural Induction Principle
Matthias Kunik
2021-12-21
Logic in Computer Science · Computer Science
The Stratified Foundations as a theory modulo
Gilles Dowek
2023-05-31
Commutative Algebra · Mathematics
Primary decomposition of modules: a computational differential approach
Justin Chen, Yairon Cid-Ruiz
2022-02-15
Combinatorics · Mathematics
Arithmetree
Jean-Louis Loday
2007-05-23
Logic in Computer Science · Computer Science
Classical Mathematics for a Constructive World
Russell O'Connor
2011-10-18
Logic in Computer Science · Computer Science
Confluence as a cut elimination property
Gilles Dowek
2023-05-24