Name
Abstract | ||
|---|---|---|
We present a framework for solving a system of equations and disequations that allow to determine, upon unsolvability, the “cause” of the failure, i.e. the minimal unsolvable subsets of equations and disequations responsible of it.Solving equations in the algebra of term is well-known as unification. However if usual unification algorithms are apt to give a unifier when the set is unifiable they don't give any pertinent information when the set in not unifiable. An interesting problem is to determine, in case of unsolvability (minimal) unsolvable subsets cause of the failure of the whole set, i.e. isolate the equations that lead to failure. An immediate application of such an enhanced unification algorithm is in so called intelligent backtracking methods in resolution-based systems, see for instance [Cod 88]. Consider that the set of equations to solve corresponds to the current substitution of a proof method based on the Resolution principle, eg. Logic Programming or most automated theorem provers. Then each equation is associated to a (possible) choice-point in the proof and determining the unsolvable subsets corresponds to isolate pertinent choice-points where it is useful to backtrack to from useless choice-points. This avoids useless deduction/backtracking steps.Recently several authors have been interesting in not only solving sets of equations but also sets of equations and disequations. Colmerauer [Col 84], motivated by the introduction of inequations in Prolog-II, was the first to propose an algorithm to extend his unification algorithm for handling disequations. [Kir 87] presents a set of transformation rules to solve equational problems consisting in a disjunction of conjunctions of equations or disequations with existentially and universally quantified variables. [Com 89] extends this work and gives completness results for transformation rules. This framework clearly separates the control part of the algorithm and encompases a large class of algorithms. As we will restrict ourselves to sets of equations and disequations (i.e. conjunctions), we will use the basic results of [Col 84].Our approach is based on the representation of a set of equations by a unification graph that contain the complete “history” of the unification process, i.e. of variables bindings. This graph represents the solution of the system if it is solvable and allows to easily compute unsolvable subsets (“causes” of the unification failure) in case of failure. This unification graph is formally detailed in [Cod 88], and a simplified version of our algorithm has been implemented as the basis of intelligent backtracking in a Prolog compiler. This system has a low overhead (30%) w.r.t. standard Prolog unification and gives substantial speedups (from 2 to 20) on non-deterministic programs, see once more [Cod 88]. In our approach the unification process consists in the non-deterministic transformation, by two simple derivation rules, of a unification graph corresponding to the initial set of equation to a final irreductible graph corresponding to a solved form. The “cause” of a derived equation can be simply computed by following generalized paths in the graph, and this information is used in case of unsolvability for determining the minimal unsolvable subsets. We then extend our algorithm for dealing with disequations along the lines of [Col 84] and see how unsolvable subsets can also be easily computed thanks to the unification graph for failures due to inequations.See [Cod 90] for a full treatment of our framework. |
Year | DOI | Venue |
|---|---|---|
1990 | 10.1145/96877.96956 | ISSAC |
Keywords | Field | DocType |
unification algorithm,usual unification algorithm,enhanced unification algorithm,transformation rule,minimal unsolvable subsets,unification failure,unification graph,standard prolog unification,unsolvable subsets,unification process,theorem prover,col,system of equations | Discrete mathematics,Combinatorics,Equation solving,System of linear equations,Algebra,Computer science,Unification,Compiler,Prolog,Differentiation rules,Logic programming,Backtracking | Conference |
ISBN | Citations | PageRank |
0-201-54892-5 | 0 | 0.34 |
References | Authors | |
0 | 1 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| P. Codognet | 1 | 17 | 1.76 |