Equational inference, canonical proofs, and proof orderings
From MaRDI portal
Publication:4299008
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
Related Items
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
