Logic programming with external procedures: Introducing S-unification (Q1097682)

A motivation for this work is the problem of re-usability of existing traditional software in logic programs. It can be viewed in an abstract way as the problem of amalgamation of Horn clause logic with a term reduction system whose rewrite rules are not accessible and thus cannot be used for construction of E-unifiers. Therefore, we introduce a new unification algorithm, called S-unification, which is a special incomplete case of E-unification. It has the property that whenever it succeeds, the result is a singleton complete set of E-unifiers of the arguments. It may also fail or report that it is not able to solve the problem of E-unification for given arguments. If the algorithm fails, the actual arguments have no E-unifier. The paper discusses the problem of amalgamation of external functional procedures in a logic program and gives a characterization of a class of amalgamated programs for which S- unification is complete.