Computing answers with model elimination

DOI10.1016/S0004-3702(96)00042-2MaRDI QIDQ1402748zbMATH OpenFDO

Authors Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg

Publication date 28 August 2003

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0004-3702(96)00042-2

zbMATH Keywords

Automated reasoningComputing answersLogic programingModel eliminationTheorem proving

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Logic programming (68N17)

Recommendations

• Model elimination without contrapositives
• scientific article; zbMATH DE number 1292288
• An Implementation of the Model Elimination Proof Procedure
• scientific article; zbMATH DE number 517000
• A disjunctive positive refinement of model elimination and its application to subsumption deletion

Cites work

• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Automated deduction by theory resolution
• Consolution as a framework for comparing calculi
• Controlled integration of the cut rule into connection tableau calculi
• scientific article; zbMATH DE number 4049047 (Why is no real title available?)
• scientific article; zbMATH DE number 4094866 (Why is no real title available?)
• scientific article; zbMATH DE number 3672245 (Why is no real title available?)
• scientific article; zbMATH DE number 43398 (Why is no real title available?)
• scientific article; zbMATH DE number 67453 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 408808 (Why is no real title available?)
• scientific article; zbMATH DE number 1330425 (Why is no real title available?)
• scientific article; zbMATH DE number 3380160 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• Implication of clauses is undecidable
• Mechanical Theorem-Proving by Model Elimination
• Model elimination without contrapositives
• Near-Horn prolog and beyond
• Near-Horn Prolog and the ancestry family of procedures
• Non-Horn clause logic programming without contrapositives
• Problem corner: Predicate logic hacker tricks
• Removing redundancy from a clause
• SETHEO: A high-performance theorem prover
• The TPTP problem library

Cited in

(7)

• Computing finite models by reduction to function-free clause logic
• Eliminating models during model elimination
• Blocking and other enhancements for bottom-up model generation methods
• Computationally Equivalent Elimination of Conditions
• scientific article; zbMATH DE number 1292288 (Why is no real title available?)
• Model elimination without contrapositives
• An abductive framework for negation in disjunctive logic programming

Describes a project that uses

Uses Software

• SETHEO
• OTTER
• TPTP
• SATCHMO
• PROTEIN

This page was built for publication: Computing answers with model elimination

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