A Unifying View of Some Linear Herbrand Procedures

DOI10.1145/321694.321706MaRDI QIDQ5655006zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Donald W. Loveland

Publication date 1972

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

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

Mathematics Subject Classification ID

Cited in

(8)

• Refutation graphs
• Controlled integration of the cut rule into connection tableau calculi
• A comparative study of several proof procedures
• Complexity analysis of propositional resolution with autarky pruning
• Set of support, demodulation, paramodulation: a historical perspective
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• A note on linear resolution strategies in consequence-finding
• Automatic theorem proving in paraconsistent logics: Theory and implementation

This page was built for publication: A Unifying View of Some Linear Herbrand Procedures

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