Proof normalization modulo

DOI10.2178/JSL/1067620188MaRDI QIDQ4650285zbMATH OpenOpenAlexFDO

Authors Gilles Dowek, Benjamin Werner

Publication date 9 February 2005

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL https://projecteuclid.org/euclid.jsl/1067620188, https://hal.inria.fr/inria-00073143/file/RR-3542.pdf

zbMATH Keywords

cut eliminationfirst-order theorieshigher-order logicpre-modelrewrite systemssimple type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)

Recommendations

• A Semantic Proof that Reducibility Candidates entail Cut Elimination
• Modular Cut-Elimination: Finding Proofs or Counterexamples
• About folding-unfolding cuts and cuts modulo
• Orthogonality and Boolean Algebras for Deduction Modulo
• scientific article; zbMATH DE number 1082077

Cites work

• A Brief Overview of PVS
• A formulation of the simple theory of types
• A normalization theorem for set theory
• Automated deduction by theory resolution
• Banishing the rule of substitution for functional variables
• scientific article; zbMATH DE number 4147469 (Why is no real title available?)
• scientific article; zbMATH DE number 4091495 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3702108 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 512790 (Why is no real title available?)
• scientific article; zbMATH DE number 1082077 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• Intensional interpretations of functionals of finite type I
• On the sum Σ n  P h i σ h j
• The calculus of constructions
• Theorem proving modulo

Cited in

(25)

• Some general results about proof normalization
• From the universality of mathematical truth to the interoperability of proof systems
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Regaining cut admissibility in deduction modulo using abstract completion
• About folding-unfolding cuts and cuts modulo
• On the convergence of reduction-based and model-based methods in proof theory
• Orthogonality and Boolean Algebras for Deduction Modulo
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• scientific article; zbMATH DE number 1808201 (Why is no real title available?)
• A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
• Axiom Directed Focusing
• scientific article; zbMATH DE number 1082077 (Why is no real title available?)
• scientific article; zbMATH DE number 1420786 (Why is no real title available?)
• Index-stratified types
• Linking focusing and resolution with selection
• Proof normalisation in a logic identifying isomorphic propositions
• Modular Cut-Elimination: Finding Proofs or Counterexamples
• A Simple Proof That Super-Consistency Implies Cut Elimination
• A modular construction of type theories
• Extensional proofs in a propositional logic modulo isomorphisms
• Theoretical computer science: computability, decidability and logic
• A simple proof that super-consistency implies cut elimination
• Judgmental and definitional equality from a Fregean perspective
• On the expressive power of schemes
• Resolution is cut-free

Describes a project that uses

Uses Software

• Coq
• Automath

This page was built for publication: Proof normalization modulo

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