موضوع مقاله: برنامه‌نویسی منطقی | مخاطب: عمومی | لحن: دانشنامه‌ای | ساختار: عنوان، مقدمه، 3 بخش، جمع‌بندی | مقاله: | # برنامه‌نویسی منطقی | مقدمه: هر برنامه نوشته‌شده به یک زبان برنامه‌نویسی منطقی مجموعه‌ای از جمله‌ها است که حالت منطقی دارند، که آن جمله‌ها بیانگر «واقعیت» و «قاعده» دربارهٔ یک دامنه مسئله هستند. | ## بخش 1: برنامه‌نویسی منطقی | خانواده‌های زبان برنامه‌نویسی منطقی اصلی شامل پرولوگ، برنامه‌نویسی مجموعه جواب (ASP) و دیتالاگ است. در ساده‌ترین حالت که H, B1, … , Bn همه شان فرمول اتمی هستند، به این بندها بند معین یا بند هورن گفته می‌شود. با این حال گسترش‌های زیادی برای این حالت ساده وجود دارد، که مهمترین گسترش حالتی است که شرط‌های موجود در بدنه بند، توانمندی "نقیض فرمول اتمی بودن" را نیز دارند. زبان‌های برنامه‌نویسی منطقی که شامل این گسترش هستند، توانمندی‌های نمایش دانش را برای منطق غیریکنواخت دارند. در ASP و Dataloog، برنامه‌های منطقی را فقط به صورت اعلانی می‌توان خواند، و اجرایشان توسط فرایند اثبات، یا مولد مدل انجام می‌شود، که این رفتار در آن‌ها توسط برنامه‌نویس قابل کنترل نیست. که بر اساس مثالی از آقای تری وینوگراد است، و هدفش توضیح زبان برنامه‌نویسی پلانر است. به عنوان یک بند در برنامه منطقی، از آن هم به عنوان «یک روند برای آزمون آنکه آیا X خطاپذیر است، توسط آزمون آنکه X انسان است استفاده می‌شود»، و هم به صورت «رویه یافتن یک X که خطاپذیر است، از طریق یافتن یک X که انسان است» به کار می‌رود. هم قابلیت استفاده به صورت رویه‌ای برای نشان دادن آنکه سقراط انسان است، و هم به صورت رویه‌ای برای یافتن یک X که انسان است، با «انتساب» سقراط به X به کار می‌رود. یک برنامه‌نویس می‌تواند برنامه‌های منطقی را به صورت اعلانی بخواند تا صحت آن را راستی‌آزمایی کند. بعلاوه، فنون تبدیل برنامه مبتنی بر منطق، را می‌توان استفاده کرد تا برنامه‌های منطقی را به برنامه‌های معادل منطقی که کاراتر هستند تبدیل کرد. در خانواده زبان‌های برنامه‌نویسی منطقی مبتنی بر پرولوگ، برنامه‌نویس می‌تواند از «رفتار حل مسئله شناخته شده سازوکار اجرایی» استفاده کند تا کارایی برنامه‌ها را بهبود بدهد. تاریخچه استفاده از منطق ریاضی برای نمایش و اجرای برنامه‌های رایانه‌ای اولین بار در دهه ۱۹۳۰ توسط آلونزو چرچ صورت گرفت. مفاهیم منطق و کنترل برنامه‌نویسی منطقی را می‌توان به صورت «استنتاج کنترل‌شده» نگریست. یک مفهوم مهم در برنامه‌نویسی منطقی، جداسازی برنامه‌ها به «مولفهٔ منطقی» و «مولفهٔ کنترلی» است. | ## بخش 2: برنامه‌نویسی منطقی | در زبان‌های برنامه‌نویسی منطقی محض، «فقط» مولفه منطقی جواب‌های تولید شده را تعیین می‌کند. اما مولفه کنترلی برای ایجاد روش‌های متمایز اجرای یک برنامه منطقی قابل تغییر است. این مفهوم توسط این شعار قابل بیان است: الگوریتم = منطق + کنترل که در آن «منطق» نمایش‌دهنده یک برنامه منطقی است، و «کنترل» نمایش‌دهنده راهکارهای اثبات قضیه مختلف است. اثبات مسئله در حالت ساده و گزاره‌ای، که در آن برنامه منطقی و هدف اتمی سطح بالا، هیچ متغیری ندارند، استدلال پس‌گرد تعیین‌کننده یک درخت and-or است، که یک فضای جستجو را برای حل هدف می‌سازد. برای هر گره از درخت و هر بند که سر آن با آن گره منطبق است، یک مجموعه از گره‌های فرزند وجود دارد که متناظر با زیر هدف‌های موجود در بدنه بند هستند. مجموعه‌های جایگزین از فرزندان که متناظر با راه‌های جایگزین برای آن حل گره‌اند، توسط یک «or» با هم گروهبندی می‌شوند. پرولوگ از راهکار پس‌گرد، ورودی آخر-خروجی اول و ترتیبی استفاده می‌کند، که در آن در هر لحظه فقط یک جایگزین و یک زیر هدف در هر زمان درنظر گرفته می‌شود. در دیگر راهکارهای جستجو، مثل جستجوی موازی، پس‌گرد هوشمند، یا جستجوی بهترین-اول برای یافتن یک جواب بهینه، هم ممکن هستند. در حالت عمومی تر، که در آن زیر هدف‌ها متغیر را به اشتراک می‌گذارند، راهکارهای دیگری را می‌توان استفاده کرد، مثلاً زیر هدفی را انتخاب کرد که بیشترین نمونه‌برداری را دارد، یا به اندازه کافی نمونه‌برداری شده‌است که فقط یک رویه را اعمال کند. نقیض به عنوان شکست برای بیشتر کاربردهای عملی، مثل کاربردهایی که نیاز به استدلال غیریکنواخت در هوش مصنوعی دارند، برنامه‌های منطقی بند هورن را باید به برنامه‌های منطقی نرمال گسترش داد، که در آن شرایط منفی وجود دارد. نقیض موجود در لیترال‌های منفی not Bi به صورت معمول به صورت «نقیض به عنوان شکست » گفته می‌شود، زیرا در بیشتر پیاده‌سازی‌ها یک شرط منفی not Bi را با نشان دادن آنکه شرط مثبت Bi شکست می‌خورد نشان می‌دهند. زبان میکروپلنر، یک ساختار به نام "thnot" دارد، که موقعی که به یک عبارت اعمال شود، مقدار درست را فقط (و فقط) وقتی برمی‌گرداند که ارزیابی عبارت شکست بخورد. این عملگر با نقیض در منطق مرتبه اول متفاوت است: یک نقیض مثل \+ X == 1 موقعی که متغیر X به اتم 1 انتساب یافته باشد، شکست می‌خورد، اما در همه حالت‌های دیگر پیروز می‌شود، که این شامل حالتی است که X انتسابی نداشته باشد. این موضوع استدلال پرولوگ را غیریکنواخت می‌کند: X = 1, \+ X == 1 همیشه شکست می‌خورد اما، عبارت \+ X == 1, X = 1 می‌تواند پیروز شود، اگر X را به 1 انتساب دهیم، بسته به آنکه آیا X از اول انتسابی داشته‌است یا نه (توجه کنید که پرولوگ استاندارد هدف‌ها را به ترتیب چپ-به-راست اجرا می‌کند). | ## بخش 3: برنامه‌نویسی منطقی | وضعیت منطقی نقیض به صورت شکست تا زمان کیث کلارک (۱۹۷۸) حل نشده بود، که او نشان داد که تحت شرایط طبیعی معین، یک پیاده‌سازی درست (و گاهی کامل) از نقیض کلاسیک، در رابطه با کامل بودن برنامه، است. کامل بودن تقریباً به درنظر گرفتن مجموعه همه بندهای برنامه با یک گزاره مشابه در سمت چپ می‌رسد، اگر بگوییم: H :- Body1. نوشتن کامل‌بودن نیاز به استفاده صریح از گزاره تساوی و نیز شمول یک مجموعه از اتم‌های مناسب برای تساوی دارد. با این حال، پیاده‌سازی "نقیض به عنوان شکست" تنها نیاز به نیمه‌های-if از تعاریف، بدون اتم‌های تساوی دارد. مفهوم کامل بودن در بالا، به معناشناسی انحصار مک‌کارتی برای استدلال پیش‌فرض، و نیز به فرض جهانی بسته، بسیار مرتبط است. به عنوان یک جایگزین برای معناشناسی کامل‌بودن، «نقیض به عنوان شکست» را می‌توان به صورت معرفتی تفسیر کرد، که این موضوع در معناشناسی مدل ثابت برای برنامه‌نویسی مجموعه جواب وجود دارد. در این تفسیر، عبارت not(Bi) به صورت لیترالی، یعنی که Bi را نمی‌دانیم یا به آن عقیده نداریم. «تفسیر معرفتی» این مزیت را دارد که توانایی ترکیب بسیار ساده با نقیض کلاسیک را دارد، این موضوع در «برنامه‌نویسی منطقی گسترش‌یافته» برای صوری‌سازی عباراتی مثل «ضد را نمی‌توان نشان دارد» وجود دارد، که در آن «ضد» همان نقیض کلاسیک، و «را نمی‌توان نشان داد» تفسیر معرفتی از نقیض به صورت شکست است. نمایش دانش این واقعیت که «می‌توان به بندهای هورن یک تفسیر رویه‌ای داد»، و برعکس این موضوع که «رویه‌های کاهش هدف را می‌توان به صورت بند هورن + استدلال پس‌گرد شناخت»، یعنی برنامه‌های منطقی نمایش‌های رویه‌ای و اعلانی از دانش را ترکیب کرده‌اند. علیرغم سادگی، در مقایسه با منطق کلاسیک، این موضوع ثابت شده‌است که این ترکیب بند هورن با «نقیض به صورت شکست» به طرز شگفت‌آوری گویا و رسا است. برای مثال، یک نمایش طبیعی برای قوانین، حس عام «دلیل» و «تأثیر» ایجاد می‌کند، که هم به صورت حساب وضعیت و هم به صورت حساب واقعه صوری‌سازی شده‌است. نشان داده شده‌است که به صورت کاملاً طبیعی با زبان نیمه صوری قانون‌گذاری متناظر است. | ## جمع‌بندی | نمایش British Nationality Act را به صورت یک برنامه منطقی اعتبار دادند، که در آن «نفوذ بزرگی برای توسعه نمایش‌های محاسباتی قانون‌گذاری بود، که نشان می‌داد که چگونه برنامه‌نویسی منطقی امکان ایجاد نمایش‌های جذاب بصری را می‌داد، که برای ایجاد استدلال‌های خودکار قابل استقرار مستقیم بود».