cs.LO

Automatic Generation of Polynomial Symmetry Breaking Constraints

تقترح هذه الورقة طريقة جبرية للتوليد التلقائي لعائلة عشوائية من قيود كسر التماثل متعددة الحدود بناءً على متعدد حدود أساسي ومجموعة تبديل محددة، مبرهنةً من خلال دراسة حالة لتعبئة الصناديق أن القيود التربيعية البسيطة فعالة بشكل خاص في تقليل أوقات حل البرمجة الصحيحة.

SAT Encodings for Bandwidth Coloring: A Systematic Design Study

تقدم هذه الورقة دراسة منهجية وإطاراً موحداً لست طرق لترميز (SAT) لمسألة تلوين عرض النطاق، مبرهنةً أن ترميزات الكتل (block encodings) مقترنة بالحل التدريجي وكسر التماثل تحقق أداءً هو الأفضل حالياً وتحل حالات كانت مستعصية سابقاً إلى المثالية المثبتة.

Impredicativity in Linear Dependent Type Theory

تقدم هذه الورقة بناءً رسميًا لنموذج تحقق لنظرية الأنواع التبعية الخطية باستخدام جبر توافقي خطي، حيث تقدم كونًا غير محدد وتضع قواعد محددة تتيح ترميز الأنواع الاستقرائية الخطية.

On the role of connectivity in Linear Logic proofs

تقدم هذه الورقة شرطاً هندسياً على بنى البراهين غير المحددة النوع (untyped proof-structures) يحول خاصية اتصال ضرورية معروفة إلى معيار كفاية للصحة لشرائح محددة من المنطق الخطي، مما يتيح استعادة براهين حساب السيكوينت (sequent calculus) وتوصيف تبديلات القواعد.

Neuro-symbolic AI for Predictive Maintenance (PdM) -- review and recommendations

تستعرض هذه الورقة أوجه القصور في النهج المعتمدة كلياً على البيانات والنهج التقليدية القائمة على المعرفة في مجال الصيانة التنبؤية خلال السنوات الخمس الماضية، محاجةً بضرورة اعتماد الذكاء الاصطناعي العصبي الرمزي لدمج التعلم العميق مع المنطق الرمزي من أجل أنظمة صناعية أكثر دقة وقابلية للتفسير ومتانة.

Do It for HER: First-Order Temporal Logic Reward Specification in Reinforcement Learning (Extended Version)

The proof theory and semantics of second-order (intuitionistic) tense logic

تثبت هذه الورقة تكافؤ التعريفات البديهية، والبرهانية، والنموذجية لمنطق الزمن الحدسي من الدرجة الثانية، مظهرةً أن معامل الماسة يمكن اشتقاقه من صناديق عبر التكميم من الدرجة الثانية، وتثبت تمام وقابلية قطع حساب متتاليات موسوم لمتغيرات حدسية وكلاسيكية.

Fine-tuned LLM-based Code Migration Framework

تقدم هذه الورقة إطار عمل لنماذج لغوية كبيرة مضبوطة بدقة تعمل بفعالية على أتمتة هجرة الأنظمة القائمة على لغة SQL من Oracle PL/SQL إلى PostgreSQL عبر دمج تقنيات الهندسة التقليدية، وتحليل الأخطاء التكراري، وملاحظات الخبراء لتقليل الأخطاء النحوية بشكل كبير وتحسين منطق قواعد البيانات.

On the Reachability Problem for One-Dimensional Thin Grammar Vector Addition Systems

تؤسس هذه الورقة نظام برمجة صحيحة فعالاً لأنظمة إضافة المتجهات القواعدية الرقيقة أحادية الأبعاد (thin 1-GVAS) من خلال تعميم تقنيات التفكيك الخاصة بأنظمة إضافة المتجهات (VASS) على أشجار الاشتقاق القواعدي، مما يؤدي إلى استنباط حد علوي $\mathbf{F}_{2k}$ أكثر إحكاماً لتعقيد مسألة الوصول الخاصة بها بناءً على مقياس المؤشر.

Color Refinement for Relational Structures

تقدم هذه الورقة خوارزمية "تكرير الألوان العلاقاتي" (RCR)، وهي تعميم لخوارزمية "تكرير الألوان" الكلاسيكية لتشمل البنى العلاقاتية التعسفية، وتثبت إمكانية تنفيذها في زمن قدره $O(N \log N)$ مع توصيف قدرتها التمييزية بدقة من خلال التماثلات من البنى العلاقاتية اللاتكرارية والجمل في الجزء المحروس من المنطق من الدرجة الأولى مع مكممات العد.