Thumbnail
Access Restriction
Subscribed

Author Buntine, Wray L. ♦ Brckert, Hans-Jrgen
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Copyright Year ©1994
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword E-disunification ♦ E-unification equational theory ♦ Definite clause ♦ Inequations ♦ Logic programming ♦ Solving equations and disequations
Abstract We are interested in the problem of solving a system<si=ti:1≤i≤n,pj≠qj:1≤j≤m><?Pub Caret>. Solutions to disunification problems are substitutions for the variables of the problem that make the two terms of each equation equal, but leave those of the disequations different. We investigate this in both algebraic and logical contexts where equality is defined by an equational theory and more generally by a definitive clause equality theory E. We show how E-disunification can be reduced to E-unification, that is, solving equations only, and give a disunification algorithm for theories given a unification algorithm. In fact, this result shows that for theories in which the solutions of all unification problems can also be represented finitely. We sketch how disunification can be applied to handle negation in logic programming with equality in a similar style to Colmerauer's logic programming with rational trees, and to represent many solutions to AC-unification problems by a few solutions to ACI-disunification problems.
ISSN 00045411
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 1994-07-01
Publisher Place New York
e-ISSN 1557735X
Journal Journal of the ACM (JACM)
Volume Number 41
Issue Number 4
Page Count 39
Starting Page 591
Ending Page 629


Open content in new tab

   Open content in new tab
Source: ACM Digital Library