Abstract canonical presentations

DOI10.1016/J.TCS.2006.03.012MaRDI QIDQ2500482zbMATH OpenOpenAlexFDO

Authors Nachum Dershowitz, Claude Kirchner

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

saturationredundancycanonicitycompletioncanonical rewritingproof orderings

Mathematics Subject Classification ID

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

Recommendations

• Abstract canonical inference
• Canonical representations
• Canonical representations
• scientific article; zbMATH DE number 2079676
• Canonical extensions and canonicity via dcpo presentations
• scientific article; zbMATH DE number 1048041
• Generalised weak presentations
• scientific article; zbMATH DE number 3845579

Cites work

• scientific article; zbMATH DE number 1688810 (Why is no real title available?)
• scientific article; zbMATH DE number 1701351 (Why is no real title available?)
• scientific article; zbMATH DE number 3941661 (Why is no real title available?)
• scientific article; zbMATH DE number 4056995 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 3635472 (Why is no real title available?)
• scientific article; zbMATH DE number 3290336 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A complete proof of correctness of the Knuth-Bendix completion algorithm
• About the rewriting systems produced by the Knuth-Bendix completion algorithm
• Abstract canonical inference
• Abstract canonical presentations
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• Complete Sets of Reductions for Some Equational Theories
• Completion Is an Instance of Abstract Canonical System Inference
• Completion for unification
• Completion of a Set of Rules Modulo a Set of Equations
• Completion of first-order clauses with equality by strict superposition
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Equational inference, canonical proofs, and proof orderings
• Existence, Uniqueness, and Construction of Rewrite Systems
• History and basic features of the critical-pair/completion procedure
• Orderings for term-rewriting systems
• Paramodulation-based theorem proving
• Proof by consistency
• Proving refutational completeness of theorem-proving strategies
• Pure patterns type systems
• Resolution theorem proving
• Rewriting
• Theorem proving modulo
• Theorem-proving with resolution and superposition
• Towards a foundation of completion procedures as semidecision procedures

Cited in

(8)

• Canonical ground Horn theories
• Abstract canonical inference
• Structures for abstract rewriting
• Some general results about proof normalization
• Abstract canonical presentations
• Canonicity!
• 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

This page was built for publication: Abstract canonical presentations

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