Abstract canonical inference

DOI10.1145/1182613.1182619MaRDI QIDQ5277771zbMATH OpenOpenAlexWikidataFDO

Authors Maria Paola Bonacina, Nachum Dershowitz

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

canonicitycompletenesscompletionfairnessinferenceproof orderingsredundancysaturation

Mathematics Subject Classification ID

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

Abstract: An abstract framework of canonical inference is used to explore how different proof orderings induce different variants of saturation and completeness. Notions like completion, paramodulation, saturation, redundancy elimination, and rewrite-system reduction are connected to proof orderings. Fairness of deductive mechanisms is defined in terms of proof orderings, distinguishing between (ordinary) "fairness," which yields completeness, and "uniform fairness," which yields saturation.

Recommendations

• Canonicity!
• Equational inference, canonical proofs, and proof orderings
• Abstract completion, formalized
• Completion Is an Instance of Abstract Canonical System Inference
• Abstract canonical presentations

Cited in

(14)

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

This page was built for publication: Abstract canonical inference

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