A note on linear resolution strategies in consequence-finding

DOI10.1016/0004-3702(72)90047-1zbMATH Open0252.68049OpenAlexW2047961808MaRDI QIDQ2557565FDOQ2557565

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 Machine-Oriented Logic Based on the Resolution Principle
• Linear resolution with selection function
• 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
• Resolution graphs
• A Unifying View of Some Linear Herbrand Procedures

Cited In (6)

• 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
• Default reasoning using classical logic

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)