إثبات النظريات آلياً

يُعدّ إثبات النظريات الآلي (المعروف أيضًا باسم الاستدلال الآلي ) فرعًا من فروع الاستدلال الآلي والمنطق الرياضي ، ويتناول إثبات النظريات الرياضية بواسطة برامج الحاسوب . وقد شكّل الاستدلال الآلي في مجال البراهين الرياضية دافعًا رئيسيًا لتطوير علوم الحاسوب .

بينما تعود جذور المنطق الصوري إلى أرسطو ، شهدت أواخر القرن التاسع عشر وأوائل القرن العشرين تطور المنطق الحديث والرياضيات الصورية. قدّم فريجه في كتابه " Begriffsschrift " (1879) حسابًا كاملًا للقضايا ، وما يُعرف أساسًا بمنطق المسندات الحديث . ^{[ 1 ]} أما كتابه "أسس الحساب " ، الذي نُشر عام 1884، ^{[ 2 ]} فقد عبّر فيه عن (أجزاء من) الرياضيات باستخدام المنطق الصوري. واصل راسل ووايتهيد هذا النهج في كتابهما المؤثر "Principia Mathematica" ، الذي نُشر لأول مرة بين عامي 1910 و1913، ^{[ 3 ]} ثم صدرت منه طبعة ثانية منقحة عام 1927. ^{[ 4 ]} اعتقد راسل ووايتهيد أنهما يستطيعان استنباط جميع الحقائق الرياضية باستخدام بديهيات وقواعد الاستدلال في المنطق الصوري، مما يفتح المجال من حيث المبدأ لأتمتة هذه العملية. ^{[ 5 ]} في عام 1920، قام ثورالف سكوليم بتبسيط نتيجة سابقة لليوبولد لوفنهايم ، مما أدى إلى نظرية لوفنهايم-سكوليم ، وفي عام 1930، إلى مفهوم عالم هيربراند وتفسير هيربراند الذي سمح باختزال (عدم) إرضاء صيغ الرتبة الأولى (وبالتالي صحة النظرية) إلى مسائل إرضاء القضايا (التي قد تكون لا نهائية العدد). ^{[ 6 ]}

في عام 1929، أثبت موجزيس بريسبورغر أن نظرية الرتبة الأولى للأعداد الطبيعية مع الجمع والمساواة (والتي تُعرف الآن باسم حساب بريسبورغر تكريماً له) قابلة للتقرير ، وقدم خوارزمية يمكنها تحديد ما إذا كانت جملة معينة في اللغة صحيحة أم خاطئة. ^{[ 7 ] [ 8 ]}

مع ذلك، بعد فترة وجيزة من هذه النتيجة الإيجابية، نشر كورت غودل كتابه "حول القضايا غير القابلة للتقرير رسميًا في مبادئ الرياضيات والأنظمة ذات الصلة " (1931)، مُبينًا أنه في أي نظام بديهي قوي بما فيه الكفاية، توجد عبارات صحيحة لا يمكن إثباتها في النظام نفسه. ^{[ 9 ]} وقد طُوّر هذا الموضوع لاحقًا في ثلاثينيات القرن العشرين على يد ألونسو تشيرش وآلان تورينج ، اللذين قدّما من جهة تعريفين مستقلين لكنهما متكافئان للحوسبة ، ومن جهة أخرى قدّما أمثلة ملموسة على المسائل غير القابلة للتقرير . ^{[ 10 ]}

في عام 1954، برمج مارتن ديفيس خوارزمية بريسبرغر لحاسوب JOHNNIAC ذي الصمامات المفرغة في معهد الدراسات المتقدمة في برينستون، نيو جيرسي. ووفقًا لديفيس، "كان إنجازها الأبرز هو إثبات أن مجموع عددين زوجيين هو عدد زوجي". ^{[ 8 ] [ 11 ]} وفي عام 1956، ظهر نظام " المنطق النظري " (Logic Theorist) ، وهو نظام استنتاجي لمنطق القضايا في كتاب "الأصول الرياضية للفلسفة الطبيعية" (Principia Mathematica) ، والذي طوره ألين نيويل ، وهربرت أ. سيمون ، وجيه سي شو ، وكان أكثر طموحًا . وقد عمل هذا النظام أيضًا على حاسوب JOHNNIAC، حيث بنى براهين من مجموعة صغيرة من بديهيات القضايا وثلاث قواعد استنتاجية: قاعدة القياس المنطقي ( modus ponens )، واستبدال المتغيرات (القضوية) ، واستبدال الصيغ بتعريفاتها. استخدم النظام التوجيه الاستدلالي ، ونجح في إثبات 38 من أول 52 نظرية في كتاب "الأصول الرياضية للفلسفة الطبيعية" . ^{[ 8 ]}

حاول النهج "الاستدلالي" لنظرية المنطق محاكاة علماء الرياضيات، ولم يستطع ضمان إيجاد برهان لكل نظرية صحيحة حتى من حيث المبدأ. في المقابل، حققت خوارزميات أخرى أكثر منهجية، نظريًا على الأقل، اكتمال منطق الرتبة الأولى. اعتمدت المناهج الأولية على نتائج هيربراند وسكوليم لتحويل صيغة الرتبة الأولى إلى مجموعات متزايدة الحجم من الصيغ المنطقية عن طريق تحديد متغيرات بمصطلحات من عالم هيربراند . بعد ذلك ، يمكن التحقق من عدم قابلية الصيغ المنطقية للإرضاء باستخدام عدد من الطرق. استخدم برنامج جيلمور التحويل إلى الصيغة الانفصالية العادية ، وهي صيغة تكون فيها قابلية الصيغة للإرضاء واضحة. ^{[ 8 ] [ 12 ]}

بحسب المنطق الأساسي، تتفاوت صعوبة تحديد صحة الصيغة من بسيطة إلى مستحيلة. في حالة منطق القضايا ، تكون المسألة قابلة للحل ولكنها من فئة NP-كاملة ، ولذا يُعتقد أن الخوارزميات ذات الوقت الأسي فقط هي الموجودة لمهام البرهان العامة. ^{[ 13 ]} بالنسبة لحساب التفاضل والتكامل من الدرجة الأولى ، تنص نظرية اكتمال غودل على أن النظريات (العبارات القابلة للإثبات) هي بالضبط الصيغ الصحيحة دلاليًا ، وبالتالي فإن الصيغ الصحيحة قابلة للتعداد الحسابي : فمع توفر موارد غير محدودة، يمكن إثبات أي صيغة صحيحة في النهاية. مع ذلك، لا يمكن دائمًا التعرف على الصيغ غير الصحيحة (تلك التي لا تستلزمها نظرية معينة). ^{[ 14 ]}

ينطبق ما سبق على نظريات الرتبة الأولى، مثل حساب بيانو . مع ذلك، بالنسبة لنموذج محدد يمكن وصفه بنظرية من الرتبة الأولى، قد تكون بعض العبارات صحيحة ولكنها غير قابلة للتقرير في النظرية المستخدمة لوصف النموذج. على سبيل المثال، وفقًا لنظرية عدم الاكتمال لغودل ، نعلم أن أي نظرية متسقة تكون بديهياتها صحيحة للأعداد الطبيعية لا يمكنها إثبات صحة جميع عبارات الرتبة الأولى للأعداد الطبيعية، حتى لو سُمح لقائمة البديهيات بأن تكون غير محدودة. ^{[ 15 ]} يترتب على ذلك أن برنامج إثبات النظريات الآلي سيفشل في التوقف أثناء البحث عن برهان تحديدًا عندما تكون العبارة قيد البحث غير قابلة للتقرير في النظرية المستخدمة، حتى لو كانت صحيحة في النموذج محل الاهتمام. على الرغم من هذا القيد النظري، عمليًا، يمكن لبرامج إثبات النظريات حل العديد من المسائل الصعبة، حتى في النماذج التي لا تصفها أي نظرية من الرتبة الأولى وصفًا كاملًا (مثل الأعداد الصحيحة ).

تُعدّ مسألة التحقق من صحة البرهان ، وهي مسألة أبسط ولكنها ذات صلة، حيث يتم التحقق من صحة برهان موجود لنظرية ما. ولتحقيق ذلك، يُشترط عمومًا أن يكون بالإمكان التحقق من كل خطوة من خطوات البرهان باستخدام دالة أو برنامج تكراري بسيط ، وبالتالي فإن المسألة قابلة للحل دائمًا.

نظراً لأن البراهين التي تولدها برامج إثبات النظريات الآلية عادة ما تكون كبيرة جداً، فإن مشكلة ضغط البراهين أمر بالغ الأهمية، وقد تم تطوير تقنيات مختلفة تهدف إلى جعل مخرجات برنامج الإثبات أصغر حجماً، وبالتالي أكثر سهولة في الفهم والتحقق.

تتطلب برامج المساعدة في البرهان من المستخدم البشري تقديم تلميحات للنظام. وبحسب درجة الأتمتة، يمكن اختزال برنامج البرهان إلى مجرد مدقق للبرهان، حيث يقدم المستخدم البرهان بطريقة رسمية، أو يمكن تنفيذ مهام برهان مهمة تلقائيًا. تُستخدم برامج البرهان التفاعلية في مهام متنوعة، ولكن حتى الأنظمة الآلية بالكامل أثبتت عددًا من النظريات الشيقة والصعبة، بما في ذلك نظرية واحدة على الأقل استعصت على علماء الرياضيات لفترة طويلة، وهي حدسية روبنز . ^{[ 16 ] [ 17 ]} ومع ذلك، فإن هذه النجاحات متقطعة، وعادةً ما يتطلب العمل على المسائل الصعبة مستخدمًا خبيرًا.

يُفرّق أحيانًا بين إثبات النظريات والتقنيات الأخرى، حيث تُعتبر العملية إثباتًا للنظريات إذا كانت تتألف من برهان تقليدي، يبدأ بالمسلمات ويُنتج خطوات استدلال جديدة باستخدام قواعد الاستدلال. وتشمل التقنيات الأخرى التحقق من النماذج ، والذي يتضمن، في أبسط حالاته، تعدادًا شاملًا للعديد من الحالات الممكنة (مع أن التنفيذ الفعلي لبرامج التحقق من النماذج يتطلب براعة كبيرة، ولا يقتصر على التعداد الشامل).

توجد أنظمة إثبات نظريات هجينة تستخدم التحقق من النماذج كقاعدة استدلال. كما توجد برامج مصممة لإثبات نظرية معينة، مع برهان (غير رسمي عادةً) يُثبت صحة النظرية إذا انتهى البرنامج بنتيجة معينة. ومن الأمثلة الجيدة على ذلك البرهان الآلي لنظرية الألوان الأربعة ، والذي أثار جدلاً واسعاً لكونه أول برهان رياضي يُزعم أنه يستحيل التحقق منه بشرياً نظراً لحجم حسابات البرنامج الهائل (تُسمى هذه البراهين بالبراهين غير القابلة للتحقق ). ومن الأمثلة الأخرى على البراهين المدعومة بالبرامج البرهان الذي يُبين أن لعبة " توصيل أربعة" يمكن أن يفوز بها اللاعب الأول دائماً.

يتركز الاستخدام التجاري لإثبات النظريات الآلي في الغالب على تصميم الدوائر المتكاملة والتحقق منها. منذ ظهور خطأ FDIV في معالج بنتيوم ، صُممت وحدات الفاصلة العائمة المعقدة في المعالجات الدقيقة الحديثة بدقة متناهية. تستخدم شركات مثل AMD وإنتل وغيرها إثبات النظريات الآلي للتحقق من صحة تنفيذ عمليات القسمة وغيرها من العمليات في معالجاتها. ^{[ 18 ]}

تشمل الاستخدامات الأخرى لبرامج إثبات النظريات توليف البرامج ، أي بناء برامج تُلبي مواصفات رسمية . ^{[ 19 ]} وقد تم دمج برامج إثبات النظريات الآلية مع مساعدي البرهان ، بما في ذلك Isabelle/HOL . ^{[ 20 ]}

تُستخدم أدوات إثبات النظريات أيضًا في معالجة اللغة الطبيعية والدلالات الرسمية ، حيث تُستخدم لتحليل تمثيلات الخطاب . ^{[ 21 ] [ 22 ]}

في أواخر الستينيات، بدأت الجهات الممولة لأبحاث الاستدلال الآلي بالتركيز على الحاجة إلى تطبيقات عملية. وكان من أوائل المجالات المثمرة مجال التحقق من البرامج، حيث طُبقت أدوات إثبات النظريات من الدرجة الأولى على مشكلة التحقق من صحة برامج الحاسوب المكتوبة بلغات مثل باسكال وآدا وغيرها . ومن أبرز أنظمة التحقق من البرامج المبكرة نظام ستانفورد للتحقق من باسكال، الذي طوره ديفيد لوكهام في جامعة ستانفورد . ^{[ 23 ] [ 24 ] [ 25 ]} وقد استند هذا النظام إلى نظام ستانفورد للتحقق من الحلول، الذي طُوّر أيضًا في ستانفورد باستخدام مبدأ الحل لجون آلان روبنسون . وكان هذا أول نظام استدلال آلي يُظهر قدرة على حل مسائل رياضية نُشرت في مجلة " إشعارات الجمعية الرياضية الأمريكية" قبل نشر حلولها رسميًا.

يُعدّ إثبات النظريات من الرتبة الأولى أحد أكثر فروع إثبات النظريات الآلي نضجًا. يتميز هذا المنطق بقدرته التعبيرية الكافية التي تسمح بتحديد مسائل عشوائية، غالبًا بطريقة طبيعية وبديهية. من ناحية أخرى، لا يزال شبه قابل للتقرير، وقد طُوّر عدد من الحسابات السليمة والكاملة، مما يُتيح أنظمة مؤتمتة بالكامل . ^{[ 26 ]} تسمح أنواع المنطق الأكثر تعبيرًا، مثل منطق الرتب العليا ، بالتعبير بسهولة عن نطاق أوسع من المسائل مقارنةً بمنطق الرتبة الأولى، إلا أن إثبات النظريات لهذه الأنواع من المنطق أقل تطورًا. ^{[ 27 ] [ 28 ]}

لقد استفادت جودة الأنظمة المنفذة من وجود مكتبة كبيرة من الأمثلة المعيارية القياسية - مكتبة مسائل الآلاف من المسائل لإثبات النظريات (TPTP) ^{[ 31 ]} - بالإضافة إلى مسابقة نظام CADE ATP (CASC)، وهي مسابقة سنوية لأنظمة الدرجة الأولى للعديد من الفئات المهمة من مسائل الدرجة الأولى.

بعض الأنظمة المهمة (جميعها فازت على الأقل بقسم واحد من أقسام مسابقة CASC) مدرجة أدناه.

• E هو برنامج إثبات عالي الأداء لمنطق الدرجة الأولى الكامل، ولكنه مبني على حساب المعادلات البحت ، وقد تم تطويره في الأصل في مجموعة الاستدلال الآلي في جامعة ميونخ التقنية تحت إشراف فولفغانغ بيبل ، والآن في جامعة بادن فورتمبيرغ التعاونية الحكومية في شتوتغارت .
• يعتمد برنامج Otter ، الذي طُوّر في مختبر أرغون الوطني ، على دقة من الدرجة الأولى والتعديل البارامتري . وقد استُبدل برنامج Otter لاحقًا ببرنامج Prover9 ، الذي يُستخدم مع برنامج Mace4 .
• SETHEO هو نظام عالي الأداء يعتمد على حساب حذف النماذج الموجه نحو الهدف ، وقد طُوِّر في الأصل بواسطة فريق تحت إشراف فولفغانغ بيبل . تم دمج E وSETHEO (مع أنظمة أخرى) في برنامج إثبات النظريات المركب E-SETHEO.
• طُوِّر برنامج Vampire ونُفِّذ في الأصل في جامعة مانشستر على يد أندريه فورونكوف وكريستوف هودر. ويجري تطويره الآن بواسطة فريق دولي متنامٍ. وقد فاز البرنامج بفئة FOF (من بين فئات أخرى) في مسابقة CADE ATP System بانتظام منذ عام 2001. ^{[ 32 ]}
• فالدمايستر هو نظام متخصص لمنطق الرتبة الأولى ذي المعادلات الوحدوية، طوره أرنيم بوخ وتوماس هيلينبراند. وقد فاز بجائزة قسم CASC UEQ لمدة أربعة عشر عامًا متتالية (1997-2010).
• SPASS هو برنامج لإثبات نظريات المنطق من الدرجة الأولى مع خاصية المساواة. وقد طُوّر هذا البرنامج من قبل مجموعة أبحاث أتمتة المنطق في معهد ماكس بلانك لعلوم الحاسوب .

يُعدّ متحف مُثبتات النظريات ^{[ 33 ]} مبادرةً لحفظ مصادر أنظمة مُثبتات النظريات لتحليلها مستقبلاً، نظراً لأهميتها الثقافية والعلمية. ويضمّ المتحف مصادر العديد من الأنظمة المذكورة آنفاً.

• حل من الدرجة الأولى مع التوحيد
• استبعاد النموذج
• طريقة الجداول التحليلية
• التراكب وإعادة كتابة المصطلحات
• التحقق من النموذج
• الاستقراء الرياضي ^{[ 34 ]}
• مخططات القرار الثنائي
• DPLL
• التوحيد من الدرجة الأعلى
• حذف المحدد الكمي ^{[ 35 ]}
• نماذج لغوية كبيرة ^{[ 36 ]}

• قائمة بأدوات إثبات النظريات