Case Study: Other Ways of Thinking - Thinking as Computation - page 265

Observe that the only thing that prevents representing all the given facts as a set of
clauses in Prolog (and using normal back-chaining) is the fact about the bottom block
not being green. But to handle this negative fact properly and to fully use what is
known requires thinking in this new advanced way.
Want to read more?
This chapter explored ways of thinking that went beyond simple back-chaining.
Remarkably enough, these new ways of thinking were all formulated in terms of
back-chaining.
The idea of using a programming language to write a language processor for that
very language (a meta-interpreter ) is a practice developed to a fine art in the LISP
community [53], which uses this idea in a number of ways, including adding new
primitive constructs to the language. In this chapter it was used to explore variants
of the Prolog processor and to handle abduction and induction by making temporary
additions to the underlying knowledge base.
The section on explanation took a first glance at an area of research called abductive
logic programming (for example, see [54]). The section on learning introduced the area
of inductive logic programming (for example, see [56]). These two continue to be active
areas of research, although techniques more closely allied with probability theory
have gradually come to dominate the study of both diagnosis and learning.
The section on propositional reasoning is perhaps the most open-ended part of the
book. Its generalization of clauses to dclauses allowed representing a much wider
range of knowledge, in particular, incomplete knowledge , when certain facts must be
considered even though their truth is unknown (like the guilt of Alice). When vari-
ables and a few other features are included, the resulting first-order logic is the typical
starting point for logical reasoning within AI, for example in [4].
Computing satisfiability (for CNF formulas without variables) has become an active
area of AI research. It turns out that many of the problems considered in this topic
(including constraint satisfaction and planning) can be reformulated directly in terms
of satisfiability. This is significant because there have been great advances in recent
programs that compute satisfiability [55].
Computing unsatisfiability (for CNF formulas with variables) is also an active area
of research called automated theorem-proving [57]. The emphasis is on taking (small)
parts of mathematics, formalizing them as a set of axioms in a first-order logic, and