Anti-Unification in Constraint Logics: Foundations and Applications to Learnability in First-Order Logic, to Speed-Up Learning, and to Deduction

Abstract

Unification is central to automated reasoning. Unification comes in a variety of forms, all of which compute (roughly stated) the greatest lower bound, or all maximal lower bounds, of any two or more syntactic objects in a partially-ordered set of such objects. The dual of unification is an operation called generalization, or anti-unification, which computes least or minimal upper bounds. As with unification, anti-unification comes in a variety of forms. The thesis of this dissertation is: anti-unification in its various forms is, like unification, a powerful tool for automated reasoning. In defense of the thesis, several forms of anti-unification in constraint logic, anti-unification relative to background information, are defined, and their semantic and computational properties are studied. It is shown that these forms of anti-unification are applicable to inductive logic programming (inductive learning of logic programs), speed-up learning, and knowledge base vivification (an approach to efficient deduction).