Please use this identifier to cite or link to this item:
http://dspace.mediu.edu.my:8181/xmlui/handle/1721.1/5906| Title: | A Useful Algebraic Property of Robinson's Unification Algorithm |
| Issue Date: | 9-Oct-2013 |
| Description: | This memo presupposes some acquaintance with "A Machine Oriented Logic Based on the Resolution Principle", J.A. Robinson, JACM Jan65. The reader unfamiliar with this paper should be able to get a general idea of the theorem if he knows that OA is a post operator indicating a minimal set of substitutions (most general substitution) necessary to transform all elements of the set of formulae, A, into the same element (to "unify" A), so that when OA exists AOA is a set with one element (a "unit"). Example: A={f(x),y f(g(u)), f(g(z))} UA= {g(u)/x, f(g(u))/y, u/z} AOA= {f(g(u))} Another most general unifier of A is {g(z)/x, f(g(z))/y, z/u}. |
| URI: | http://koha.mediu.edu.my:8181/xmlui/handle/1721 |
| Other Identifiers: | AIM-091 http://hdl.handle.net/1721.1/5906 |
| Appears in Collections: | MIT Items |
Files in This Item:
There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.