مصاص دماء (مُثبت نظرية)

برنامج Vampire هو برنامج آلي لإثبات النظريات في منطق الرتبة الأولى الكلاسيكي، طُوِّر في قسم علوم الحاسوب بجامعة مانشستر . حتى الإصدار الثالث، طُوِّر البرنامج بواسطة أندريه فورونكوف بالتعاون مع كريستوف هودر، وقبل ذلك مع ألكسندر ريازانوف. ومنذ الإصدار الرابع، انضم إلى فريق دولي أوسع نطاقًا فريق التطوير، ضم لورا كوفاكس، وجايلز ريجر، ومارتن سودا. ومنذ عام ١٩٩٩، حصد البرنامج ما لا يقل عن ٥٣ جائزة في مسابقة CADE ATP System ، وهي "كأس العالم لبرامج إثبات النظريات"، بما في ذلك قسم FOF المرموق وقسم TFA الخاص بالاستدلال النظري. ^{[ ٣ ] [ ٤ ]}

تُنفّذ نواة Vampire حسابات التحليل الثنائي المرتب والتراكب (للتعامل مع المساواة). ويمكن محاكاة قاعدة التقسيم وتقسيم المساواة السالبة من خلال إدخال تعريفات جديدة للمسندات والطي الديناميكي لهذه التعريفات. كما تدعم النواة خوارزمية تقسيم على غرار DPLL . ويُستخدم عدد من معايير التكرار القياسية وتقنيات التبسيط لتقليص مساحة البحث، مثل حذف التكرار ، وحل التضمين ، وإعادة الكتابة باستخدام معادلات الوحدة المرتبة، وقيود الأساسية، وعدم قابلية اختزال حدود الاستبدال . ويعتمد ترتيب الاختزال على الحدود على ترتيب كنوت-بنديكس القياسي .

تُستخدم عدة تقنيات فهرسة فعّالة لتنفيذ جميع العمليات الرئيسية على مجموعات المصطلحات والعبارات . ويُستخدم تخصيص الخوارزمية في وقت التشغيل لتسريع عملية المطابقة الأمامية.

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

إلى جانب إثبات النظريات، يمتلك برنامج Vampire وظائف أخرى ذات صلة مثل توليد الدوال الوسيطة .

يمكن الحصول على الملفات التنفيذية من موقع النظام الإلكتروني. ^{[ 5 ]} اعتبارًا من نوفمبر 2020، تم إصدار برنامج Vampire بموجب نسخة معدلة من رخصة BSD ثلاثية البنود، والتي تسمح صراحةً بالاستخدام التجاري. كانت الإصدارات السابقة متاحة بموجب رخصة احتكارية غير تجارية.

• الموقع الرسمي