COMPUTING ANSWERS WITH MODEL ELIMINATION

We demonstrate that theorem provers using model elimination (ME) can b e used as answer-complete interpreters for disjunctive logic programmi ng. More specifically, we introduce a family of restart variants of mo del elimination, and we introduce a mechanism for computing answers. B uilding on this, we develop a new calculus called ancestry restart ME. This variant admits a more restrictive regularity restriction than re start ME, and, as a side-effect, it is in particular attractive for co mputing definite answers. The presented calculi can also be used succe ssfully in the context of automated theorem proving. We demonstrate ex perimentally that it is more difficult to compute nontrivial answers t o goals than to prove the existence of answers. (C) 1997 Elsevier Scie nce B.V.