Negation as Failure, Completion and Stratification
John C. Shepherdson · Oxford University Press eBooks · 1998
The usual way of introducing negation into Horn clause logic programming is by ‘negation as failure’: if A is a ground atom . . . the goal ¬A succeeds if A fails the goal ¬A fails if A succeeds. . . . This is obviously not classical negation, at least not relative to the given program P; the fact that A fails from P does not mean that you can prove ¬A from P, e.g. if P is . . . a ← ¬b . . . then ? - b fails so, using negation as failure, ? – a succeeds, but a is not a logical consequence of P. You could deal with classical negation by using a form of resolution which gave a complete proof procedure for full first order logic. To a logician this would be the natural thing to do. Two reasons are commonly given for why this is not done. The first is that it is believed by most, but not all, practitioners, that this would be infeasible because it would lead to a combinatorial explosion, whereas negation as failure does not, since it is not introducing any radically new methods of inference, just turning the old ones round. The second is that, in practical logic programming, negation as failure is often more useful than classical negation. This is the case when the program is a database, e.g. an airline timetable. You list all the flights there are. If there is no listed flight from Zurich to London at 12.31, then you conclude that there is no such flight. The implicit use of negation as failure here saves us the enormous labour of listing all the non-existent flights. This implicit usage is made precise in the closed world assumption, one of the two commonest declarative semantics given for negation as failure. This was introduced by Reiter [1978] and formalises the idea that the database contains all the positive information about objects in the domain, that any positive ground literal which is not implied by the program is assumed to be false.