Computing answers with model elimination

Citations of this article
Mendeley users who have this article in their library.


We demonstrate that theorem provers using model elimination (ME) can be used as answer-complete interpreters for disjunctive logic programming. More specifically, we introduce a family of restart variants of model elimination, and we introduce a mechanism for computing answers. Building on this, we develop a new calculus called ancestry restart ME. This variant admits a more restrictive regularity restriction than restart ME, and, as a side-effect, it is in particular attractive for computing definite answers. The presented calculi can also be used successfully in the context of automated theorem proving. We demonstrate experimentally that it is more difficult to compute nontrivial answers to goals than to prove the existence of answers. © 1997 Elsevier Science B.V.




Baumgartner, P., Furbach, U., & Stolzenburg, F. (1997). Computing answers with model elimination. Artificial Intelligence, 90(1–2), 135–176.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free