##
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