استدلال منطقی و اثبات قضیه
استدلال منطقی و اثبات قضیه به استفاده از منطق صوری برای نمایش دانش و خودکارسازی استنتاج، یعنی استخراج نتایجی که لزوماً از مجموعهای از مقدمات پیروی میکنند، مربوط میشود.
Definition
اثبات قضیه، استخراج خودکار این است که آیا یک فرمول منطقی از مجموعهای از اصول موضوعه پیروی میکند یا خیر، که معمولاً با دستکاری فرمولها با قوانین استنتاج صحیح تا زمانی که هدف استخراج شود یا به تناقض برسد، انجام میشود.
Scope
این موضوع استدلال در منطق گزارهای و منطق مرتبه اول و الگوریتمهایی که آن را خودکار میکنند، پوشش میدهد: بررسی ارضاپذیری مبتنی بر جدول درستی و DPLL برای منطق گزارهای، یکسانسازی و اصل وضوح برای منطق مرتبه اول، زنجیره پیشرو و پسرو، و مبانی برنامهنویسی منطقی. این مبحث به صحت، کامل بودن و تصمیمپذیری رویههای استنتاج میپردازد. استدلالی که عدم قطعیت یا پیشفرضها را تحمل میکند، در موضوعات مرتبط با استدلال تحت عدم قطعیت و استدلال غیریکنواخت مورد بررسی قرار میگیرد.
Core questions
- یک نتیجه چه زمانی توسط مجموعهای از مقدمات مستلزم میشود و چگونه میتوان استلزام را به صورت مکانیکی بررسی کرد؟
- چگونه اصل وضوح، با یکسانسازی، یک قانون استنتاج کامل واحد برای منطق مرتبه اول ارائه میدهد؟
- زنجیره پیشرو و پسرو به عنوان استراتژیهای استنتاج چه تفاوتی با یکدیگر دارند؟
- با توجه به اینکه اعتبار مرتبه اول تنها نیمهتصمیمپذیر است، محدودیتهای استدلال خودکار چیست؟
Key concepts
- منطق گزارهای و مرتبه اول
- استلزام و اعتبار
- یکسانسازی
- وضوح و رد
- DPLL و حل SAT
- زنجیره پیشرو و پسرو
- بندهای هورن و برنامهنویسی منطقی
- صحت و کامل بودن
Key theories
- اصل وضوح
- وضوح رابینسون یک قانون استنتاج واحد بر روی بندها است که با یکسانسازی ترکیب شده و برای منطق مرتبه اول کامل در رد است: هر مجموعه بند غیرقابل ارضا را میتوان با استخراج بند تهی، غیرقابل ارضا نشان داد.
- DPLL و ارضاپذیری گزارهای
- رویه دیویس-پاتنام و پالایش DPLL آن، ارضاپذیری گزارهای را با تقسیمبندی سیستماتیک موارد با انتشار واحد و حذف لفظ خالص تعیین میکنند و اساس حلکنندههای SAT مدرن را تشکیل میدهند.
- برنامهنویسی منطقی و زنجیره پسرو
- محدود کردن منطق مرتبه اول به بندهای هورن و حل اهداف به صورت پسرو، منجر به برنامهنویسی منطقی میشود که در آن محاسبات، جستجوی اثبات است و هم یک روش استدلال و هم یک پارادایم برنامهنویسی را فراهم میکند.
Clinical relevance
اثبات قضیه خودکار و حلکنندههای SAT/SMT در تأیید سختافزار و نرمافزار، تحلیل برنامه، برنامهریزی و ریاضیات استفاده میشوند، در حالی که زبانهای برنامهنویسی منطقی مانند Prolog استنتاج زنجیره پسرو را در پایگاههای داده، تجزیه و تحلیل و سیستمهای مبتنی بر قانون به کار میبرند.
History
روشهای اثبات اولیه توسط گیلمور، دیویس و پاتنام (1960) استدلال گزارهای و کمی را خودکار کردند، و اصل وضوح رابینسون (1965) استنتاج مرتبه اول را در یک قانون واحد ادغام کرد. دهه 1970 شاهد پالایش وضوح در برنامهنویسی منطقی و Prolog بود؛ حلکنندههای SAT و SMT بعدها به یک فناوری عملی مهم تبدیل شدند.
Key figures
- John Alan Robinson
- Martin Davis
- Hilary Putnam
- Robert Kowalski
- Alan Robinson
Related topics
Seminal works
- robinson1965
- davis1960
- kowalski1979
Frequently asked questions
- اصل وضوح چیست؟
- وضوح یک قانون استنتاج واحد است که دو بند حاوی لفظهای مکمل را میگیرد و یک بند جدید را با ترکیب بقیه تولید میکند. با اعمال مکرر همراه با یکسانسازی، میتواند نشان دهد که مجموعهای از بندهای مرتبه اول غیرقابل ارضا است، که اساس اثبات قضایا با رد است.
- آیا اثبات قضیه خودکار تضمین شده است که خاتمه یابد؟
- برای منطق گزارهای، اعتبار تصمیمپذیر است، بنابراین رویهها خاتمه مییابند. برای منطق کامل مرتبه اول، اعتبار تنها نیمهتصمیمپذیر است: یک اثباتگر کامل در نهایت هر فرمول معتبر را تأیید میکند، اما ممکن است برای یک فرمول نامعتبر برای همیشه اجرا شود، بنابراین خاتمه به طور کلی تضمین نمیشود.