A note on linear resolution strategies in consequence-finding

DOI10.1016/0004-3702(72)90047-1zbMath0252.68049OpenAlexW2047961808MaRDI QIDQ2557565

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

Related Items

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

Cites Work

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