Mechanical Theorem Proving and Artificial Intelligence Languages.

摘要

This dissertation is principally concerned with incompleteness issues in the design of artificial intelligence languages. Major sources of incompleteness are the pattern matching and inference facilities of the languages. Incompleteness in the area of pattern matching can be repaired by developing unification algorithms for the specialized data types of the languages. A complete, but potentially infinite unification process is described for arbitrary data types in general and is applied to the QA4/QLISP vector, bag, and class data types. Finite, complete unification algorithms are also described for the bag and class data types. The bag unification algorithm is extended to the case of unification of first order predicate calculus terms with functions which are both associative and commutative. Incompleteness in the area of the inference system can be repaired by use of some form of the pi inference procedure which is a complete extension derived from model elimination of the problem reduction method. This can readily be accomplished in present or new artificial intelligence languages by attempting to derive all goals in the context of the asserted negations of all higher goals.