The use of lemmas in the model elimination procedure
From MaRDI portal
Publication:1367083
DOI10.1023/A:1005770705587zbMath0882.68132OpenAlexW1600228510MaRDI QIDQ1367083
O. L. Astrachan, Donald W. Loveland
Publication date: 17 September 1997
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1023/a:1005770705587
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ Subsumption-linear Q-resolution for QBF theorem proving ⋮ Towards a unified model of search in theorem-proving: subgoal-reduction strategies ⋮ Controlled use of clausal lemmas in connection tableau calculi ⋮ On the modelling of search in theorem proving -- towards a theory of strategy analysis ⋮ Lemma matching for a PTTP-based top-down theorem prover ⋮ Evaluating general purpose automated theorem proving systems
Uses Software
This page was built for publication: The use of lemmas in the model elimination procedure
