MIXED-INTEGER PROGRAMMING METHODS FOR COMPUTING NONMONOTONIC DEDUCTIVE DATABASES

Though the declarative semantics of both explicit and nonmonotonic neg ation in logic programs has been studied extensively, relatively littl e work has been done on computation and implementation of these semant ics. In this paper, we study three different approaches to computing s table models of logic programs based on mixed integer linear programmi ng methods for automated deduction introduced by R. Jeroslow. We subse quently discuss the relative efficiency of these algorithms. The resul ts of experiments with a prototype compiler implemented by us tend to confirm our theoretical discussion. In contrast to resolution, the mix ed integer programming methodology is both fully declarative and handl es reuse of old computations gracefully. We also introduce, compare, i mplement, and experiment with linear constraints corresponding to four semantics for ''explicit'' negation in logic programs: the four-value d annotated semantics [Blair and Subrahmanian 1989], the Gelfond-Lifsc hitz semantics [1990], the over-determined models [Grant and Subrahman ian 1990], and the classical logic semantics. Gelfond and Lifschitz [1 990] argue for simultaneous use of two modes of negation in logic prog rams, ''classical'' and ''nonmonotonic,'' so we give algorithms for co mputing ''answer sets'' for such logic programs too.