Proof normalization modulo

DOI10.2178/JSL/1067620188zbMATH Open1059.03062OpenAlexW1977882652MaRDI QIDQ4650285FDOQ4650285

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

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

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)

Cites Work

• A Brief Overview of PVS
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• A formulation of the simple theory of types
• Automated deduction by theory resolution
• The calculus of constructions
• Theorem proving modulo
• Intensional interpretations of functionals of finite type I
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Banishing the rule of substitution for functional variables
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the sum Σ n  P h i σ h j
• Title not available (Why is that?)
• A normalization theorem for set theory

Cited In (23)

• A simple proof that super-consistency implies cut elimination
• Title not available (Why is that?)
• From the universality of mathematical truth to the interoperability of proof systems
• Title not available (Why is that?)
• Axiom Directed Focusing
• Extensional proofs in a propositional logic modulo isomorphisms
• On the expressive power of schemes
• 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
• Index-stratified types
• Some general results about proof normalization
• 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
• A modular construction of type theories
• Regaining cut admissibility in deduction modulo using abstract completion
• 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
• Title not available (Why is that?)
• A Simple Proof That Super-Consistency Implies Cut Elimination

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)