An Implementation of the Model Elimination Proof Procedure
From MaRDI portal
Publication:4770008
DOI10.1145/321796.321807zbMath0283.68057OpenAlexW2062032114WikidataQ56814474 ScholiaQ56814474MaRDI QIDQ4770008
Donald W. Loveland, A. K. Smiley III, S. Fleisig, D. L. Yarmush
Publication date: 1974
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/321796.321807
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (9)
Seventy Years of Computer Science ⋮ Hierarchical deduction ⋮ A Prolog technology theorem prover: Implementation by an extended Prolog compiler ⋮ Near-Horn Prolog and the ancestry family of procedures ⋮ Resolution remains hard under equivalence ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ A Prolog technology theorem prover: A new exposition and implementation in Prolog ⋮ Refutation graphs ⋮ Analytic resolution in theorem proving
This page was built for publication: An Implementation of the Model Elimination Proof Procedure
