Computing answers with model elimination

DOI10.1016/S0004-3702(96)00042-2zbMath1017.03505MaRDI QIDQ1402748

Ulrich Furbach, Frieder Stolzenburg, Peter Baumgartner

Publication date: 28 August 2003

Published in: Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

Automated reasoningTheorem provingComputing answersLogic programingModel elimination

Mathematics Subject Classification ID

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

Related Items

Computing finite models by reduction to function-free clause logic, Blocking and other enhancements for bottom-up model generation methods, An abductive framework for negation in disjunctive logic programming

Uses Software

• SETHEO
• OTTER
• TPTP
• SATCHMO
• PROTEIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Removing redundancy from a clause
• Near-Horn prolog and beyond
• Implication of clauses is undecidable
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• Non-Horn clause logic programming without contrapositives
• SETHEO: A high-performance theorem prover
• Consolution as a framework for comparing calculi
• Controlled integration of the cut rule into connection tableau calculi
• Automated deduction by theory resolution
• Problem corner: Predicate logic hacker tricks
• Near-Horn Prolog and the ancestry family of procedures
• Model elimination without contrapositives
• The TPTP problem library
• Mechanical Theorem-Proving by Model Elimination