1215 ورقة بحثية
تُرسخ هذه الورقة تقابلاً صورياً بين المنطق الحدسي الزمني والبرمجة المنطقية الزمنية عبر رفع المناهج الرائدة لبيرس وأوزوريو إلى الإطار الزمني، مما يعمق الأسس النظرية لبرمجة مجموعات الإجابات الزمنية من خلال منطق التوازن الزمني.
تقدم هذه الورقة برهاناً جبرياً بديلاً لتمام الجبر العلائقي بالنسبة لصيغ المنطق من الدرجة الأولى، وذلك عبر الاستفادة من تضمينه في الجبر الأسطواني لاستنباط خوارزمية تحويل جديدة وإرساء الأساس لتوسيع هذه النتائج لتشمل النماذج التي تتعامل مع المعلومات غير المكتملة أو الغامضة.
تقترح هذه الورقة إطار عمل جديدًا لتوصيف الخوارزميات الموزعة رسميًا كنظريات بديهية تصريحية ضمن منطق جهوي ثلاثي القيم فوق شبه طوبولوجيا، مما يوفر تجريدًا عالي المستوى ودقيقًا يلتقط خصائص النظام الجوهرية مع تمكين التحقق البشري والآلي الصارم، كما هو موضح من خلال البراهين الرسمية في لغة Lean 4 لبروتوكولات التصويت، والبث، والاتفاق.
تقدم الورقة البحثية TaoBench، وهو معيار مرجعي جديد مستمد من كتاب تيرانس تاو "التحليل 1" (Analysis I)، والذي يقيم أدوات إثبات النظريات الآلية بناءً على إنشاءات رياضية مخصصة، كاشفاً عن انخفاض ملحوظ في الأداء بنسبة 26% مقارنة بمسائل MathLib القياسية، ومسلطاً الضوء على أن القصور الأساسي للأنظمة الحالية يكمن في عدم قدرتها على التعميم عبر أطر تعريفية مختلفة بدلاً من الصعوبة المتأصلة في المهام نفسها.
تقدم هذه الورقة تضميناً آلياً للأنواع المعتمدة والأكوان في نظرية مجموعات "تارسكي-غروثينديك" ضمن مساعد الإثبات "ليسا" (Lisa)، مما يتيح تكتيك تحقق من الأنواع ينتج براهين ويستفيد من قواعد المساواة والتعويض المجموعاتية القياسية للاستنتاج الآلي.
تقترح هذه الورقة نهجاً للتطبيع يحافظ على الدلالات، حيث يقوم بتحويل سياسات ODRL المعقدة إلى نماذج دنيا تقتصر على الأذونات مع قيود مبسطة، مما يتيح مقارنة السياسات بكفاءة من خلال فحوصات الهوية الهيكلية المباشرة.
تقدم هذه الورقة Delta1 مع LLM، وهو إطار عمل عصبي-رمزي يجمع بين توليد النظريات الحتمي ذي الوقت متعدد الحدود لـ Delta1 (مولد النظريات الآلي) مع النماذج اللغوية الكبيرة لإنتاج استدلال موثوق وقابل للتدقيق ومفسر طبيعياً عبر مجالات حرجة مثل الرعاية الصحية والامتثال.
تُثبت هذه الورقة أن دلالات تمديد القاعدة لـ "ساندكفيست" للمنطق القضايا الحدسي تقبل تفسيراً حوسبياً بنائياً، حيث يتوافق الدعم في قاعدة ثابتة تماماً مع البحث عن البراهين في برنامج منطق "هاروب" الوراثي من الدرجة الثانية.
تقدم هذه الورقة خوارزمية ديناميكية تتيح وصولاً مباشراً ومرتباً في زمن لوغاريتمي إلى إجابات استعلامات المنطق من الدرجة الأولى أحادي الموناد (MSO) على كل من السلاسل غير المضغوطة والسلاسل المضغوطة باستخدام برنامج الخط المستقيم (SLP)، مع دعم التحديثات الفعالة للتمثيل المضغوط.
تقدم هذه الورقة التحقق من الخصائص المتينة، وهي طريقة تركيبية وقابلة للتنفيذ تحدد ما تلتزم به سياسة التحكم في الوصول غير المكتملة أو المتطورة بغض النظر عن التوسعات المستقبلية، وذلك عبر اختزال مشكلة التحقق إلى البحث عن إثبات في البرمجة بالمنطق من الدرجة الثانية.