A disjunctive positive refinement of model elimination and its application to subsumption deletion

DOI10.1023/A:1005812703468zbMATH Open0885.03011OpenAlexW1519829133MaRDI QIDQ1369080FDOQ1369080

Stefan Brüning, Peter Baumgartner

Publication date: 15 April 1998

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1023/a:1005812703468

zbMATH Keywords

automated theorem provingsubsumptionmodel elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (2)

• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Controlled use of clausal lemmas in connection tableau calculi

Uses Software

• SETHEO
• TPTP

This page was built for publication: A disjunctive positive refinement of model elimination and its application to subsumption deletion

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