|
fallible(X) :- human(X).
</syntaxhighlight>
که بر اساس مثالی از آقای [[:en:Terry_Winograd|تری وینوگراد]]<ref name="Winograd">{{cite journal|author=T. Winograd|date=1972|title=Understanding natural language|journal=Cognitive Psychology|volume=3|issue=1|pages=1–191|doi=10.1016/0010-0285(72)90002-3}}</ref> است، و هدفش توضیح زبان برنامه‌نویسی [[پلانر (زبان برنامه‌نویسی)|پلانر]] است. به عنوان یک بند در برنامه منطقی، از آن هم به عنوان «یک روند برای آزمون آنکه آیا X خطاپذیر است، باتوسط آزمون آنکه X انسان است استفاده می‌شود،می‌شود»، و هم به صورت «رویه یافتن یک X که خطاپذیر است، از طریق یافتن یک X که انسان است،است» به کار می‌رود. حتی واقعیت‌ها هم تفسیر [[برنامه‌نویسی رویه‌ای|رویه‌ای]] دارند. برای مثال، بند:
<syntaxhighlight lang="prolog">
human(socrates).
هم قابلیت استفاده به صورت رویه‌ای برای نشان دادن آنکه سقراط انسان است، و هم به صورت رویه‌ای برای یافتن یک X که انسان است، با «انتساب» سقراط به X به کار می‌رود.
یک برنامه‌نویس می‌تواند برنامه‌های منطقی را به صورت اعلانی بخواند تا صحت آن را راستی‌آزمایی کند. بعلاوه، فنون [[تبدیل برنامه]] مبتنی بر منطق، را می‌توان استفاده کرد تا برنامه‌های منطقی را به برنامه‌های معادل منطقی که کاراتر هستند تبدیل کرد. در خانواده زبان‌های برنامه‌نویسی منطقی مبتنی بر پرولوگ، برنامه‌نویس می‌تواند از «رفتار حل مسئله شناخته شده سازوکار اجرایی» استفاده کند تا کارایی برنامه‌ها را بهبود بدهد.
== تاریخچه ==
== مفاهیم ==
=== منطق و کنترل ===
برنامه‌نویسی منطقی را می‌توان به صورت «استنتاج کنترل‌شده» نگریست. یک مفهوم مهم در برنامه‌نویسی منطقی، جداسازی برنامه‌ها به «مولفهٔ منطقی» و «مولفهٔ کنترلی» است. در زبان‌های برنامه‌نویسی منطقی محض، «فقط» مولفه منطقی جواب‌های تولید شده را تعیین می‌کند. اما مولفه کنترلی برای ایجاد روش‌های متمایز اجرای یک برنامه منطقی قابل تغییر است. این مفهوم توسط این شعار قابل بیان است:
الگوریتم = منطق + کنترل
که در آن «منطق» نمایش دهندهنمایش‌دهنده یک برنامه منطقی است، و «کنترل» نمایش دهندهنمایش‌دهنده راهکارهای اثبات قضیه مختلف است.<ref>{{cite journal|author=R.A.Kowalski|date=July 1979|title=Algorithm=Logic + Control|journal=Communications of the ACM|volume=22|issue=7|pages=424–436|doi=10.1145/359131.359136|s2cid=2509896}}</ref>
=== اثبات مسئله ===
در حالت ساده شده و گزاره‌ای، که در آن برنامه منطقی و هدف اتمی سطح بالابالا، هیچ متغیری ندارند، استدلال پس‌گرد تعیین‌کننده یک [[درخت و-یا|درخت and-or]] است، که یک فضای جستجو را برای حل هدف می‌سازد. هدف سطح بالا همان ریشه درخت است. برای هر گره از درخت و هر بند که سر آن با آن گره منطبق است، یک مجموعه از گره‌ایگره‌های فرزند وجود دارد که متناظر با زیرهدف‌های موجود در بدنه بند هستند. این گره‌های فرزند توسط یک «and» با هم گروهبندی می‌شوند. مجموعه‌های جایگزین از فرزندان که متناظر با راه‌های جایگزین برای آن حل گره اند،گره‌اند، توسط یک «or» با هم گروهبندی می‌شوند.
از هر راهکار جستجوییجستجو ای برای جستجوی این فضا می‌توان استفاده کرد. پرولوگ از راهکار پس‌گرد، ورودی آخر-خروجی اول و ترتیبی استفاده می‌کند، که در آن در هر لحظه فقط یک جایگزین و یک زیرهدف در هر زمان درنظر گرفته می‌شود. در دیگر راهکارهای جستجو، مثل جستجوی موازی، پس‌گرد هوشمند، یا جستجوی بهترین-اول برای یافتن یک جواب بهینه، هم ممکن هستند.
در حالت عمومی تر، که در آن زیرهدف‌ها متغیر را به اشتراک می‌گذارند، راهکارهای دیگری را می‌توان استفاده کرد، مثلاً زیرهدفی را انتخاب کرد که بیشترین نمونه‌برداری را دارد، یا به اندازه کافی نمونه‌برداری شده‌است که فقط یک رویه را اعمال کند. از این راهکارها مثلاً در [[برنامه‌نویسی منطقی همزمان]] استفاده می‌شود.
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> شکست می‌خورد نشان می‌دهند. برای مثال:
<syntaxhighlight lang="prolog">
canfly(X) :- bird(X), not abnormal(X).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).
</syntaxhighlight>
و با هدف معین یافتن چیزی که بتواند پرواز کند:
<syntaxhighlight lang="prolog">
: <kbd>H :- Body<sub>k</sub>.</kbd>
{{پایان چپ‌چین}}
: به عنوان تعریفی از گزاره یگزاره‌ی:
{{چپ‌چین}}
H iff (Body<sub>1</sub> or … or Body<sub>k</sub>)
{{پایان چپ‌چین}}
که در آن "iff" یعنی "اگر و فقط اگر". نوشتن کامل‌بودن نیاز به استفاده صریح از گزاره تساوی و نیز شمول یک مجموعه از اتم‌های مناسب برای تساوی دارد. با این حال، پیاده‌سازی تساوی"نقیض به صورتعنوان شکست" تنها نیاز به نیمه‌های-if از تعاریف، بدون اتم‌های تساوی دارد.
برای مثال مکمل برنامه بالا به این صورت است:
: <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> را نمی‌دانیم یا به آن عقیده نداریم. «تفسیر معرفتی» این مزیت را دارد که توانایی ترکیب بسیار ساده با نقیض کلاسیک را دارد، این موضوع در «برنامه‌نویسی منطقی گسترش‌یافته» برای صوری‌سازی عباراتی مثل «ضد را نمی‌توان نشان دارد» وجود دارد، که در آن «ضد» همان نقیض کلاسیک، و «را نمی‌توان نشان داد» تفسیر معرفتی از نقیض به صورت شکست است.
=== نمایش دانش ===
این واقعیت که «می‌توان به بندهای هورن یک تفسیر رویه‌ای داد،داد»، و برعکس این موضوع که «رویه‌های کاهش هدف را می‌توان به صورت بند هورن + استدلال پس‌گرد شناخت،شناخت»، یعنی برنامه‌های منطقی نمایش‌های رویه‌ای و اعلانی از [[بازنمود دانش|دانش]] را ترکیب کرده‌اند. شمول «[[نقیض به عنوان شکست]]» یعنی برنامه‌نویسی منطقی نوعی [[منطق غیریکنواخت]] است.
علیرغم سادگیسادگی، در مقایسه با منطق کلاسیک، اثباتاین موضوع ثابت شده‌است که این ترکیب بند هورن با «نقیض به صورت شکست» به طرز شگفت‌آوری گویا و رسا است. برای مثال، یک نمایش طبیعی برای قوانینقوانین، حس مشترکعام «دلیل» و «تأثیر» ایجاد می‌کند، که هم به صورت [[:en:Situation_calculus|حساب وضعیت]] و هم به صورت [[:en:Event_calculus|حساب واقعه]] صوری سازیصوری‌سازی شده‌است. نشان داده شده‌است که به صورت کاملاً طبیعی با زبان نیمه صوری قانون‌گذاری متناظر است. بخصوص پراکن و سارتور<ref>Prakken, H. and Sartor, G. , 2015. [http://www.cs.uu.nl/groups/IS/archive/henry/ReviewLogicAndLawRevised.pdf Law and logic: a review from an argumentation perspective]. Artificial Intelligence, 227, 214–245.</ref> نمایش British Nationality Act را به صورت یک برنامه منطقی اعتبار دادند، که در آن «نفوذ بزرگی برای توسعه نمایش‌های محاسباتی قانون‌گذاری بود، که نشان می‌داد که چگونه برنامه‌نویسی منطقی امکان ایجاد نمایش‌های جذاب بصری را می‌داد، که برای ایجاد استدلال‌های خودکار قابل استقرار مستقیم بود».
== جستارهای وابسته ==
| 