💻 computer science
Proof Identity and Categorical Models of BV
تؤسس هذه الورقة مفهومًا لهوية البرهان لمنطق BV بناءً على التدفقات الذرية وتستخدمه لتعزيز تعريف فئات BV، مما يثبت سلامتها فيما يتعلق بالمنطق.
💻 Category
cs.LO
1215 ورقة بحثية
💻 computer science
Partially Finite Model Reasoning in Description Logics Extended Version
تقدم هذه الورقة مفهوم النماذج شبه المنتهية في منطق الوصف لتوحيد الاستدلال المحدود واللانهائي، حيث تثبت أن استلزام الاستعلام الاتصالي للمنطق S مع مفهوم منتهٍ متميز هو قابل للتقرير في زمن 2-EXPTIME، وتوضح تطبيقه على احتواء الاستعلام مع المحمولات المغلقة.
💻 computer science
Positional Properties in Temporal Logic
تتقصى هذه الورقة الخصائص الموضعية في التوليف التفاعلي القائم على الألعاب، حيث تُثبت قابليتها للتعبير في المنطق الزمني الخطي، وتضع الشروط الضرورية والكافية للموضعية، وتثبت القيود المفروضة على إغلاقها البولياني، وتستكشف الآثار المترتبة على الأجزاء القابلة للمعالجة من المنطق الزمني للوقت المتناوب.
💻 computer science
Verification of Neural Networks (Lecture Notes)
تقدم هذه الورقة ملاحظات محاضرة تقدم مقدمة نظرية للتحقق من الشبكات العصبية، تغطي بنيات مثل الشبكات الأمامية، والشبكات العصبية المتكررة، والمحولات، إلى جانب لغات المواصفات والتقنيات الخوارزمية.
💻 computer science
Fair Vertex Problems Parameterized by Cluster Vertex Deletion
تثبت هذه الورقة أنه في حين أن المسائل القابلة للتعريف بـ MSO العادلة تكون عموماً صعبة من فئة W[1] عند تمثيلها بمعلمة عدد حذف رأس العنقود، إلا أنها تقبل خوارزميات قابلة للحل في وقت ثابت بمعلمة (FPT) تحت شروط كافية محددة تشمل مختلف مسائل الرسوم البيانية العادلة الطبيعية مثل غطاء الرؤوس العادل ومجموعة الهيمنة العادلة.
🔢 mathematics
Hofmann-Streicher lifting of fibred categories
مستلهماً من التحليل الدالي لـ "أوودي" (Awodey) لرفع "هوفمان-شترايشر" (Hofmann-Streicher)، تُعرّف هذه الورقة نسخة نسبية من البناء باستخدام اللاحق شبه الملحق للتركيب البعدي مع "فيبرة" (fibration)، وتستخدم هذا الإطار لبناء "2-بيفيبرة" (2-bifibration) جديدة من الـ "فيبرات".
🔢 mathematics
From Copying to Corelations via Ancestry Partitions
تُبين الورقة أن خارج قسمة الـ PROP الحر المتولد بواسطة مولد ثنائي واحد، والمستخرج عبر دالة السلف (ancestry functor)، يكافئ الـ PROP الخاص بالكومونويدات التبادلية غير المرافقة للوحدة (non-counital cocommutative comonoids)، مع وضع هذه النتيجة ضمن السياق الأوسع للارتباطات (corelations) وفئات المخططات البيانية الفائقة (hypergraph categories).
🤖 machine learning
Verifying Quantized GNNs With Readout Is Decidable But Highly Intractable
تقدم هذه الورقة لغة منطقية لتوصيف الشبكات العصبية الرسومية ذات التجميع والدمج المكمم مع القراءة العالمية (ACR-GNNs)، وتثبت أن التحقق من هذه النماذج هو مسألة (co)NEXPTIME-complete، مما يوضح أنه بينما يصعب التحقق منها حاسوبياً، إلا أنها تظل خفيفة الوزن ودقيقة في الممارسة العملية.
🤖 machine learning
Towards Understanding the Expressive Power of GNNs with Global Readout
تتقصى هذه الورقة القدرة التعبيرية لشبكات الرسم البياني العصبية (GNNs) القائمة على تمرير الرسائل من خلال إثبات أن التفاعل بين التجميع المحلي والقراءة العالمية يسمح لها بتجاوز القدرة التعبيرية المنطقية لمنطق ، مع تحديد قيود محددة على التجميع أو درجة الرسم البياني التي تعيد إمكانية التوصيف عبر المنطق الجهوي المتدرج مع العد العالمي.
💻 computer science
From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
تُعد ProofLoop أداة وكيل (ReAct) مدعومة بالأدوات، تعمل على أتمتة توليد تأكيدات SystemVerilog (SVA) من اللغة الطبيعية عبر الجمع بين استرجاع سياق التصميم المعزز بالاسترجاع وعملية صقل تكرارية تتضمن وجود مُحلل في الحلقة باستخدام أدوات التحقق الرسمي.