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 eliminationhigher-order logicsimple type theoryfirst-order theoriesrewrite systemspre-model

Mathematics Subject Classification ID

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

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

• 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?)
• 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
• 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

(23)

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

Describes a project that uses

Uses Software

• Automath
• Coq

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)