(به : ) یا در و ، یک فرایند الگوریتمی برای بین است.
 بر اساس آنکه کدام عبارات (که ترم نامیده می‌شوند) اجازه رخداد در مجموعه معادلات را دارد (که مسئله همان‌سازی نام دارد)، و نیز بر اساس آنکه کدام عبارات‌ها معادل درنظر گرفته می‌شوند، چارچوب‌های همان‌سازی از هم متمایز می‌شوند. اگر متغیرهای سطح بالا، یعنی متغیرهایی که نمایش‌دهنده هستند، امکان وجود در یک عبارت را داشته باشد، به این فرایند می‌گویند، در غیر این صورت به آن می‌گویند. اگر به وجود راه‌حلی برای همان‌سازی لیترالی هر دو طرف هر معادله نیاز باشد، به این فرایند یا می‌گویند، در غیر این صورت به آن ، ، یا یا می‌گویند.
 راه‌حل‌های مسئله همان‌سازی توسط « » نشان داده می‌شوند، که «جایگزینی» یک نگاشت است که یک مقدار نمادین را به هر متغیر در عبارت‌های مسئله انتساب می‌دهد. یک الگوریتم همان‌سازی باید برای یک مسئله معین یک مجموعه جایگزینی « و » محاسبه کند، یعنی این مجموعه همه جواب‌ها را پوشش دهد، و نیز شامل هیچ عضو زایدی هم نیست. بر اساس چارچوب مسئله، یک «مجموعه جایگزینی کامل و کمینه» می‌تواند تعداد اعضایش حداکثر یک، حداکثر تعداد متناهی، یا احتمالاً تعداد بی‌نهایتی عضو داشته باشد، یا ممکن است اصلاً عضوی نداشته باشد. در بعضی از چارچوب‌ها معمولاً غیرممکن است که در مورد وجود راه‌حل تصمیم‌گیری کرد. برای همان‌سازی نحوی سطح اول، مارتلی و مانتناری یک الگوریتم ارائه دادند که قابل حل نبودن را گزارش کند، یا در غیر اینصورت یک مجموعه جایگزینی منفرد کمینه و کامل را محاسبه می‌کند، که شامل است.
 برای مثال، اگر , , متغیر باشند، مجموعه عبارت منفرد یک مسئله همان‌سازی سطح اول نحوی است، که تنها راه‌حل‌اش جایگزینی است. مسئله همان‌سازی سطح اول نحوی در مجموعه ترم‌های متناهی هیچ راه‌حلی ندارد. با این حال، راه‌حل منفرد را در مجموعه دارد. مسئله همان‌سازی سطح اول معنایی دارای جایگزینی با فرم است، که یک راه‌حل در است، یعنی اگر (.) درنظرگرفته شود، مسئله مشابهی در دیده می‌شود، که در آن (.) جابه‌جایی‌پذیر موقعی است، که هر جایگزینی اصلاً یک راه‌حل نباشد. مجموعه منفرد یک مسئله همان‌سازی سطح دوم نحوی است، زیرا یک متغیر تابعی است. یک راه‌حل برای این مسئله است، راه‌حل دیگری هم دارد که است.
 اولین الگوریتم همان‌سازی توسط کشف شد، درحالیکه اولین بررسی صوری را می‌توان به نسبت داد، که از همان‌سازی نحوی سطح اول می‌توان به عنوان بلوک سازنده اصلی فرایند اش برای منطق مرتبه اول استفاده کرد، که این موضوع در زمینه فناوری ، یک گام بزرگ به جلو محسوب می‌شد، زیرا یکی از منابع انفجار ترکیبیاتی را حذف می‌کرد: یعنی دیگر نیاز نبود نمونه‌سازی از ترم‌ها را جستجو کرد. امروزه استدلال خودکار هنوز اصلی‌ترین زمینه در کاربرد مسئله همان‌سازی است. یکسان‌سازی سطح‌اول نحوی در ، و نیز پیاده‌سازی زبان برنامه‌نویسی استفاده می‌شود، مخصوصاً در الگوریتم‌های مبتنی بر از آن استفاده می‌شود. از همان‌سازی نحوی در ، الگوریتم‌های ، و تحلیل استفاده می‌شود. از همان‌سازی سطح بالاتر در کمک اثبات‌گر استفاده می‌شود، مثلاً در ، و از آن استفاده می‌شود، و حالت‌های محدودتر همان‌سازی سطح بالا ( ) در بعضی از پیاده‌سازی‌های زبان برنامه‌نویسی، مثل ، استفاده شده‌است، به دلیل آنکه الگوهای سطح بالاتر قابلیت بیان بالاتری دارند، هنوز فرایند همان‌سازی مربوط به آن‌ها، ویژگی‌های نظری‌شان به همان‌سازی سطح اول نزدیک است.
 این مقاله راجع به موضوع علم است. برای ایدهٔ جهانی یکسان‌سازی، globalization را ببینید.
برای موارد دیگر،Unification (disambiguation) را ببینید.
 در منطق ریاضی، مخصوصاً آنچه در علم کامپیوتر به کار می‌رود، اتحاد رابطه یا جمله نوعی الحاق (در معنی شبکه)، با توجه به یک نوع تخصصی، می‌باشد. به معنای دیگر، ما یک preorder را روی یک سری از روابط در نظر می‌گیریم، مثلاً t* ≤ t یعنی اینکه t* از t گرفته شده، به وسیلهٔ جانشانی برخی رابطه(ها) برای یک یا تعداد بیشتری از متغیرهای آزاد در t. اتحاد u از s و t، در صورت وجود، یک رابطه است که برای هردوی t و s یک مثال جانشانی به‌شمار می‌رود. اگر هر مثال جانشانی از s و t یک مثال برای u هم باشد، u اتحاد کمین نامیده می‌شود.
برای مثال، در مورد چندجمله‌ای‌ها، و می‌توانند به صورت متحد شوند، اگر X را و Y را بگیریم.
 
 
 
 
 
 
 
 بگذارید p و q جملاتی در منطق نوع اول باشند.
UNIFY (p، q) = U where subst (U،p) = subst (U،q)
هرجا subst(U,p) باشد یعنی نتیجهٔ به‌کارگیری U جانشانی روی جملهٔ p. بنابراین U متحدکنندهٔ p و q نامیده می‌شود. یکسان‌سازی نتیجهٔ به‌کارگیری از U برای هردوی p و q است.
فرض کنید L مجموعه ایی از جملات باشد، برای مثال L = {p,q}. یک متحدکنندهٔ U، عمومی‌ترین متحدکننده نامیده می‌شود اگر برای تمام متحدکننده‌های U' از L، یک جایگزین s وجود داشته باشد که
subst(U',L) = subst(s,subst(U,L)).
 مفهوم یکسان‌سازی یکی از ایده‌های مهم در ورای برنامه‌نویسی منطقی است، که با زبان Prolog به بهترین نحو شناخته شده‌است. این برنامه مکانیزم محصور ومنسجم کردن محتویات متغیرها را نشان می‌دهد و می‌تواند به صورت نوعی از گمارش «یک زمانی» به نمایش در آید. در پرولوگ، این عملکرد به وسیلهٔ نماد تساوی = مشخص می‌شود، اما هنگام معرفی متغیرها نیز انجام می‌شود (قسمت زیر را ببینید). هم چنین در زبان‌های دیگر با استفاده از نماد تساوی =، استفاده می‌شود، اما هم چنین در رابطه با خیلی از عملگرها از جمله+، *، /. الگوریتم‌های استنباط نوع، به‌طور نمونه بر مبنای یکسان‌سازی هستند.
 
 
 
 
 
 
 توجه داشته باشید که عکس آن نیز درست است.
به دلیل این ذات اظهاری، ترتیب در یک توالی از یکسان‌سازی‌ها (معمولاً) مهم نیست.
توجه داشته باشید که در واژگان منطق نوع اول، یک اتم یا یک جزء، گزاره ومفهوم پایه است و به‌طور مشابه با یک جملهٔ پرولوگ یکسان می‌شود.
دانشمند فرانسوی کامپیوتر، Gérard Huet الگوریتمی برای یکسان‌سازی در simply typed lambda calculus در ۱۹۷۳ ارائه داد. از آن زمان پیشرفت‌های بسیاری در تئوری یکسان‌سازی صورت گرفته‌است.
 یکی از مؤثرترین تئوری‌های حذف این است که حذفیات، که مقدار آن‌ها با استفاده از یکسان‌سازی نوع بالاتر (HOU) تعیین شده‌است، توسط متغیرهای مستقل نمایش داده می‌شوند. برای مثال، نمایش معنایی جان شبیه مری است و پیتر هم چنین، این گونه است: (j; m)R(p) و مقدار R (نمایش معنایی حذفیات) توسط معادلهٔ شبیه به (j; m) = R(j) تعیین می‌شود. روند حل این معادله، یکسان‌سازی نوع بالاتر نامیده می‌شود.
 
 A, B, abc: هردوی توسط جزء abc یکسان شده‌است.
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 Retrieved from " "
Categories: Automated theorem proving | Logic programming
{"title": "همان‌سازی (علوم رایانه)", "link": "https://fa.wikipedia.org//w/index.php?title=%D9%87%D9%85%D8%A7%D9%86%E2%80%8C%D8%B3%D8%A7%D8%B2%DB%8C_(%D8%B9%D9%84%D9%88%D9%85_%D8%B1%D8%A7%DB%8C%D8%A7%D9%86%D9%87)&oldid=33109480", "language": "fa"}