Logic programming is proof search for some logic. Traditionally, this is the Horn clause fragment of first-order logic. Languages like lambdaProlog extend this to (intuitionistic) hereditary Harrop formulas. There are also languages like Lolli, LolliMon, and Olli that work in fragments of linear logic (ordered linear logic in the last case). The concepts here are the notion of uniform proofs, focused proofs, and polarization, which lead to the concept of an abstract logic programming language.
The other way of thinking about logic programming that is more common via the Datalog path is as finite model theory. The idea there is simple: just calculate what the model would be, i.e. literally the sets of tuples for each relation. For Datalog (with or without stratified negation), this is relatively simple; there is a single minimal model.
When non-stratified negation is allowed, the situation gets quite a bit more complex. There is no longer a unique minimal model. There are two ways of dealing with this situation. One is to move to 3-valued models and for things like $q\leftarrow\neg q$ we can assign the truth-value $U$ to $q$ representing an "undefined" third truth-value. This leads to well-founded semantics. Given this 3-valued model, we can create a set of 2-valued models by considering all ways of assigning $T$ or $F$ to the "undefined" tuples excluding models with unfounded propositions which gives stable model semantics. The recent paper Founded Semantics and Constraint Semantics of Logic Rules gives a nice way of generalizing, organizing, and understanding these various semantics and the details of what "unfounded" means. Answer set programming is often conceptualized as stable model semantics. The XSB implementation of tabled logic programming is capable of handling non-stratified negation and producing a well-founded semantics which can then be fed into an answer set programming system leading to a significant performance gain over directly applying answer set programming.
Returning to proof search, what's happening in answer set programming can be partially thought of with respect to disjunctive logic programming. Typical logic programming languages do not allow disjunction in the head. That is, you can't prove $p\lor q$ except by proving $p$ or $q$. The issue is clear. Given the (disjunctive) logic program $p\lor q.$, should $?{-}\,p$ succeed or not? More pointedly, what should be produced by $?{-}\,t(X)$ where $t(1)\leftarrow p\land\neg q. t(2)\leftarrow q\land\neg p.$ is appended to the earlier program? Finally, append $r\leftarrow t(1)\land t(2).$ and ask if $?{-}\,r$ holds. These examples illustrate that while we can find a model where $t(1)$ holds and a model where $t(2)$ holds, there's no model where both $t(1)$ and $t(2)$ hold. This can be related to the previous paragraph by noting the classical equivalence $p\lor q \equiv p \leftarrow \neg q$. In particular, the program $p\leftarrow\neg q. q\leftarrow\neg p.$ leads to both $p$ and $q$ being "undefined" in well-founded semantics and has two stable models, though this omits the model where both $p$ and $q$ hold. (One way to see why this happens is that there are implicitly completion rules that make the program look like $(p\leftrightarrow\neg q)\land(q\leftrightarrow\neg p)$.) In terms of proof search, there's simply no proof of $p$ from $p\lor q$. Via the soundness and completeness theorems of (classical) first-order logic, having a proof of some formula is equivalent to having it hold in all models. Answer set programming just enumerates the (stable) models. To see if answer set programming has proven something, you need to check to see if it's true in all the models the answer set program produces. Normal logic programming implicitly constructs a proof, so it can only talk about what holds in all models.
Finally, pure logic programming meaning logic programming omitting extra-logical features like cut (!), assert, retract, and others, is, as I said at the beginning, purely a matter of proof search. It does not "assert new facts and knowledge". It is the process of "discover[ing] consquences that are implicit in the initial premises". Most logic programming languages are restricted to a fragment of logic where this process is particularly amenable to computation. Indeed, they are often restricted to satisfy a much more stringent notion of "monotonicity" as is especially evident in Datalog. Datalog is usually implemented via forward chaining, which means starting from what is known and producing all immediate consequences. This is iterated until a fixed point is found. Monotonicity in this context means that once something is derived, you can never learn something later that will change your mind. Non-stratified uses of negation lead to non-monotonicity. For example, for the program $p\leftarrow\neg q. q\leftarrow\neg p.$, initially neither $p$ nor $q$ is true thus we may feel justified in deriving either or both of $p$ and $q$. If we pick both, then we scuttle our justification for picking either. Whichever we pick, we end up with a statement that isn't true in all models. Of course, in general there can be an arbitrary long chain of logic before we realize we're in this situation at which point we'll have already derived a bunch of things we should not have.
