Model Elimination, Logic Programming and Computing Answers

Abstract

. We prove that theorem provers using model elimination (ME) can be used as answer complete interpreters for disjunctive logic programming. For this, the restart variant of ME with a mechanism for computing answers and the ancestry refinement is introduced. Furthermore, we demonstrate that in the context of automated theorem proving it is much more difficult to compute (non-trivial) answers to goals, instead of only proving the existence of answers. It holds that resolution with subsumption is not answer complete. We consider puzzle examples and give a comparative study of OTTER, SETHEO and our restart model elimination prover PROTEIN. Keywords. Automated reasoning; theorem proving; model elimination; logic programming; computing answers. The aim of this paper is twofold: Firstly, we prove that theorem provers using model elimination (ME) can be used as answer complete interpreters for disjunctive logic programming. Secondly, we demonstrate that in the context of automated theorem p...