Abstract canonical presentations

DOI10.1016/j.tcs.2006.03.012zbMath1099.03047OpenAlexW2130170010MaRDI QIDQ2500482

Claude Kirchner, Nachum Dershowitz

Publication date: 16 August 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.03.012

zbMATH Keywords

completionredundancysaturationcanonicitycanonical rewritingproof orderings

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items (7)

Structures for abstract rewriting ⋮ Some general results about proof normalization ⋮ Canonicity! ⋮ Canonical Ground Horn Theories ⋮ Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01). ⋮ Regaining cut admissibility in deduction modulo using abstract completion ⋮ Abstract canonical presentations

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
• Orderings for term-rewriting systems
• Towards a foundation of completion procedures as semidecision procedures
• Theorem-proving with resolution and superposition
• Proof by consistency
• History and basic features of the critical-pair/completion procedure
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• Completion for unification
• Theorem proving modulo
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Abstract canonical presentations
• Pure patterns type systems
• Existence, Uniqueness, and Construction of Rewrite Systems
• Completion of a Set of Rules Modulo a Set of Equations
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• Equational inference, canonical proofs, and proof orderings
• Proving refutational completeness of theorem-proving strategies
• Abstract canonical inference
• Completion Is an Instance of Abstract Canonical System Inference
• Completion of first-order clauses with equality by strict superposition

This page was built for publication: Abstract canonical presentations