6.1 Chapter 6 notes

Chapter 6 covers some basic material regarding mathematical and computational logic. The contents of this chapter were used as notes for part of a theoretical computer science course on automated reasoning at the masters level from about 1995 until about 2001. It was assumed that the student had at least one background course in logic, with at least an informal introduction to symbolic logic.

Section 6.2 covers positive logic. Positive rulebases and goals are defined. The topics covered include the Herbrand universe for a rulebase, answer substitutions, interpretations and models, answers, minimal model, rule trees, Prolog computation, and extraction of proofs as rule trees. The material in this section is a good company for the material in the popular book Foundations of Logic Programming by J.W. Lloyd (1984,1987).

Section 6.3 develops a nice Prolog translator from first-order logic into normal form logic rules. The normal form rules serve as inputs to a normal form reasoning program in section 6.4.

Section 6.4 develops an interesting normal rulebase query interpreter for linear disjunctive logic. The semantics for normal rulebases is based upon states and rule trees. Rule trees were introduced in a simpler setting in Section 6.2, for positive rulebases. The design and implementation of a normal rulebase query interpreter is developed in Prolog.

Section 6.5 discusses some of the issues regarding soundness and completeness of the normal rulebase interpreter developed in Section 6.4. The use of a tabeled Prolog (such as XSB Prolog) is discussed briefly.

Section 6.6 presents a Java visualization tool for displaying the ruletrees generated by the normal rulebase interpreter of Section 6.4. Other material regarding visual logic, including Luu Tran's thesis (c.1996), can be found by clicking here (opens in separate window). {The link is no longer active.}

Recently (c. 2005), finitary geometric logic (aka coherent logic) seems to be an interesting alternative to linear disjunctive logic. Please see Geolog and Skolem Machines for some web notes focusing on Prolog implementations of geometric logic (opens in separate window).

Prolog Tutorial Contents