Negation in logic and deductive databases

This thesis studies negation in logic and deductive databases. Among other things, two kinds of negation are discussed in detail: strong negation and nonmonotonic negation.

In the logic part, we have constructed a first-order logic CF 0 of strong negation with bounded quantifiers. The logic is based on constructive logics, in particular, Thomason's logic CF. However, unlike constructive logic, quantifiers in our system as in Thomason's are static rather than dynamic. For the logic CF 0 , the usual Kripke formal semantics is defined but based on situations instead of conventional possible worlds. A sound and complete axiomatic system of CF 0 is established based on the axiomatic systems of constructive logics with strong negation and Thomason's completeness proof techniques. CF 0 is proposed as the underlying logic for situation theory. Thus the connection between CF 0 and infon logic is briefly discussed.

In the database part, based on the study of some main existing semantic theories for logic programs with nonmonotonic negation, we have defined a novel semantics of logic programs called quasi-stable semantics. An important observation is that a nonmonotonic negation such as is required for logic programs should be computed by a nonmonotonic, revision process. Only a process that allows one to withdraw by revising provisionally held negative information can hope to be adequate to model a non-monotonic negation. In light of this, we propose a model of negation that owes much to the stable semantics but allows, through a mechanism of consistency- recovery, for just this withdrawal of previously assumed negative information. It has been proved that our new semantics maintains the desired features of both the well-founded semantics and the stable model semantics while overcoming their shortcomings. In addition, the quasi-stable semantics has been generalised to logic programs with both strong negation and nonmonotonic negation, giving rise to the quasi-answer set semantics.