1215 ورقة بحثية
تتقصى هذه الورقة المنطقيات الفضائية الأفينية ثلاثية الأبعاد، مبرهنةً أن المنطقيات عبر الأبعاد المختلفة تمتلك نظريات متميزة، ومثبتةً أن الحالة ثلاثية الأبعاد معبرة بما يكفي لتعريف أطر الإحداثيات وتوصيف المناطق حتى التكافؤ الأفيني.
تقدم هذه الورقة فئات مونويديةية (monoidal categories) مُدرجة بواسطة مونويدات تبادلية جزئية لأكسمنة البنية المدرجة للفئات المؤثرة، مما يوضح أن هذا الإطار يعمم كلاً من الفئات المونويدية القياسية والفئات المؤثرة مع توفير منظور موحد حول الحوسبة الواعية بالموارد والتوازي.
تقدم هذه الورقة حسابات جدول (tableau calculi) سليمة وكاملة، وإن كانت غير متناهية، لمنطق الضرب الهجين ثنائي الأبعاد ومنطق الضرب التابع الهجين، بما في ذلك نسخة معدلة ذات قاعدة خاصة للأخير.
تُثبت هذه الورقة طبيعية نظرية النوع متعدد الوسائط (MTT) عبر توسيع قابلية حساب "تايت" التركيبية للتعامل مع الأنماط، مما يوفر خوارزمية موحدة للتحقق من الأنواع لمختلف الأنظمة النمطية مثل العودية المحروسة والبارامتريّة الداخلية.
تقدم هذه الورقة حسابات تابلوء منتهية تكون كاملة للمنطق الهجين عند تطبيقها على نماذج ذات علاقات وصول مرتبة جزئياً بشكل صارم، ومرتبة جزئياً بشكل صارم غير محدودة، ومرتبة جزئياً.
تقدم هذه الورقة استمرارية أكثر منهجية لتحليل المؤلف السابق فيما يتعلق بترميز يابلو لمفارقة الكاذب باستخدام الرسوم البيانية اللانهائية غير الحلقية.
تقدم هذه الورقة أول تنفيذ ناجح لبرنامج "المنطق النظري" (Logic Theorist) الأصلي منذ أكثر من نصف قرن، وذلك عبر بناء مفسر لغة "كومون ليسب" (Common Lisp) جديد للغة "آي بي إل-5" (IPL-V) وإعادة إحياء برنامج الذكاء الاصطنا-عي لعام 1956 بأمانة من الكود المصدري لـ "ستيفيرود" لعام 1963، والذي نجح في إثبات 16 نظرية من أصل 23 نظرية من كتاب "مبادئ الرياضيات" (Principia Mathematica).
تقدم هذه الورقة جبر حدود القوة متعدد الحدود، وهو تمثيل وسيط مبتكر يجسّر الفجوة بين الصيغة العادية الموصلة (CNF) والصيغة العادية الجبرية (ANF) عبر ترميز الحدود أحادية الحد والبنود المهيكلة بشكل مدمج دون متغيرات مساعدة، مما يتيح معالجة رمزية فعالة واستدلالاً هجيناً مع تجنب التضخم الأسي.
تقدم هذه الورقة البحثية \textit{s2n-bignum-bench}، وهو أول معيار عام مُصمم لتقييم قدرة النماذج اللغوية الكبيرة على توليد براهين قابلة للتحقق آلياً لروتينات التجميع التشفيرية منخفضة المستوى والخاصة بالصناعة في HOL Light، وبذلك تعالج الفجوة بين النجاح في مسابقات الرياضيات والتحقق الرسمي في العالم الحقيقي.
تقدم هذه الورقة تحققاً رسمياً لمتراجحة إيزوبيريمتريك (المحيط المتساوي) الكلاسيكية في المستوي باستخدام مساعد الإثبات Lean 4 وMathlib، متبعةً نهج أدولف هورتويتز التحليلي لإثبات أنه من بين جميع المنحنيات المغلقة البسيطة ذات محيط معين، الدائرة هي التي تعظم المساحة المحصورة بشكل فريد.