foundations of computational agents
Propositional logic has a long history; the semantics for propositional logic presented here is based on that of Tarski . For introductions to logic see Copi et al.  for an informal overview, Enderton  and Mendelson  for more formal approaches, and Bell and Machover  for advanced topics. For in-depth presentations on the use of logic in AI see the multivolume Handbook of Logic in Artificial Intelligence and Logic Programming [Gabbay et al., 1993].
Much of the foundation of definite and Horn clause reasoning was developed in the context of a richer first-order logic that is presented in Chapter 13 and is studied under the umbrella of logic programming. Resolution was developed by Robinson . SLD resolution was pioneered by Kowalski  and Colmerauer et al. , building on previous work by Green , Hayes , and Hewitt . The fixed point semantics was developed by van Emden and Kowalski . For more detail on the semantics and properties of logic programs see Lloyd .
The work on negation as failure is based on the work of Clark . Apt and Bol  provide a survey of different techniques and semantics for handling negation as failure. The bottom-up negation-as-failure proof procedure is based on the truth maintenance system (TMS) of Doyle , who also considered incremental addition and removal of clauses; see Exercise 15. The use of abnormality for default reasoning was advocated by McCarthy .
The abduction framework presented here is based on the assumption-based truth maintenance system (ATMS) of de Kleer  and on Theorist [Poole et al., 1987]. Abduction has been used for diagnosis [Peng and Reggia, 1990], natural language understanding [Hobbs et al., 1993], and temporal reasoning [Shanahan, 1989]. Kakas et al.  and Kakas and Denecker  review abductive reasoning. For an overview of the work of Peirce, who first characterized abduction, see Burch . The bottom-up Horn implementation for finding explanations is based on the ATMS [de Kleer, 1986]. The ATMS is more sophisticated in that it considers the problem of incremental addition of clauses and assumables also; see Exercise 16.