Two Results on Ordering for Resolution with Merging and Linear Format
From MaRDI portal
Publication:5649439
DOI10.1145/321662.321678zbMath0238.68030OpenAlexW2003287551MaRDI QIDQ5649439
Publication date: 1971
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321662.321678
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (9)
A logic for default reasoning ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ An extension to linear resolution with selection function ⋮ Multi-ary α-semantic resolution automated reasoning based on lattice-valued first-order logic LF (X)1 ⋮ Linear resolution for consequence finding ⋮ Experimental tests of resolution-based theorem-proving strategies ⋮ A note on linear resolution strategies in consequence-finding ⋮ Strategies of the search for derivation of statements with restricted quantifiers ⋮ Saturation, nonmonotonic reasoning and the closed-world assumption
This page was built for publication: Two Results on Ordering for Resolution with Merging and Linear Format
