J Strother Moore

Abstract: I will present some of the basic ideas behind the most commonly
used "uniform proof procedure", namely resolution.  Resolution is a
semi-complete procedure for first-order predicate calculus.  The basic idea
is to remove quantifiers with Skolemization, convert the axioms and the
negation of the challenge into clausal (conjunctive normal) form, and apply
the resolution principle in all possible ways to try to derive a
contradiction.  I will discuss unification, the representation of clauses,
and some restrictions on the search strategy that maintain completeness.
I will be more focused on implementation issues than theoretical issues.