From "Logic Programming with Strong Negation" (David Pearce, Gerd Wagner, FU Berlin, 1991), appears in Springer LNAI 475: Extensions of Logic Programming, International Workshop Tübingen, FRG, December 8–10, 1989 Proceedings):
According to the standard view, a logic program is a set of definite Horn clauses. Thus, logic programs are regarded as syntactically restricted first-order theories within the framework of classical logic. Correspondingly, the proof theory of logic programs is considered as the specialized version of classical resolution, known as SLD-resolution. This view, however, neglects the fact that a program clause, a_0 <— a_1, a_2, • • •, a_n, is an expression of a fragment of positive logic (a subsystem of intuitionistic logic) rather than an implicational formula of classical logic. The classical interpretation of logic programs, therefore, seems to be a semantical overkill.
It should be clear that in order to explain the deduction mechanism of Prolog one does not have to refer to the indirect method of SLD-resolution which checks for the refutability of the contrary. It is certainly more natural to view Prolog's proof procedure as a kind of natural deduction, as, for example, in [Hallnäs & Schroeder-Heister 1987] and [Miller 1989]. This also is more in line with the intuitions of a Prolog programmer. Since Prolog is the paradigm, logic programming semantics should take it as a point of departure.
See also: Logic programming with strong negation and inexact predicates (1991), where we read:
Akama [S.Akama (1987): Resolution in constructivism, Logique et Analyse, 120, 385-392] proposed to use constructive logic for the interpretation of logic programming. He showed how the resolution calculus for definite Horn clauses can be interpreted within constructive logic. In fact, he makes the point that in the definite Horn clause setting the differences between strong negation, intuitionistic negation and classical negation do not matter. We remark that this observation is not surprising since the language of definite Horn clauses can be viewed as a fragment of positive logic which forms a common subpart of constructive, intuitionistic and classical logic.
Further afield, an interesting note from Answer Set Programming’s Contributions to Classical Logic (appears in Springer LNAI6565, 2011):
Integrating classical logic and ASP is not a trivial task, as research on rule languages for the semantic web is now also discovering [J. Pührer, S. Heymans, and T. Eiter. Dealing with inconsistency when combining ontologies and rules using dl-programs]. Expanding the stable semantics to the syntax of FO (classical first-order logic) as in [P. Ferraris, J. Lee, and V. Lifschitz. A new perspective on stable models] is obviously redefining FO, not integrating ASP and FO. Among subtle problems and tricky mismatches, one glaring difference clearly stands out: ASP uses the answer set as its basic semantic construct, whereas FO of course uses interpretations (or structures). There is a profound difference between the two concepts. As defined in [M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases], an answer set is a set of literals that represents a possible state of belief that a rational agent might derive from the logic program. In other words, an answer set is subjective; it does not talk directly about the world itself, but only about the beliefs of an agent about this world. This conception of answer sets is not a philosophical afterthought, but is tightly connected with the view of negation as failure as a modal, epistemic or default operator, and therefore truly lies at the heart of ASP. By contrast, FO has a possible world semantics, in which each model of a theory represents a state of the world that is possible according to this theory. In other words, FO is concerned with objective forms of knowledge, that do not involve propositional attitudes such as the belief or knowledge of an epistemic agent, etc. Modal extensions of classical logic that can express such forms of subjective knowledge typically use Kripke structures (or the special case of sets of possible worlds) as a semantic object.
Going all philosophical, I am unsure about the difference made above. A logic never talks about "the world itself" unless it is all facts or the world can be directly mapped to the objects subject of the logic (e.g. number theory, or the objects of a Herbrand basis). Any derivation performed is necessarily "just" the agent's belief otherwise.