Anti-unification in constraint logics: foundations and applications to learnability in first-order logic, to speed-up learning, and to deduction
Jr. Charles David Page · Illinois Digital Environment for Access to Learning and Scholarship (University of Illinois at Urbana-Champaign) · 1993
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).