Propositional logic has a long history; the semantics for propositional logic presented here is based on that of Tarski [1956].

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 15 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 5.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]. Kakas and Denecker [2002] review abductive reasoning. For an overview of the work of Peirce, who first characterized abduction, see Burch [2022]. The bottom-up Horn implementation for the ATMS is more sophisticated in that it considers the problem of incremental addition of clauses and assumables also; see Exercise 5.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]. See also Chapter 11.

The FDIV bug and the development of formal hardware verification at Intel is covered by Seger [2021]. Xu et al. [2008] and Biere et al. [2021] cover SAT, modern SAT solvers, and the applications for hardware and software verification. Sundermann et al. [2021] surveys product configuration using SAT. The application of formal methods to the Mercedes product lines is described by Sinz et al. [2003]. The TLA$+$ system is described by Lamport [2002] and Kuppe et al. [2019].