Using the Davis and Putnam Procedure for an Efficient Computation of Preferred Models.
Thierry Castell, Claudette Cayrol, Michel Cayrol, Daniel Le Berre · 1996
Some famous problems (ATMS inference, Closed World Reasoning (CWR) for instance) can be replaced by a problem of preferred model computation. We thus propose a preference relation between models based on a preference relation between literals and an "efficient" algorithm to compute the associated preferred models of a theory. Then, we apply this algorithm to ATMS inference and problems of CWR. Sub-problems like subsumption and label computation [7][8] are thus implicitly solved.