رزلوشن SLD
رزلوشن بند معین خطی انتخابی (به انگلیسی: Selective Linear Definite clause resolution) با کوتهنوشت SLD قاعده استنتاج اصلی استفاده شده در برنامهنویسی منطقی است. این رزلوشن یک روش اصلاحی از رزلوشن معمولی است و مزیت اصلیاش آن است که برای بندهای هورن، استوار و کامل ابطال است.
قاعده رزلوشن SLD
اگر به ما یک بند هدف به صورت زیر داده شود:
و لیترال انتخابی ما
که در آن لیترال مثبت (اتم)
به صورت ساده، در منطق گزارهای، اتمهای
منشأ نام «SLD»
نام «رزلوشن SLD» توسط آقای ماارتن ون امرن ارائه شد، او در واقع نامی را برای قاعده استنتاج بینام روبرت کوالسکی انتخاب کرده بود. این نام از زرلوشن SL گرفته شدهاست، که برای «منطق بندهای بدون محدودیت»، هم استوار و هم ابطال کامل بود. در واقع «SLD» به معنی «رزلوشن SL با بندهای معین» است.
هم در SL و هم در SLD، حرف «L» به این واقعیت اشاره دارد که یک اثبات رزلوشن را میتوان به ترتیب خطی بندها محدود کرد:
که در آن «بند ابتدا» یعنی
در SLD، همه بندهای موجود در ترتیب، بند هدف هستند، و والد دیگر یک بند ورودی است. اما در رزلوشن SL، والد دیگر یا یک بند ورودی است، یا یک بند جد (نیا)ی قبلی موجود در ترتیب است.
حرف «S» هم در SL و هم در SLD به معنی آن است که تنها لیترالی که در هر بند
تفسیر محاسباتی رزلوشن SLD
در منطق بندی، یک انکار SLD، نشاندهنده آن است که مجموعه ورودی بندها صدقناپذیر هستند. با این حال، در برنامهنویسی منطقی، یک ابطال SLD یک تفسیر محاسباتی دارد. بند اولیه
راهبرد رزلوشن SLD
رزلوشن SLD به صورت ضمنی یک درخت جستجو از محاسبات مختلف را تعریف میکند، که در آن «بند هدف اولیه» با «ریشه درخت» مرتبط است. برای هر گره در درخت، و برای هر بند معین در برنامه که لیترال مثبت آن با لیترال انتخابی در بند هدف مرتبط با گره، همانسازی میشود، یک گره فرزند مرتبط با بند هدف وجود دارد که این گره فرزند، از رزلوشن SLD به دست آمدهاست.
یک گره برگ (که هیچ فرزندی ندارد) موقعی گره موفقیت است که بند هدف مرتبط با آن بند خالی باشد. و موقعی یک گره شکست است که بند هدف مرتبط با آن غیرخالی باشد، و نیز لیترال انتخاب شدهاش با هیچ لیترال مثبتی از هر بند ورودی همانسازی نشود.
رزلوشن SLD از یک نظر غیرمعین است: زیرا راهبرد جستجو برای کاوش درخت جستجو را تعیین نمیکند. پرولوگ، درخت را به صورت اول-عمق جستجو میکند، یعنی یک شاخه در هر زمان بررسی میشود، و موقعی که به یک گره شکست میرسد، از پسگرد استفاده میکند. جستجوی اول عمق از نظر استفاده از منابع بسیار کارا و مؤثر است، اما ایرادش آن است که اگر فضای جستجو شامل شاخههای بیانتها باشد، و راهبرد جستجو آن شاخهها را قبل از شاخههای متناهی جستجو کند، یک الگوریتم غیر کامل میشود: یعنی محاسبات خاتمه نمییابد. راهبردهای دیگر جستجو، شامل اول-سطح، اول-بهترین، و جستجوی شاخه و حد، هم ممکن هستند. بعلاوه جستجو را میتوان به صورت ترتیبی یا موازی انجام داد، یعنی در حالت ترتیبی هر زمان یک گره را بررسی کنیم یا به صورت موازی باشد یعنی همزمان چندین گره بررسی شوند.
رزلوشن SLD از این نظر که قاعده گزینش توسط قاعده استنتاج تعیین نمیشود، یک الگوریتم «غیر معین» است، این قاعده گزینش را میتوان توسط یک فرایند تصمیم جداگانه تعیین کرد، که میتواند نسبت به موارد پویای فرایند اجرای برنامه حساس باشد.
فضای جستجوی رزلوشن SLD یک درخت or است، که در آن شاخههای مختلف نشان دهنده محاسبات متفاوت هستند. در حالت برنامههای منطق گزارهای، میتوان SLD را به شیوه ای تعمیم داد که فضای جستجو یک درخت and-or بشود، که در آن گرهها توسط لیترال منفرد برچسبزنی میشوند، و نشان دهنده زیرهدف هستند، و این گرهها یا با عطف یا با فصل به یکدیگر پیوند مییابند. به صورت کلی، موقعی که زیرهدفهای عطفی، متغیرهای مشترک دارند، نمایش درخت and-or پیچیدهتر است.
مثال
اگر به ما برنامه منطقی زیر داده شده باشد:
q :- p
p
و هدف سطح بالای ما اینطوری باشد:
q
فضای جستجو شامل فقط یک شاخه است، که در آن q
به p
کاهش مییابد که آن هم به مجموعه خالی از زیرهدفها کاهش مییابد، که این موضوع اشاره به محاسبات موفقیت میکند. در این حالت برنامه بسیار ساده است، و در آن نقشی برای تابع گزینش وجود ندارد و هیچ نیازی به جستجو هم نیست.
در منطق بندها، برنامه توسط مجموعهای از بندها نمایش مییابد:
و هدف سطح بالا، توسط بند هدف با یک لیترال منفی منفرد نمایش مییابد:
و فضای جستجو شامل یک ابطال منفرد است:
که در آن
اگر این بند به برنامه اضافه گردد:
q :- r
آنوقت یک شاخه اضافی به فضای جستجو اضافه میشود، که در آن گره برگ r
یک گره شکست است. در پرولوگ، اگر این بند به جلوی برنامه اصلی اضافه شود، آنوقت پرولوگ از ترتیب نوشته شدن بندها استفاده میکند تا در شاخههای فضای جستجو، ترتیب بررسی را تعیین کند. پرولوگ این شاخه جدید را اول امتحان میکند، و شکست میخورد، و سپس پسگرد میکند تا شاخه منفرد برنامه اصلی را بررسی کند، و سپس موفق میشود.
اگر اکنون بند زیر
p :- p
به برنامه اضافه شود، آنوقت درخت جستجو شامل یک شاخه نامتناهی میشود، و اگر این بند را اول امتحان کند، پرولوگ وارد یک حلقه نامتناهی میشود، و شاخه موفق را پیدا نمیکند.
SLDNF
SLDNF یک گسترش برای رزلوشن SLD است، که با نفی به صورت شکست برخورد میکند. در SLDNF، بندهای هدف میتواند شامل نفی به صورت لیترال شکست باشد، که فرم
پانویس
- ↑ Robert Kowalski 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.
- ↑ Robert Kowalski and Donald Kuehner, Linear Resolution with Selection Function Artificial Intelligence, Vol. 2, 1971, pp. 227-60.
- ↑ Krzysztof Apt and Maarten van Emden, Contributions to the Theory of Logic Programming, Journal of the Association for Computing Machinery. Vol, 1982 - portal.acm.org
منابع
مشارکتکنندگان ویکیپدیا. «SLD resolution». در دانشنامهٔ ویکیپدیای انگلیسی، بازبینیشده در ۱۸ مهٔ ۲۰۲۱.