We introduce and discuss a number of refinements for restart model elimination (RME). Most of these refinements are motivated by the use of RME as an interpreter for disjunctive logic programming. Especially head selection function, computation rule, strictness and independence of the goal clause are motivated by aiming at a procedural interpretation of clauses. Other refinements like regularity and early cancellation pruning are techniques to handle the tremendous search space. We discuss these techniques and investigate their compatibility. As a new result we give a proof of completeness for RME with early cancellation pruning; we furthermore show that this powerful refinement is compatibel with regularity tests.

Das Jahrestreffen 1997 der GI-Fachgruppe 1.2.1 `Deduktionssysteme' --- besser bekannt als `Deduktionstreffen' --- fand vom 30.9. bis 2.10. 1997 in Schloss Dagstuhl statt. Die Organisation wurde dieses Jahr von der KI-Gruppe an der Universität Koblenz-Landau (Leitung Prof. Furbach) übernommen.

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.

In [?] a very efficient system for solving diagnosis tasks has been described, which is based on belief revision procedures and uses first order logic system descriptions. In this paper we demonstrate how such a system can be rigorously formalized from the viewpoint of deduction by using the calculus of hyper tableaux [?]. The benefits of this approach are twofold: first, it gives us a clear logical description of the diagnosis task to be solved; second, as our experiments show, the approach is feasible in practice and thus serves as an example of a successful application of deduction techniques to real-world applications.

In this paper we demonstrate how general purpose automated theorem proving techniques can be used to solve realistic model-based diagnosis problems. For this we modify a model generating tableau calculus such that a model of a correctly behaving device can be used to guide the search for minimal diagnoses. Our experiments show that our general approach is competitive with specialized diagnosis systems.

We introduce a bottom-up and a top-down calculus for disjunctive logic programming (DLP). The bottom-up calculus, hyper tableaux, is depicted in its ground version and its relation to fixed point approaches from the literature is investigated. The top-down calculus, restart model elimination (RME), is presented as a sound and complete answer-computing mechanism for DLPs, and its relation to hyper tableaux is discussed.
In two aspect this represents an extension of SLD-resolution for Horn clause logic programming: RME is SLD-resolution when restricted to Horn clauses, and it has a direct counterpart to the immediate consequence operator for Horn clauses. Furthermore we discuss, that hyper tableaux can be seen as an extension of SLO-resolution.

In this paper, we show how techniques from disjunctive logic programming and classical first-order theorem proving can be used for efficient (deductive) database updates. The key idea is to tranform the given database together with the update request into a disjunctive logic program and apply disjunctive techniques (such as minimal model reasoning) to solve the original update problem. We present two variants of our algorithm both of which are of polynomial space complexity. One variant, which is based on offline preprocessing, is of polynomial time complexity. We also show that both variants are rational in the sense that they satisfy certain rationality postulates stemming from philosophical works on belief dynamics.

The Model Elimination (ME) calculus is a refutationally complete, goal-oriented calculus for first-order clause logic. In this paper, we introduce a new variant called disjunctive positive ME (DPME); it improves on Plaisted's positive refinement of ME in that reduction steps are allowed only with positive literals stemming from clauses having at least two positive literals (so-called disjunctive clauses).

DPME is motivated by its application to various kinds of subsumption deletion: in order to apply subsumption deletion in ME equally successful as in Resolution, it is crucial to employ a version of ME which minimizes ancestor context (i.e. the necessary A-literals to find a refutation). DPME meets this demand. We describe several variants of ME with subsumption, with the most important ones being ME with backward and forward subsumption and the T^*-Context Check. We compare their pruning power, also taking into consideration the well-known regularity restriction.

All proofs are supplied. The practicability of our approach is demonstrated with experiments.

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 non-trivial answers to goals than to prove the existence of answers.