The use of lemmas in the model elimination procedure

DOI10.1023/A:1005770705587zbMATH Open0882.68132OpenAlexW1600228510MaRDI QIDQ1367083FDOQ1367083

Authors: 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

Recommendations

• scientific article; zbMATH DE number 1500560
• Lemma and cut strategies for propositional model elimination
• Persistent and quasi-persistent lemmas in propositional model elimination
• An Implementation of the Model Elimination Proof Procedure
• scientific article; zbMATH DE number 1612567

zbMATH Keywords

model eliminationMETEOR

Mathematics Subject Classification ID

Cited In (14)

• On terminating lemma speculations.
• The resonance strategy
• Lemma matching for a PTTP-based top-down theorem prover
• First order Stålmarck. Universal lemmas through branch merges
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• Persistent and quasi-persistent lemmas in propositional model elimination
• Title not available (Why is that?)
• On the modelling of search in theorem proving -- towards a theory of strategy analysis
• Evaluating general purpose automated theorem proving systems
• Subsumption-linear Q-resolution for QBF theorem proving
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• An Implementation of the Model Elimination Proof Procedure
• Controlled use of clausal lemmas in connection tableau calculi
• Lemma and cut strategies for propositional model elimination

Uses Software

• SETHEO

This page was built for publication: The use of lemmas in the model elimination procedure

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