Two Results on Ordering for Resolution with Merging and Linear Format

DOI10.1145/321662.321678MaRDI QIDQ5649439zbMATH OpenOpenAlexFDO

Authors Raymond Reiter

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

Mathematics Subject Classification ID

Cited in

(9)

• Saturation, nonmonotonic reasoning and the closed-world assumption
• A logic for default reasoning
• An extension to linear resolution with selection function
• Linear resolution for consequence finding
• Experimental tests of resolution-based theorem-proving strategies
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• A note on linear resolution strategies in consequence-finding
• Multi-ary \(\alpha\)-semantic resolution automated reasoning based on lattice-valued first-order logic \(\mathrm{LF}(X)\)
• Strategies of the search for derivation of statements with restricted quantifiers

This page was built for publication: Two Results on Ordering for Resolution with Merging and Linear Format

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