
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.
term reduction system, rewrite rules, unification algorithm, logic program, external functional procedures, General topics in the theory of software, Theorem proving (deduction, resolution, etc.), Horn clause logic
term reduction system, rewrite rules, unification algorithm, logic program, external functional procedures, General topics in the theory of software, Theorem proving (deduction, resolution, etc.), Horn clause logic
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 2 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
