Resolution in Sorted Logic

With regard to improving the efficiency of automated deduction systems, the final word has not yet been spoken. In Chapter 8 we became acquainted with various techniques for pruning search spaces associated with deduction, most of which rely on restricting applications of the resolution and factorization rules. While such methods are indeed helpful in constructing more efficient resolution theorem provers, in fact some of the most promising techniques for increasing deduction efficiency have been based not on methods for restricting the application of deduction rules, but rather on modifications of the input calculi themselves. Two general tendencies in modifying calculi for efficiency are clearly discernible. The first is the development of special calculi for particular commonly occurring predicates. A classic example of this approach to improving deduction efficiency is the development of completion procedures—based on the Knuth-Bendix algorithm—for equational logic. The second tendency is that of using knowledge about special functions or predicates to arrive at more powerful unification algorithms. The fundamental idea behind this latter approach is to hand over the lion’s share of the deduction work to the (deterministic) unification mechanism, and so to reduce the computational burden placed on the (nondeterministic) logical inference system.