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

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

Authors: Peter Baumgartner, Stefan Brüning 

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

Recommendations

• An Implementation of the Model Elimination Proof Procedure
• Model elimination and connection tableau procedures
• A sequent-style model elimination strategy and a positive refinement
• Subsumption algorithms based on search trees
• scientific article; zbMATH DE number 517000

zbMATH Keywords

automated theorem provingsubsumptionmodel elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cited In (11)

• A sequent-style model elimination strategy and a positive refinement
• Title not available (Why is that?)
• Eliminating redundant search space on backtracking for forward chaining theorem proving
• Refutation search for Horn sets by a subgoal-extraction method
• R-SATCHMO: Refinements on I-SATCHMO
• Computing answers with model elimination
• On subsumption in distributed derivations
• Subgoal alternation in model elimination
• Towards a unified model of search in theorem-proving: subgoal-reduction strategies
• Model elimination and connection tableau procedures
• 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)