1215 ورقة بحثية
تقدم الورقة البحثية Apply2Isar، وهي أداة تقوم تلقائياً بتحويل براهين نمط "apply" الإجرائية في Isabelle/HOL إلى براهين Isar إعلانية مقروءة ومتينة، وتثبت فعاليتها من خلال التقييم على مجموعة مرجعية كبيرة من أرشيف البراهين الرسمية في Isabelle.
تثبت هذه الورقة أن فرق الحجم بين الدوائر البولينية المثلى والصيغ فوق أساس AIG يقتصر بدقة على 0 أو 1، مما يميز الشروط الدقيقة التي يحدث عندها المشاركة ويثبت أن أي فجوة غير صفرية تنشأ حصرياً من بوابة واحدة ذات تفرع مخرج قدره 2.
تقدم هذه الورقة نظرية الفئات الموسعة والمغنية بنصف المعيار (dilated seminorm-enriched category theory) كإطار عمل موحد لنظريات الحد المركزي، حيث تؤسس لنظرية حد مركزي مجردة تستعيد النتائج الكلاسيكية وتثمر عن تطبيقات مبتكرة في المتشعبات الرمزية والميكانيكا الإحصائية.
تثبت هذه الورقة كون قابلية الإرضاء للمعادلات الديوفانتية التكعيبية المفردة فوق الأعداد الطبيعية هي -complete وغير قابلة للتقرير، وذلك عبر بناء مترجم أولي تكراري موحد يترجم القابلية للإثبات الحسابي إلى قيود تكعيبية، مما يؤدي في النهاية إلى الحصول على متعدد حدود تكعيبي كوني صريح واحد تم التحقق منه آلياً في Rocq.
تقترح هذه الورقة نهجاً عصبياً رمزياً يدمج نماذج اللغات الكبيرة بشكل تآزري مع أدوات حل القيود لتوليد والتحقق من التمهيدات المساعدة بشكل تكراري، مما يحسن بشكل كبير القدرة على حل القيود التي تتضمن تعريفات استقرائية مقارنة بأدوات الحل المتطورة.
تقدم هذه الورقة إطاراً رسمياً لـ "تغيير النموذج" في مفاهيم منطق الوصف، حيث تميز بين الإقصاء والاستقبال والمراجعة، وتثبت أن المراجعة هي عملية متميزة لا يمكن اختزالها ببساطة إلى مزيج من العمليتين الأخريين عند تحليل توافقهما ضمن منطقي EL وALC.
تقدم هذه الورقة مفهومًا فئويًا لـ "التفسير" بين النماذج الاحتمالية باستخدام الروابط (spans)، مبرهنةً أن كل نظرية احتمالية محدودة محليًا تقبل تمثيلًا كلاسيكيًا حادًا ومعياريًا من خلال بناء دالي.
إن LTLGuard هو إطار عمل معياري يُمكّن نماذج اللغة ذات الأوزان المفتوحة والموفرة للموارد (4-14 مليار معلمة) من توليد مواصفات المنطق الزمني الخطي (LTL) صحيحة وخالية من التعارض من المتطلبات غير الرسمية، وذلك عبر الجمع بين التوليد المقيد والاستدلال الرمزي خفيف الوزن للتحقق من الاتساق والتحسين بشكل تكراري.
تُثبت هذه الورقة أنه بينما لا تستطيع آلات تورينج المحدودة تحقيق المصادقة الذاتية بسبب العبء الزمني، فإن التقدم التكراري لملاحظات التوقف النهائية يشكل سلسلة صاعدة يؤدي حد سكوت (Scott limit) الخاص بها إلى النقطة الثابتة الصغرى، مما يحل مشكلة التوقف فعلياً من خلال التأجيل المستمر للتشخيص (diagonalization).
تقدم هذه الورقة نهجاً جديداً قائماً على الـ SAT لحسابات الاتصال في المنطق من الدرجة الأولى يقوم بترميز بنية البحث عن البرهان ذاتها، حيث تعرض ثلاثة ترميزات متميزة مع كسر التماثل وتنفذها في الحل الجديد upCoP للنهوض بالاستدلال الآلي.