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

DOI10.1023/A:1005812703468MaRDI QIDQ1369080zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

automated theorem provingsubsumptionmodel elimination

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

Cited in

(11)

• A sequent-style model elimination strategy and a positive refinement
• scientific article; zbMATH DE number 4047180 (Why is no real title available?)
• Eliminating redundant search space on backtracking for forward chaining theorem proving
• Refutation search for Horn sets by a subgoal-extraction method
• Computing answers with model elimination
• R-SATCHMO: Refinements on I-SATCHMO
• 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

Describes a project that uses

Uses Software

• TPTP
• SETHEO

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)