Proof normalization modulo
From MaRDI portal
Publication:4650285
DOI10.2178/jsl/1067620188zbMath1059.03062OpenAlexW1977882652MaRDI QIDQ4650285
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
Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05)
Related Items (17)
A modular construction of type theories ⋮ Some general results about proof normalization ⋮ Extensional proofs in a propositional logic modulo isomorphisms ⋮ Unnamed Item ⋮ Unnamed Item ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms ⋮ Orthogonality and Boolean Algebras for Deduction Modulo ⋮ A simple proof that super-consistency implies cut elimination ⋮ Resolution is cut-free ⋮ Regaining cut admissibility in deduction modulo using abstract completion ⋮ Unnamed Item ⋮ On the expressive power of schemes ⋮ Axiom Directed Focusing ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ From the universality of mathematical truth to the interoperability of proof systems ⋮ On the Convergence of Reduction-based and Model-based Methods in Proof Theory
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The calculus of constructions
- Theorem proving modulo
- Automated deduction by theory resolution
- A Brief Overview of PVS
- A normalization theorem for set theory
- Intensional interpretations of functionals of finite type I
- On the sum Σ n P h i σ h j
- A formulation of the simple theory of types
- Banishing the rule of substitution for functional variables
This page was built for publication: Proof normalization modulo
