Embedding negation as failure into a model generation theorem prover

Here, for the first time, we give an implementation which computes answer sets of every class of (function-free) logic programs and deductive databases containing both negation as failure and classical negation. The proposal is based on bottom-up, incremental, backtrack-free computation of the minimal models of positive disjunctive programs, together with integrity constraints over beliefs and disbeliefs. Our translation method not only provides a simple fixpoint characterization of answer sets, but also is very helpful to understand under what conditions each model is “stable” or “unstable”. The procedure has been implemented on top of the model generation theorem prover MGTP on a parallel inference machine, and has been applied to a legal reasoning system.