[1] That a particular method of inference is legitimate is not a trivial assertion. One must prove that if one starts with true premises, only true conclusions can be derived. The method of inference represented by rule applications is modus ponens, the familiar method of inference that says that if A is true and A implies B is true, then we may conclude that B is true.
[2] We must qualify this statement by agreeing that, in speaking of the inference accomplished by a logic program, we assume that the computation terminates. Unfortunately, even this qualified statement is false for our implementation of the query language (and also false for programs in Prolog and most other current logic programming languages) because of our use of not and javascript_value. As we will describe below, the not implemented in the query language is not always consistent with the not of mathematical logic, and javascript_value introduces additional complications. We could implement a language consistent with mathematical logic by simply removing not and javascript_value from the language and agreeing to write programs using only simple queries, and, and or. However, this would greatly restrict the expressive power of the language. One of the major concerns of research in logic programming is to find ways to achieve more consistency with mathematical logic without unduly sacrificing expressive power.
[3] This is not a problem of the logic but one of the procedural interpretation of the logic provided by our interpreter. We could write an interpreter that would not fall into a loop here. For example, we could enumerate all the proofs derivable from our assertions and our rules in a breadth-first rather than a depth-first order. However, such a system makes it more difficult to take advantage of the order of deductions in our programs. One attempt to build sophisticated control into such a program is described in deKleer et al. 1977. Another technique, which does not lead to such serious control problems, is to put in special knowledge, such as detectors for particular kinds of loops (exercise 4.58). However, there can be no general scheme for reliably preventing a system from going down infinite paths in performing deductions. Imagine a diabolical rule of the form To show $P(x)$ is true, show that $P(f(x))$ is true, for some suitably chosen function $f$.
[4] Consider the query not(baseball_fan(list("Bitdiddle", "Ben"))). The system finds that baseball_fan(list("Bitdiddle", "Ben")) is not in the data base, so the empty frame does not satisfy the pattern and is not filtered out of the initial stream of frames. The result of the query is thus the empty frame, which is used to instantiate the input query to produce not(baseball_fan(list("Bitdiddle", "Ben"))).
[5] A discussion and justification of this treatment of not can be found in the article by Clark (1978).
4.4.3 Is Logic Programming Mathematical Logic?