A note on linear resolution strategies in consequence-finding

DOI10.1016/0004-3702(72)90047-1MaRDI QIDQ2557565zbMATH OpenOpenAlexFDO

Authors Eliana Minicozzi, Raymond Reiter

Publication date 1972

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0004-3702(72)90047-1

Mathematics Subject Classification ID

Cites work

• A Linear Format for Resolution With Merging and a New Technique for Establishing Completeness
• A Machine-Oriented Logic Based on the Resolution Principle
• A Unifying View of Some Linear Herbrand Procedures
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Linear resolution with selection function
• Resolution graphs
• The Unit Proof and the Input Proof in Theorem Proving
• Two Results on Ordering for Resolution with Merging and Linear Format

Cited in

(6)

• Default reasoning using classical logic
• Linear resolution for consequence finding
• First order LUB approximations: characterization and algorithms
• Partition-based logical reasoning for first-order and propositional theories
• A Prolog technology theorem prover: A new exposition and implementation in Prolog
• A Modal-Layered Resolution Calculus for K

This page was built for publication: A note on linear resolution strategies in consequence-finding

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