Abstract canonical inference

DOI10.1145/1182613.1182619zbMath1367.03023arXivcs/0406030OpenAlexW3104411811WikidataQ118123557 ScholiaQ118123557MaRDI QIDQ5277771

Nachum Dershowitz, Maria Paola Bonacina

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/cs/0406030

zbMATH Keywords

fairnesscompletenesscompletionredundancyinferencesaturationcanonicityproof orderings

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Related Items

Interpolation systems for ground proofs in automated deduction: a survey, Structures for abstract rewriting, From diagrammatic confluence to modularity, Canonicity!, Canonical Inference for Implicational Systems, Towards a unified model of search in theorem-proving: subgoal-reduction strategies, On Interpolation in Decision Procedures, Canonical Ground Horn Theories, Regaining cut admissibility in deduction modulo using abstract completion, Abstract canonical presentations, On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving, Set of support, demodulation, paramodulation: a historical perspective