🔢 mathematics
A nesting-free normal form for nested conditions in finite lattices of subgraphs
تقدم هذه الورقة شكلاً نموذجياً خالياً من التداخل لصيغة الشروط والقيود المتداخلة في سياق الشبكات الجزئية ذات المجموعات المحدودة.
💻 Category
cs.LO
1215 ورقة بحثية
💻 computer science
A formalization of System I with type Top in Agda
تقدم هذه الورقة صياغة صورية كاملة في لغة Agda لمتغير من النظام I ممتد بالنوع Top، بما في ذلك براهين صورية على التقدم والتقارب القوي.
💻 computer science
On the Decidability of Monadic Theories of Arithmetic Predicates
تتقصى هذه الورقة البحثية قابلية التقرير لنظريات الرتبة الثانية الأحادية للهياكل الحسابية التي تتضمن المتتاليات التكرارية الخطية والقوى، حيث تُرسخ نتائج جديدة غير مشروطة ومشروطة من خلال دمج تقنيات من الأنظمة الديناميكية، ونظرية الأعداد، ونظرية الأتمتة.
🔢 mathematics
Coslice Colimits in Homotopy Type Theory
تُوصّف هذه الورقة العلاقة بين النهايات المحدودة (colimits) المفهرسة بالرسوم البيانية في كون النوع (type universe) وبين النهايات المحدودة في الفئة المقطوعة (coslice colimits) ضمن نظرية النوعوطيا (Homotopy Type Theory)، حيث تقدم بناءً مُصمماً لإثبات أن الدالة الناسيّة (forgetful functor) تُنشئ النهايات المحدودة فوق الأشجار، وتُبين أن جميع النهايات المحدودة للأنواع المنقطة (pointed types) تحافظ على الاتصال من الرتبة ، مما يؤدي إلى إثبات أن الزمر العليا مغلقة تحت النهايات المحددة.
💻 computer science
Multi types and reasonable space
تقدم هذه الورقة نظاماً جديداً متعدد الأنواع يستخرج كلاً من تعقيدات الزمان والمكان لـ Space KAM من اشتقاقات النوع، مما يوفر توصيفاً نظرياً للأنواع لهذه النماذج التكلفية المعقولة لحساب لامدا.
💻 computer science
Tighter Bounds for Query Answering with Guarded TGDs
يُحسّن هذا البحث حدود التعقيد للإجابة على الاستعلامات في العالم المفتوح باستخدام قواعد الاشتقاق التبعية المحروسة (guarded TGDs) من خلال إثبات أن المشكلة قابلة للحل في زمن أسي (EXPTIME) عندما يكون رتبة التوقيع الجانبي محدودة، وفي زمن متعدد الحدود غير محدد (NP) عندما يكون كل من التوقيع الجانبي وعرض التبعية ثابتين، وذلك باستخدام متغير جديد لعملية الخطية ومطاردة مقيدة.
🤖 AI
From Knowledge to Conjectures: A Modal Framework for Reasoning about Hypotheses
تقدم هذه الورقة عائلة جديدة من المنطق الجهوي غير البديهي، وتحديداً و، والتي تصيغ الاستدلال التخميني من خلال الحفاظ على الحقائق المعروفة عبر البديهية C ضمن إطار دلالي غير ثنائي لتجنب الانهيار الجهوي، مع تقديم تفسير موحد للحالات المعرفية وعامل ديناميكي للانتقال بالتخمينات إلى الواقع.
💻 computer science
Determination of the fifth Busy Beaver value
تقدم هذه الورقة أول تحديد مُثبت رسميًا لقيمة "الرجل الكسول" الخامسة، ، والذي تم تحقيقه من خلال جهد تعاوني هائل عبر الإنترنت باستخدام مساعد الإثبات Coq لتحليل أكثر من 181 مليون آلة تورينج.
💬 NLP
Conflict-Aware Fusion: Mitigating Logic Inertia in Large Language Models via Structured Cognitive Priors
تقدم هذه الورقة البحثية "الدمج الواعي بالصراع"، وهو إطار عمل يستخدم بنية معالجة مزدوجة وأوليات معرفية مهيكلة للتغلب على "القصور الذاتي المنطقي" في النماذج اللغوية الكبيرة، مما يحقق دقة مثالية في مهام الاستدلال حتى في ظل وجود أدلة متناقضة واضطرابات هيكلية حيث تفشل النماذج القياسية تماماً.
💻 computer science
Can LLMs Perform Synthesis?
تقيم هذه الورقة أداء الأدوات الرمزية مقابل النماذج اللغوية الكبيرة (Qwen وGPT-5) عبر أربعة مجالات لتخليق البرامج، حيث وجدت أن الحلّالات الرمزية تحل باستمرار عددًا أكبر من الاختبارات المرجعية وتعمل بشكل أسرع من كل من النماذج اللغوية الكبيرة مفتوحة المصدر والرائدة، حتى عندما يتم تشغيل الأخيرة على أجهزة أكثر قوة.