A Useful Algebraic Property of Robinson's Unification Algorithm
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...
| Main Author: | |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/5906 |
| _version_ | 1826206757406375936 |
|---|---|
| author | Hart, Timothy |
| author_facet | Hart, Timothy |
| author_sort | Hart, Timothy |
| collection | MIT |
| 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}. |
| first_indexed | 2024-09-23T13:37:46Z |
| id | mit-1721.1/5906 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T13:37:46Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/59062019-04-10T17:24:10Z A Useful Algebraic Property of Robinson's Unification Algorithm Hart, Timothy 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}. 2004-10-04T14:08:53Z 2004-10-04T14:08:53Z 1965-11-01 AIM-091 http://hdl.handle.net/1721.1/5906 en_US AIM-091 5 p. 1889407 bytes 108227 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Hart, Timothy A Useful Algebraic Property of Robinson's Unification Algorithm |
| title | A Useful Algebraic Property of Robinson's Unification Algorithm |
| title_full | A Useful Algebraic Property of Robinson's Unification Algorithm |
| title_fullStr | A Useful Algebraic Property of Robinson's Unification Algorithm |
| title_full_unstemmed | A Useful Algebraic Property of Robinson's Unification Algorithm |
| title_short | A Useful Algebraic Property of Robinson's Unification Algorithm |
| title_sort | useful algebraic property of robinson s unification algorithm |
| url | http://hdl.handle.net/1721.1/5906 |
| work_keys_str_mv | AT harttimothy ausefulalgebraicpropertyofrobinsonsunificationalgorithm AT harttimothy usefulalgebraicpropertyofrobinsonsunificationalgorithm |