مساعد التدقيق اللغوي

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

يتمثل أحد الجهود الحديثة في هذا المجال في جعل هذه الأدوات تستخدم الذكاء الاصطناعي لأتمتة صياغة الرياضيات العادية. ^{[ 1 ]}

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

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

يُعتبر برنامج أوتوماث ، الذي طوّره نيكولاس جوفرت دي بروين بدءًا من عام 1967، أول برنامج للتحقق من البراهين وأول نظام يستخدم علاقة كاري-هوارد بين البرامج والبراهين. ^{[ 2 ]} استخدم إل إس فان بنثام جوتينغ برنامج أوتوماث عام 1977 لصياغة كتاب لاندو " أسس التحليل" ، الذي كان أول صياغة رسمية للأعداد الحقيقية. ^{[ 3 ]}

في عام 1973، نشر روبرت بوير وجيه مور كتاب "إثبات النظريات حول وظائف لغة ليسب" الذي كان يهدف إلى التحقق من صحة البرامج، وليس الرياضيات. ^{[ 4 ]} يُعرف برنامج إثبات النظريات الخاص بهما الآن باسم ACL2 .

في سبعينيات القرن العشرين، قدمت كلية لندن للتصميم في إدنبرة فكرة استخدام لغة برمجة وظيفية كلغة وصفية لإثبات النظريات، مما أدى إلى ظهور عائلة HOL من مساعدي البرهان. ^{[ 3 ]}

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

• ACL2 – لغة برمجة، ونظرية منطقية من الدرجة الأولى، وبرنامج إثبات النظريات (مع كل من الوضعين التفاعلي والتلقائي) في تقليد بوير-مور.
• مُثبتات النظريات HOL – مجموعة من الأدوات مُشتقة في الأصل من مُثبت النظريات LCF . في هذه الأنظمة، يُمثل النواة المنطقية مكتبة لغة البرمجة الخاصة بها. تُمثل النظريات عناصر جديدة في اللغة، ولا يُمكن إدخالها إلا عبر "استراتيجيات" تضمن صحتها المنطقية. يُتيح تركيب الاستراتيجيات للمستخدمين إمكانية إنتاج براهين مهمة بتفاعلات قليلة نسبيًا مع النظام. تشمل هذه المجموعة ما يلي:
  • HOL4 – النسخة "الأصلية"، لا تزال قيد التطوير النشط. تدعم كلاً من Moscow ML و Poly/ML . تتمتع بترخيص من نوع BSD .
  • HOL Light – نسخة مزدهرة من "النسخة البسيطة". مبنية على لغة OCaml .
  • ProofPower – تحولت إلى شركة احتكارية، ثم عادت إلى المصادر المفتوحة. تعتمد على Standard ML .
• IMPS، نظام إثبات رياضي تفاعلي. ^{[ 11 ]}
• إيزابيل هي أداة تفاعلية لإثبات النظريات، حيث يمكن ترميز أنظمة أخرى. تُعدّ إيزابيل/هول أشهر إصداراتها، وتعتمد بنيتها الأساسية على أساس قريب من أساس أداة إثبات هول. تشمل الإصدارات الأخرى إيزابيل/زد إف وإيزابيل/إف أو إل ^{[ 12 ]} . يخضع الكود البرمجي الرئيسي لترخيص بي إس دي، لكن توزيعة إيزابيل تتضمن العديد من الأدوات الإضافية بتراخيص مختلفة.
• Jape – مبني على لغة جافا.
• Lean هي أداة تفاعلية لإثبات النظريات ولغة برمجة وظيفية ذات أنواع بيانات تابعة. تعتمد على حساب الإنشاءات الاستقرائية مع عوالم غير تراكمية. منذ الإصدار الرابع (الذي صدر عام ٢٠٢٣)، أصبحت Lean ذاتية الاستضافة. يمكن استخدامها لصياغة الرياضيات (وتمتلك مكتبة واسعة ومتكاملة للرياضيات الرسمية)، وكذلك للتحقق من البرمجيات والأجهزة.
• ليغو
• ماتيتا – نظام إضاءة يعتمد على حساب الإنشاءات الاستقرائية.
• مينلوج – مساعد إثبات يعتمد على المنطق الأدنى من الدرجة الأولى.
• ميزر – مساعد إثبات يعتمد على منطق الرتبة الأولى، بأسلوب الاستنتاج الطبيعي ، ونظرية مجموعة تارسكي-غروتينديك .
• PhoX – مساعد إثبات يعتمد على منطق الرتبة العليا وهو قابل للتوسيع.
• نظام التحقق من النموذج الأولي (PVS) - لغة إثبات ونظام يعتمدان على منطق من الدرجة العليا.
• Rocq (المعروف سابقًا باسم Coq ) – برنامج إثبات نظريات تفاعلي شائع يعتمد على حساب التفاضل والتكامل للإنشاءات الاستقرائية.
• نظام إثبات النظرية (TPS) و ETPS - مثبتات نظرية تفاعلية تعتمد أيضًا على حساب لامدا المكتوب ببساطة، ولكنها تعتمد على صياغة مستقلة للنظرية المنطقية وتنفيذ مستقل.

كانت واجهة المستخدم الأمامية الشائعة الاستخدام لمساعدي البرهان هي Proof General، المبنية على Emacs ، والتي طُوّرت في جامعة إدنبرة . أما اليوم، فتتضمن العديد من برامج البرهان محررها الخاص. يتضمن Rocq برنامج RocqIDE، المبني على OCaml/ Gtk . ويتضمن Isabelle برنامج Isabelle/jEdit، المبني على jEdit وبنية Isabelle/ Scala لمعالجة البراهين الموجهة نحو المستندات. ومؤخرًا، طُوّرت إضافات لبرنامج Visual Studio Code لـ Rocq، ^{[ 13 ]} وIsabelle بواسطة ماكاريوس وينزل، ^{[ 14 ]} ولـ Lean 4 بواسطة مطوري leanprover. ^{[ 15 ]}

يُجري فريك ويديك تصنيفًا لبرامج المساعدة في البرهان بناءً على عدد النظريات المُصاغة رسميًا من قائمة تضم 100 نظرية معروفة. وحتى سبتمبر 2025، لم يكن سوى ستة أنظمة لديها براهين رسمية لأكثر من 70% من النظريات، وهي: إيزابيل، وهول لايت، ولين، وروك، وميتاماث، وميزر. ^{[ 16 ] [ 17 ]}

فيما يلي قائمة بالبراهين البارزة التي تم صياغتها بشكل رسمي ضمن برامج مساعدة البرهان.

نظرية	مساعد التدقيق اللغوي	سنة
نظرية الألوان الأربعة [ 18 ]	روك	2005
نظرية فيت – طومسون [ 19 ]	روك	2012
المجموعة الأساسية للدائرة [ 20 ]	روك	2013
مشكلة إردوس-جراهام [ 21 ] [ 22 ]	نحيف	2022
تخمين فريمان-روزا متعدد الحدود على${\displaystyle \mathbb {F} _{2}}$[ 23 ]	نحيف	2023
BB(5) = 47,176,870 [ 24 ]	روك	2024

• إثبات النظريات آلياً – مجال فرعي من الاستدلال الآلي والمنطق الرياضي 
• البرهان بمساعدة الحاسوب – برهان رياضي يتم إنشاؤه جزئيًا على الأقل بواسطة الحاسوب 
• التحقق الرسمي – إثبات أو دحض صحة خوارزميات معينة مقصودة 
• Prover9 – هو برنامج آلي لإثبات النظريات في منطق الرتبة الأولى والمنطق المعادلاتي
• بيان QED – اقتراح لإنشاء قاعدة بيانات حاسوبية لجميع المعارف الرياضية 
• قابلية الإرضاء modulo النظريات – مشكلة منطقية تُدرس في علوم الحاسوب 

• باريندريخت، هينك ؛ جوفرز، هيرمان (2001). "18. مساعدو البرهان باستخدام أنظمة الأنواع التابعة" (ملف PDF) . في روبنسون، آلان جيه إيه؛ فورونكوف، أندريه (محرران). دليل الاستدلال الآلي . المجلد  2. إلسيفير. الصفحات  1149 وما بعدها. ISBN 978-0-444-50812-6تمت أرشفة النسخة الأصلية (PDF) بتاريخ 27-07-2007.
• بفينينغ، فرانك . "17. الأطر المنطقية" (ملف PDF) . دليل المجلد 2 2001. الصفحات 1065-1148 . 
• بفينينغ، فرانك (1996). "ممارسة الأطر المنطقية". في كيرشنر، هـ. (محرر). الأشجار في الجبر والبرمجة - CAAP '96 . سلسلة محاضرات في علوم الحاسوب. المجلد  1059. سبرينغر. الصفحات 119-134 . doi : 10.1007/3-540-61064-2_33 . ISBN  3-540-61064-2.
• كونستابل، روبرت ل. (1998). "الأنواع في علوم الحاسوب والفلسفة والمنطق" . في: بوس، إس آر (محرر). دليل نظرية البرهان . دراسات في المنطق. المجلد  137. إلسيفير. الصفحات 683-786 . ISBN  978-0-08-053318-6.
• فيديك، فريك (2005). “المثبتون السبعة عشر في العالم” (PDF) . جامعة رادبود نيميغن.

• متحف مُثبت النظريات
• "مقدمة" في البرمجة المعتمدة مع الأنواع التابعة .
• مقدمة إلى مساعد إثبات Coq (مع مقدمة عامة عن إثبات النظريات التفاعلي)
• إثبات النظريات التفاعلي لمستخدمي أغدا
• قائمة بأدوات إثبات النظريات

الكتالوجات

• الرياضيات الرقمية حسب الفئة: أدوات إثبات التكتيكات
• أنظمة ومجموعات الاستدلال الآلي
• أنظمة إثبات النظريات والاستدلال الآلي
• قاعدة بيانات لأنظمة الاستدلال الآلي الحالية
• NuPRL: أنظمة أخرى
• "أطر منطقية وتطبيقات محددة" . مؤرشف من الأصل في 10 أبريل 2022. تم الاطلاع عليه في 15 فبراير 2024 .(بقلم فرانك فيننج).
• DMOZ : العلوم: الرياضيات: المنطق والأسس: المنطق الحسابي: الأطر المنطقية