Arithmetic as a theory modulo

DOI10.1007/978-3-540-32033-3_31MaRDI QIDQ5703867zbMATH OpenOpenAlexFDO

Authors Gilles Dowek, Benjamin Werner

Publication date 11 November 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b135673

zbMATH Keywords

cut elimination normalizationdeduction moduloHeyting arithmetic

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Grammars and rewriting systems (68Q42)

Cited in

(13)

• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Regaining cut admissibility in deduction modulo using abstract completion
• On the convergence of reduction-based and model-based methods in proof theory
• Verificationism and Classical Realizability
• Automating theories in intuitionistic logic
• Term sequent logic
• Learning Modulo Theories
• Linking focusing and resolution with selection
• Experimenting with deduction modulo
• scientific article; zbMATH DE number 2362600 (Why is no real title available?)
• A modular construction of type theories
• On the expressive power of schemes
• Resolution is cut-free

This page was built for publication: Arithmetic as a theory modulo

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5703867)