برنامه‌نویسی منطقی: تفاوت میان نسخه‌ها

محتوای حذف‌شده محتوای افزوده‌شده
بدون خلاصۀ ویرایش
خط ۵۱:
=== نقیض به عنوان شکست ===
برای بیشتر کاربردهای عملی، مثل کاربردهایی که نیاز به استدلال غیریکنواخت در هوش مصنوعی دارند، برنامه‌های منطقی [[عبارت هورن|بند هورن]] را باید به برنامه‌های منطقی نرمال گسترش داد، که در آن شرایط منفی وجود دارد. یک بند در برنامه منطقی نرمال این فرم را دارد:
{{چپ‌چین}}
 
H :- A<sub>1</sub>, …, A<sub>n</sub>, not B<sub>1</sub>, …, not B<sub>n</sub>.
{{پایان چپ‌چین}}
 
و به صورت اعلانی به صورت یک پیامد منطقی خوانده می شود:
{{چپ‌چین}}
 
H if A<sub>1</sub> and … and A<sub>n</sub> and not B<sub>1</sub> and … and not B<sub>n</sub>.
{{پایان چپ‌چین}}
 
که در آن H و همه A<sub>i</sub> و <kbd>B<sub>i</sub></kbd> ها فرمول اتمی هستند. نقیض موجود در لیترال‌های منفی not B<sub>i</sub> به صورت معمول به صورت «[[نقیض به عنوان شکست]] {{به انگلیسی|negation as failure}}» گفته می شود، زیرا در بیشتر پیاده‌سازی ها یک شرط منفی not B<sub>i</sub> را با نشان دادن آنکه شرط مثبت B<sub>i</sub> شکست می خورد نشان می دهند. برای مثال:
 
خط ۷۰:
 
وضعیت منطقی نقیض به صورت شکست تا زمان [[:en:Keith_Clark_(computer_scientist)|کیث کلارک]] (1978) حل نشده بود، که او نشان داد که تحت شرایط طبیعی معین، یک پیاده‌سازی درست (و گاهی کامل) از نقیض کلاسیک، در رابطه با کامل بودن برنامه، است. کامل بودن تقریبا به درنظر گرفتن مجموعه همه بندهای برنامه با یک گزاره مشابه در سمت چپ می رسد، اگر بگوییم:
{{چپ‌چین}}
 
: <kbd>H :- Body<sub>1</sub>.</kbd>
: <kbd>…</kbd>
: <kbd>H :- Body<sub>k</sub>.</kbd>
{{پایان چپ‌چین}}
 
: به عنوان تعریفی از گزاره ی:
 
{{چپ‌چین}}
 
H iff (Body<sub>1</sub> or … or Body<sub>k</sub>)
{{پایان چپ‌چین}}
 
که در آن "iff" یعنی "اگر و فقط اگر". نوشتن کامل‌بودن نیاز به استفاده صریح از گزاره تساوی و شمول یک مجموعه از اتم‌های مناسب برای تساوی دارد. با این حال، پیاده‌سازی تساوی به صورت شکست تنها نیاز به نیمه‌های-if از تعاریف، بدون اتم‌های تساوی دارد.
 
برای مثال مکمل برنامه بالا به این صورت است:
{{چپ‌چین}}
 
: <kbd>canfly(X) iff bird(X), not abnormal(X).</kbd>
: <kbd>abnormal(X) iff wounded(X).</kbd>
خط ۹۰:
: <kbd>not john = mary.</kbd>
: <kbd>not mary = john.</kbd>
{{پایان چپ‌چین}}
 
: مفهوم کامل بودن در بالا، به معناشناسی [[:en:Circumscription_(logic)|انحصار]] مک‌کارتی برای استدلال پیش‌فرض، و نیز به [[:en:Closed-world_assumption|فرض جهانی بسته]]، بسیار مرتبط است.
: به عنوان یک جایگزین برای معناشناسی کامل‌بودن، «نقیض برای شکست» را می توان به صورت معرفتی تفسیر کرد، که این موضوع در [[:en:Stable_model_semantics|معناشناسی مدل ثابت]] برای [[برنامه‌نویسی مجموعه جواب]] وجود دارد. در این تفسیر عبارت not(B<sub>i</sub>) به صورت لیترالی یعنی که B<sub>i</sub> را نمی دانیم یا به آن عقیده نداریم. تفسیر معرفتی این مزیت را دارد که توانایی ترکیب بسیار ساده با نقیض کلاسیک را دارد، این موضوع در «برنامه‌نویسی منطقی گسترش‌یافته» برای صوری‌سازی عباراتی مثل «ضد را نمی توان نشان دارد» وجود دارد، که در آن «ضد» همان نقیض کلاسیک، و «را نمی توان نشان داد» تفسیر معرفتی از نقیض به صورت شکست است.