Some general results about proof normalization

DOI10.1007/s11787-010-0011-4zbMath1255.03050OpenAlexW1966145877MaRDI QIDQ1931341

Marc Aiguier, Delphine Longuet

Publication date: 25 January 2013

Published in: Logica Universalis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11787-010-0011-4

zbMATH Keywords

cut eliminationrewritingformal systemsproof tree transformationweak and strong normalization

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Abstract deductive systems (03B22)

Uses Software

• Coq
• Isabelle
• CoCasl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Proof-guided test selection from first-order specifications with equality
• Bi-rewrite systems
• An institution-independent proof of the Beth definability theorem
• Conditional rewrite rules
• On the existence of free models in abstract algebraic institutions
• Quasi-varieties in abstract algebraic institutions
• A note on simplification orderings
• Term rewriting for normalization by evaluation.
• Theorem proving modulo
• Isabelle/HOL. A proof assistant for higher-order logic
• Display logic
• Logical systems for structured specifications.
• Logicality of conditional rewrite systems
• Stratified institutions and elementary homomorphisms
• Institution-independent model theory
• Abstract canonical presentations
• Structures for abstract rewriting
• Integration Testing from Structured First-Order Specifications via Deduction Modulo
• Testing from Algebraic Specifications: Test Data Set Selection by Unfolding Axioms
• Test Selection Criteria for Quantifier-Free First-Order Specifications
• Specification-Based Testing for CoCasl’s Modal Specifications
• Institutions: abstract model theory for specification and programming
• Proof normalization modulo
• Term Rewriting and All That
• Interpolation and compactness in categories of pre-institutions
• Functional and Logic Programming
• Computer Science Logic
• Typed Lambda Calculi and Applications

This page was built for publication: Some general results about proof normalization