scientific article; zbMATH DE number 2043517

MaRDI QIDQ4447217zbMATH OpenFDO

Authors Gilles Dowek

Publication date 16 February 2004

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2706/27060002.htm

zbMATH Keywords

asymmetric deductionconfluencecut eliminationrewriting system on terms

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42)

Recommendations

• Cut Admissibility by Saturation
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• Confluence by critical pair analysis
• Confluence of the disjoint union of conditional term rewriting systems
• Typed Lambda Calculi and Applications

Cited in

(7)

• Some general results about proof normalization
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• Regaining cut admissibility in deduction modulo using abstract completion
• Structure of proofs and the complexity of cut elimination
• A Completion Method to Decide Reachability in Rewrite Systems
• Automating theories in intuitionistic logic
• Canonical ground Horn theories

This page was built for publication:

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