A Useful Algebraic Property of Robinson's Unification Algorithm

dc.creator	Hart, Timothy
dc.date	2004-10-04T14:08:53Z
dc.date	2004-10-04T14:08:53Z
dc.date	1965-11-01
dc.date.accessioned	2013-10-09T02:41:54Z
dc.date.available	2013-10-09T02:41:54Z
dc.date.issued	2013-10-09
dc.identifier	AIM-091
dc.identifier	http://hdl.handle.net/1721.1/5906
dc.identifier.uri	http://koha.mediu.edu.my:8181/xmlui/handle/1721
dc.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}.
dc.format	5 p.
dc.format	1889407 bytes
dc.format	108227 bytes
dc.format	application/postscript
dc.format	application/pdf
dc.language	en_US
dc.relation	AIM-091
dc.title	A Useful Algebraic Property of Robinson's Unification Algorithm

Files in this item

Files	Size	Format	View
There are no files associated with this item.