Computing answers with model elimination

Abstract

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.