The use of lemmas in the model elimination procedure

DOI10.1023/A:1005770705587MaRDI QIDQ1367083zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

model eliminationMETEOR

Mathematics Subject Classification ID

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

Cited in

(15)

• 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
• scientific article; zbMATH DE number 1612567 (Why is no real title available?)
• 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
• Lemmatization for stronger reasoning in large theories
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• An Implementation of the Model Elimination Proof Procedure
• Lemma and cut strategies for propositional model elimination
• Controlled use of clausal lemmas in connection tableau calculi

Describes a project that uses

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)