برنامه‌نویسی منطقی
مفاهیم > نقیض به عنوان شکست

برای بیشتر کاربردهای عملی، مثل کاربردهایی که نیاز به استدلال غیریکنواخت در هوش مصنوعی دارند، برنامه‌های منطقی بند هورن را باید به برنامه‌های منطقی نرمال گسترش داد، که در آن شرایط منفی وجود دارد. یک بند در برنامه منطقی نرمال این فرم را دارد:
H :- A1, …, An, not B1, …, not Bn.
و به صورت اعلانی به صورت یک پیامد منطقی خوانده می‌شود:
H if A1 and … and An and not B1 and … and not Bn.
که در آن H و همه Ai‌ها و Bi‌ها فرمول اتمی هستند. نقیض موجود در لیترال‌های منفی not Bi به صورت معمول به صورت «نقیض به عنوان شکست (به انگلیسی: negation as failure)» گفته می‌شود، زیرا در بیشتر پیاده‌سازی‌ها یک شرط منفی not Bi را با نشان دادن آنکه شرط مثبت Bi شکست می‌خورد نشان می‌دهند. برای مثال:
canfly(X) :- bird(X), not abnormal(X).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).
و با هدف معین یافتن چیزی که بتواند پرواز کند:
:- canfly(X).
دو جواب نامزد وجود دارد که زیر هدف اول یعنی bird(X) را حل می‌کند، که X = john و X = mary هستند. دومین زیر هدف not abnormal(john) از راه‌حل نامزد اول شکست می‌خورد، زیرا wounded(john) پیروز می‌شود، و از این رو abnormal(john) پیروز می‌شود. با این حال، زیر هدف دومی not abnormal(mary) از راه‌حل نامزد دومی پیروز می‌شود، زیرا wounded(mary) شکست می‌خورد، و از این رو abnormal(mary) شکست می‌خورد. از این رو، X = mary تنها جواب برای هدف است.
زبان میکروپلنر، یک ساختار به نام "thnot" دارد، که موقعی که به یک عبارت اعمال شود، مقدار درست را فقط (و فقط) وقتی برمی‌گرداند که ارزیابی عبارت شکست بخورد. یک عملگر معادل معمولاً در پیاده‌سازی‌های مدرن پرولوگ وجود دارد. این عملگر معمولاً به صورت  not(Goal)  یا \+ Goalنوشته می‌شود، که در آن  Goal یک هدف (گزاره) است که باید توسط برنامه اثبات شود. این عملگر با نقیض در منطق مرتبه اول متفاوت است: یک نقیض مثل \+ X == 1 موقعی که متغیر  X به اتم  1 انتساب یافته باشد، شکست می‌خورد، اما در همه حالت‌های دیگر پیروز می‌شود، که این شامل حالتی است که  X انتسابی نداشته باشد. این موضوع استدلال پرولوگ را غیریکنواخت می‌کند: X = 1, \+ X == 1 همیشه شکست می‌خورد اما، عبارت \+ X == 1, X = 1 می‌تواند پیروز شود، اگر  X را به  1 انتساب دهیم، بسته به آنکه آیا  X از اول انتسابی داشته‌است یا نه (توجه کنید که پرولوگ استاندارد هدف‌ها را به ترتیب چپ-به-راست اجرا می‌کند).
وضعیت منطقی نقیض به صورت شکست تا زمان کیث کلارک (۱۹۷۸) حل نشده بود، که او نشان داد که تحت شرایط طبیعی معین، یک پیاده‌سازی درست (و گاهی کامل) از نقیض کلاسیک، در رابطه با کامل بودن برنامه، است. کامل بودن تقریباً به درنظر گرفتن مجموعه همه بندهای برنامه با یک گزاره مشابه در سمت چپ می‌رسد، اگر بگوییم:
به عنوان تعریفی از گزاره‌ی:
H iff (Body1 or … or Bodyk)
که در آن "iff" یعنی "اگر و فقط اگر". نوشتن کامل‌بودن نیاز به استفاده صریح از گزاره تساوی و نیز شمول یک مجموعه از اتم‌های مناسب برای تساوی دارد. با این حال، پیاده‌سازی "نقیض به عنوان شکست" تنها نیاز به نیمه‌های-if از تعاریف، بدون اتم‌های تساوی دارد.
برای مثال مکمل برنامه بالا به این صورت است:
مفهوم کامل بودن در بالا، به معناشناسی انحصار مک‌کارتی برای استدلال پیش‌فرض، و نیز به فرض جهانی بسته، بسیار مرتبط است.
به عنوان یک جایگزین برای معناشناسی کامل‌بودن، «نقیض به عنوان شکست» را می‌توان به صورت معرفتی تفسیر کرد، که این موضوع در معناشناسی مدل ثابت برای برنامه‌نویسی مجموعه جواب وجود دارد. در این تفسیر، عبارت not(Bi) به صورت لیترالی، یعنی که Bi را نمی‌دانیم یا به آن عقیده نداریم. «تفسیر معرفتی» این مزیت را دارد که توانایی ترکیب بسیار ساده با نقیض کلاسیک را دارد، این موضوع در «برنامه‌نویسی منطقی گسترش‌یافته» برای صوری‌سازی عباراتی مثل «ضد را نمی‌توان نشان دارد» وجود دارد، که در آن «ضد» همان نقیض کلاسیک، و «را نمی‌توان نشان داد» تفسیر معرفتی از نقیض به صورت شکست است.