نمایش مبدأ برای رزلوشن SLD

'''رزلوشن بند معین خطی انتخابی''' {{به انگلیسی|Selective Linear Definite clause resolution}} با کوته‌نوشت '''SLD''' [[قاعده استنتاج]] اصلی استفاده شده در [[برنامه‌نویسی منطقی]] است. این [[رزولوشن (منطق)|رزلوشن]] یک روش اصلاحی از رزلوشن معمولی است و مزیت اصلی‌اش آن است که برای [[عبارت هورن|بندهای هورن]]، [[استواری|استوار]] و [[تمامیت (منطق)|کامل]] ابطال است.

== قاعده رزلوشن SLD ==
اگر به ما یک بند هدف به صورت زیر داده شود:

<math> \neg L_1 \lor \cdots \lor \neg L_i \lor \cdots \lor \neg L_n </math>

و لیترال انتخابی ما <math> \neg L_i </math> باشد و نیز یک [[عبارت هورن|بند معین]] ورودی به صورت زیر داشته باشیم:

<math> L \lor \neg K_1  \lor  \cdots \lor \neg K_m </math>

که در آن لیترال مثبت (اتم)<math> L\, </math> با اتم <math> L_i \, </math> از لیترال انتخابی <math>\neg L_i \, </math> [[همان‌سازی (علوم رایانه)|همان‌سازی]] شود، رزلوشن SLD یک بند هدف دیگر را نتیجه می‌دهد، که در این بند، لیترال انتخابی با لیترال‌های منفی بند ورودی جایگزین شده‌اند، و نیز جایگزینی همان‌سازی <math> \theta \, </math> در آن اعمال شده‌است:

<math> (\neg L_1 \lor \cdots \lor \neg K_1  \lor  \cdots \lor \neg K_m\ \lor \cdots \lor \neg L_n)\theta </math>

به صورت ساده، در منطق گزاره‌ای، اتم‌های <math> L_i \, </math> و <math> L \, </math> همان هستند، و جایگزینی همان‌سازی <math> \theta \, </math> پوچ و بی‌معنی است. با این حال، در حالت کلی‌تر، این جایگزینی همانی، برای آنکه دو لیترال همان‌سازی شوند، لازم است.

== منشأ نام «SLD» ==
نام «رزلوشن SLD» توسط آقای ماارتن ون امرن ارائه شد، او در واقع نامی را برای قاعده استنتاج بی‌نام [[روبرت کوالسکی]] انتخاب کرده بود.<ref>Robert Kowalski [http://www.doc.ic.ac.uk/~rak/papers/IFIP%2074.pdf Predicate Logic as a Programming Language] Memo 70, Department of Artificial Intelligence, University of Edinburgh. 1973. Also in Proceedings IFIP Congress, Stockholm, North Holland Publishing Co. , 1974, pp. 569-574.</ref> این نام از زرلوشن SL گرفته شده‌است،<ref>Robert Kowalski and Donald Kuehner, [http://www.doc.ic.ac.uk/~rak/papers/sl.pdf Linear Resolution with Selection Function] Artificial Intelligence, Vol. 2, 1971, pp. 227-60.</ref> که برای «منطق بندهای بدون محدودیت»، هم استوار و هم ابطال کامل بود. در واقع «SLD» به معنی «رزلوشن SL با بندهای معین» است.

هم در SL و هم در SLD، حرف «L» به این واقعیت اشاره دارد که یک اثبات رزلوشن را می‌توان به ترتیب خطی بندها محدود کرد:

<math> C_1, C_2, \cdots, C_l </math>

که در آن «بند ابتدا» یعنی <math> C_1 \, </math> یک بند ورودی است، و هر بند دیگر <math> C_{i+1} \, </math> یک [[حل مسئله]] است که والدین آن بند قبلی <math> C_i \, </math> است. اثبات موقعی رد می‌شود که بند نهایی <math> C_l \, </math> یک بند خالی باشد.

در SLD، همه بندهای موجود در ترتیب، بند هدف هستند، و والد دیگر یک بند ورودی است. اما در رزلوشن SL، والد دیگر یا یک بند ورودی است، یا یک بند جد (نیا)‌ی قبلی موجود در ترتیب است.

حرف «S» هم در SL و هم در SLD به معنی آن است که تنها لیترالی که در هر بند <math> C_i \, </math> دربرابر آن حل مسئله انجام می‌شود آن لیترالی است که به صورت یکتا، توسط یک قاعده گزینش یا تابع گزینش، انتخاب شده‌است. در رزلوشن SL، لیترال انتخابی محدود به همان لیترالی است که جدیدتر به بند معرفی شده‌است. در ساده‌ترین حالت، این تابع گزینش [[پشته|ورودی-آخر-خروجی-اول]] را می‌توان با ترتیبی که لیترال‌ها توسط آن نوشته شده‌اند، تعیین نمود، مثلاً [[پرولوگ]] از این روش استفاده می‌کند. با این حال، تابع گزینش در رزلوشن SLD همگانی‌تر از رزلوشن SL و رزلوشن پرولوگ است؛ یعنی هیچ محدودیتی روی لیترال گزینش شده وجود ندارد.

== تفسیر محاسباتی رزلوشن SLD ==
در منطق بندی، یک انکار SLD، نشان‌دهنده آن است که مجموعه ورودی بندها صدق‌ناپذیر هستند. با این حال، در برنامه‌نویسی منطقی، یک ابطال SLD یک تفسیر محاسباتی دارد. بند اولیه <math> \neg L_1 \lor \cdots \lor \neg L_i \lor \cdots \lor \neg L_n </math> را می‌توان به صورت انکار عطف زیرهدف‌های <math>  L_1 \land \cdots \land L_i \land \cdots \land L_n </math> تفسیر کرد. استنتاج بند <math> C_{i+1} \, </math> از <math> C_i \, </math> یک نتیجه خروجی، به کمک [[:en:Backward_chaining|استنتاج پسگرد]]، از مجموعه جدیدی از زیرهدف‌ها است که از یک بند ورودی به عنوان فرایند کاهش هدف استفاده می‌کند. جایگزین همان‌ساز <math> \theta \, </math> دو کار می‌کند: هم ورودی را از زیرهدف انتخابی به بدنه فرایند انتقال می‌دهد، و هم به صورت همزمان خروجی را از انتهای فرایند به زیرهدف‌های باقیمانده و گزینش نشده انتقال می‌دهد. بند خالی یعنی یک مجموعه خالی از زیرهدف‌ها، نشان‌دهنده آن است که «عطف اولیه زیرهدف‌ها در بند اولیه» حل شده‌است.

== راهبرد رزلوشن SLD ==
رزلوشن SLD به صورت ضمنی یک [[جستجوی درختی|درخت جستجو]] از محاسبات مختلف را تعریف می‌کند، که در آن «بند هدف اولیه» با «ریشه درخت» مرتبط است. برای هر گره در درخت، و برای هر بند معین در برنامه که لیترال مثبت آن با لیترال انتخابی در بند هدف مرتبط با گره، همان‌سازی می‌شود، یک گره فرزند مرتبط با بند هدف وجود دارد که این گره فرزند، از رزلوشن SLD به دست آمده‌است.

یک گره برگ (که هیچ فرزندی ندارد) موقعی گره موفقیت است که بند هدف مرتبط با آن بند خالی باشد. و موقعی یک گره شکست است که بند هدف مرتبط با آن غیرخالی باشد، و نیز لیترال انتخاب شده‌اش با هیچ لیترال مثبتی از هر بند ورودی همان‌سازی نشود.

رزلوشن SLD از یک نظر غیرمعین است: زیرا راهبرد جستجو برای کاوش درخت جستجو را تعیین نمی‌کند. پرولوگ، درخت را به صورت اول-عمق جستجو می‌کند، یعنی یک شاخه در هر زمان بررسی می‌شود، و موقعی که به یک گره شکست می‌رسد، از پس‌گرد استفاده می‌کند. [[الگوریتم جستجوی اول عمق|جستجوی اول عمق]] از نظر استفاده از منابع بسیار کارا و مؤثر است، اما ایرادش آن است که اگر فضای جستجو شامل شاخه‌های بی‌انتها باشد، و راهبرد جستجو آن شاخه‌ها را قبل از شاخه‌های متناهی جستجو کند، یک الگوریتم غیر کامل می‌شود: یعنی محاسبات خاتمه نمی‌یابد. راهبردهای دیگر جستجو، شامل [[الگوریتم جستجوی اول سطح|اول-سطح]]، [[جستجوی ابتدا بهترین|اول-بهترین]]، و جستجوی [[شاخه و حد]]، هم ممکن هستند. بعلاوه جستجو را می‌توان به صورت ترتیبی یا موازی انجام داد، یعنی در حالت ترتیبی هر زمان یک گره را بررسی کنیم یا به صورت موازی باشد یعنی همزمان چندین گره بررسی شوند.

رزلوشن SLD از این نظر که قاعده گزینش توسط قاعده استنتاج تعیین نمی‌شود، یک الگوریتم «غیر معین» است، این قاعده گزینش را می‌توان توسط یک فرایند تصمیم جداگانه تعیین کرد، که می‌تواند نسبت به موارد پویای فرایند اجرای برنامه حساس باشد.

فضای جستجوی رزلوشن SLD یک درخت or است، که در آن شاخه‌های مختلف نشان دهنده محاسبات متفاوت هستند. در حالت برنامه‌های منطق گزاره‌ای، می‌توان SLD را به شیوه ای تعمیم داد که فضای جستجو یک [[درخت و-یا|درخت and-or]] بشود، که در آن گره‌ها توسط لیترال منفرد برچسب‌زنی می‌شوند، و نشان دهنده زیرهدف هستند، و این گره‌ها یا با عطف یا با فصل به یکدیگر پیوند می‌یابند. به صورت کلی، موقعی که زیرهدف‌های عطفی، متغیرهای مشترک دارند، نمایش درخت and-or پیچیده‌تر است.

== مثال ==
اگر به ما برنامه منطقی زیر داده شده باشد:
<syntaxhighlight lang="prolog" line="1">
q :- p
p
</syntaxhighlight>
و هدف سطح بالای ما اینطوری باشد:
<syntaxhighlight lang="prolog" line="1">
q
</syntaxhighlight>
فضای جستجو شامل فقط یک شاخه است، که در آن <code>q</code> به <code>p</code> کاهش می‌یابد که آن هم به مجموعه خالی از زیرهدف‌ها کاهش می‌یابد، که این موضوع اشاره به محاسبات موفقیت می‌کند. در این حالت برنامه بسیار ساده است، و در آن نقشی برای تابع گزینش وجود ندارد و هیچ نیازی به جستجو هم نیست.

در منطق بندها، برنامه توسط مجموعه‌ای از بندها نمایش می‌یابد:

<math> q \lor \neg p  </math>

<math> p \, </math>

و هدف سطح بالا، توسط بند هدف با یک لیترال منفی منفرد نمایش می‌یابد:

<math> \neg q  </math>

و فضای جستجو شامل یک ابطال منفرد است:

<math> \neg q, \neg p, \mathit{false} </math>

که در آن <math> \mathit{false} \, </math> نشان‌دهنده بند خالی است.

اگر این بند به برنامه اضافه گردد:

<syntaxhighlight lang="prolog" line="1">
q :- r
</syntaxhighlight>

آنوقت یک شاخه اضافی به فضای جستجو اضافه می‌شود، که در آن گره برگ <code>r</code> یک گره شکست است. در پرولوگ، اگر این بند به جلوی برنامه اصلی اضافه شود، آنوقت پرولوگ از ترتیب نوشته شدن بندها استفاده می‌کند تا در شاخه‌های فضای جستجو، ترتیب بررسی را تعیین کند. پرولوگ این شاخه جدید را اول امتحان می‌کند، و شکست می‌خورد، و سپس پس‌گرد می‌کند تا شاخه منفرد برنامه اصلی را بررسی کند، و سپس موفق می‌شود.

اگر اکنون بند زیر
<syntaxhighlight lang="prolog" line="1">
p :- p
</syntaxhighlight>
به برنامه اضافه شود، آنوقت درخت جستجو شامل یک شاخه نامتناهی می‌شود، و اگر این بند را اول امتحان کند، پرولوگ وارد یک حلقه نامتناهی می‌شود، و شاخه موفق را پیدا نمی‌کند.

== SLDNF ==
SLDNF<ref>Krzysztof Apt and Maarten van Emden, [http://dl.acm.org/citation.cfm?doid=322326.322339 Contributions to the Theory of Logic Programming], Journal of the Association for Computing Machinery. Vol, 1982 - portal.acm.org</ref> یک گسترش برای رزلوشن SLD است، که با [[:en:Negation_as_failure|نفی به صورت شکست]] برخورد می‌کند. در SLDNF، بندهای هدف می‌تواند شامل نفی به صورت لیترال شکست باشد، که فرم <math> not(p) \, </math> دارند، که این لیترال فقط موقعی قابل گزینش است که شامل هیچ متغیری نباشد. موقعی که چنین لیترالی فاقد متغیری گزینش شود، یک زیراثبات (یا زیرمحاسبه) سعی می‌کند تا تعیین کند که «آیا یک انکار SLDNF با شروع از لیترال غیرمنفی متناظر <math> p \, </math> به عنوان بند اولیه، وجود دارد یا نه». زیرهدف گزینش شده <math> not(p) \, </math> موقعی موفقیت است که زیراثبات شکست بخورد، و موقعی شکست می‌خورد که زیراثبات موفق باشد.

== پانویس ==
{{پانویس}}

== منابع ==
{{یادکرد-ویکی|پیوند=https://en.wikipedia.org/wiki/SLD_resolution|عنوان=SLD resolution|زبان=انگلیسی|بازیابی=۱۸ مهٔ ۲۰۲۱}}
[[رده:برنامه‌نویسی منطقی]]
[[رده:قواعد استنتاج]]