Equational inference, canonical proofs, and proof orderings

DOI10.1145/174652.174655zbMath0806.68095OpenAlexW2161257777MaRDI QIDQ4299008

Leo Bachmair, Nachum Dershowitz

Publication date: 29 June 1994

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/174652.174655

zbMATH Keywords

inference systemstheorem-proving methods

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (18)

Structures for abstract rewriting ⋮ Multi-completion with termination tools ⋮ Paramodulation with non-monotonic orderings and simplification ⋮ Linear and unit-resulting refutations for Horn theories ⋮ Buchberger's algorithm: A constraint-based completion procedure ⋮ The Maude strategy language ⋮ Canonicity! ⋮ Canonical Inference for Implicational Systems ⋮ Towards a foundation of completion procedures as semidecision procedures ⋮ Natural termination ⋮ Canonical Ground Horn Theories ⋮ The Blossom of Finite Semantic Trees ⋮ Canonicity1 1This research was supported in part by the Israel Science Foundation (grant no. 254/01). ⋮ Termination Tools in Ordered Completion ⋮ Abstract canonical presentations ⋮ Larry Wos: visions of automated reasoning ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ Deductive and inductive synthesis of equational programs

This page was built for publication: Equational inference, canonical proofs, and proof orderings