الاستدلال المنطقي وإثبات النظريات
يتعلق الاستدلال المنطقي وإثبات النظريات باستخدام المنطق الصوري لتمثيل المعرفة وأتمتة الاستنتاج، واستخلاص النتائج التي تتبع بالضرورة من مجموعة من المقدمات.
Definition
إثبات النظريات هو الاستنتاج الآلي لما إذا كانت صيغة منطقية تتبع من مجموعة من البديهيات، عادةً عن طريق معالجة الصيغ بقواعد استدلال سليمة حتى يتم اشتقاق الهدف أو الوصول إلى تناقض.
Scope
يغطي هذا الموضوع الاستدلال في المنطق الافتراضي ومنطق الرتبة الأولى والخوارزميات التي تقوم بأتمتته: التحقق من قابلية الإرضاء (satisfiability) القائم على جداول الحقيقة وDPLL للمنطق الافتراضي، والتوحيد (unification) ومبدأ الحل (resolution principle) لمنطق الرتبة الأولى، والسلسلة الأمامية والخلفية (forward and backward chaining)، وأسس البرمجة المنطقية. ويتناول صحة (soundness) واكتمال (completeness) وقابلية تقرير (decidability) إجراءات الاستدلال. يتم تناول الاستدلال الذي يتحمل عدم اليقين أو الافتراضات في الموضوعات ذات الصلة بالاستدلال في ظل عدم اليقين والاستدلال غير الرتيب (nonmonotonic reasoning).
Core questions
- ماذا يعني أن تكون النتيجة مستتبعة (entailed) بمجموعة من المقدمات، وكيف يتم التحقق من الاستتباع ميكانيكيًا؟
- كيف يوفر مبدأ الحل، مع التوحيد، قاعدة استدلال واحدة كاملة لمنطق الرتبة الأولى؟
- كيف تختلف السلسلة الأمامية والخلفية كاستراتيجيات استدلال؟
- ما هي حدود الاستدلال الآلي، بالنظر إلى أن صلاحية الرتبة الأولى قابلة للتقرير جزئيًا فقط؟
Key concepts
- المنطق الافتراضي ومنطق الرتبة الأولى
- الاستتباع والصلاحية
- التوحيد
- الحل والدحض
- DPLL وحل مشكلات SAT
- السلسلة الأمامية والخلفية
- جمل هورن (Horn clauses) والبرمجة المنطقية
- الصحة والاكتمال
Key theories
- مبدأ الحل
- حل روبنسون هو قاعدة استدلال واحدة على الجمل (clauses) التي، بالاشتراك مع التوحيد، تكون كاملة الدحض لمنطق الرتبة الأولى: يمكن إثبات أن أي مجموعة غير قابلة للإرضاء من الجمل غير قابلة للإرضاء عن طريق اشتقاق الجملة الفارغة.
- DPLL وقابلية إرضاء المنطق الافتراضي
- يحدد إجراء ديفيس-باتنام وتحسينه DPLL قابلية إرضاء المنطق الافتراضي عن طريق تقسيم الحالات المنهجي مع انتشار الوحدة (unit propagation) وإزالة الحرف النقي (pure-literal elimination)، مما يشكل أساس حلول SAT الحديثة.
- البرمجة المنطقية والسلسلة الخلفية
- تقييد منطق الرتبة الأولى بجمل هورن وحل الأهداف بشكل عكسي ينتج عنه البرمجة المنطقية، حيث يكون الحساب هو البحث عن الإثبات، مما يوفر طريقة استدلال ونموذج برمجة.
Clinical relevance
تُستخدم أتمتة إثبات النظريات وحل مشكلات SAT/SMT في التحقق من الأجهزة والبرمجيات، وتحليل البرامج، والتخطيط، والرياضيات، بينما تطبق لغات البرمجة المنطقية مثل برولوج (Prolog) استدلال السلسلة الخلفية على قواعد البيانات، والتحليل اللغوي (parsing)، والأنظمة القائمة على القواعد.
History
أدت إجراءات الإثبات المبكرة التي قدمها جيلمور، وديفيس وباتنام (1960) إلى أتمتة الاستدلال الافتراضي والكمي، ووحد مبدأ الحل لروبنسون (1965) استدلال الرتبة الأولى في قاعدة واحدة. شهدت السبعينيات تحسين الحل ليصبح برمجة منطقية وبرولوج؛ ثم تطور حل مشكلات 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
- ما هو مبدأ الحل؟
- الحل هو قاعدة استدلال واحدة تأخذ جملتين تحتويان على حرفين متكاملين وتنتج جملة جديدة تجمع البقية. عند تطبيقها بشكل متكرر مع التوحيد، يمكنها إظهار أن مجموعة من جمل الرتبة الأولى غير قابلة للإرضاء، وهو أساس إثبات النظريات عن طريق الدحض.
- هل إثبات النظريات الآلي مضمون بالانتهاء؟
- بالنسبة للمنطق الافتراضي، الصلاحية قابلة للتقرير، لذا تنتهي الإجراءات. أما بالنسبة لمنطق الرتبة الأولى الكامل، فالصلاحية قابلة للتقرير جزئيًا فقط: سيؤكد المبرهن الكامل في النهاية أي صيغة صالحة، ولكنه قد يستمر إلى الأبد في صيغة غير صالحة، لذا لا يُضمن الانتهاء بشكل عام.