Propositional logic has a long history; the semantics for propositional logic presented here is based on that of Tarski [1956]. For introductions to logic see Copi et al. [2016] for an informal overview, Enderton [1972] and Mendelson [1987] for more formal approaches, and Bell and Machover [1977] 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].

The DPLL algorithm is by Davis et al. [1962]. Levesque [1984] describes the tell-ask protocol for knowledge bases. Consistency-based diagnosis was formalized by de Kleer et al. [1992].

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 [1965]. SLD resolution was pioneered by Kowalski [1974] and Colmerauer et al. [1973], building on previous work by Green [1969], Hayes [1973], and Hewitt [1969]. The fixed point semantics was developed by van Emden and Kowalski [1976]. For more detail on the semantics and properties of logic programs see Lloyd [1987].

The work on negation as failure is based on the work of Clark [1978]. Apt and Bol [1994] 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 [1979], who also considered incremental addition and removal of clauses; see Exercise 15. The use of abnormality for default reasoning was advocated by McCarthy [1986].

The abduction framework presented here is based on the assumption-based truth maintenance system (ATMS) of de Kleer [1986] 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. [1993] and Kakas and Denecker [2002] review abductive reasoning. For an overview of the work of Peirce, who first characterized abduction, see Burch [2008]. 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.

Dung [1995] presents an abstract framework for arguments that provides a foundation for much of the work in this area. Chesnevar et al. [2000] and Besnard and Hunter [2008] survey work on arguments.

Causal models are discussed by Pearl [2009] and Spirtes et al. [2001].