1215 ورقة بحثية
تقدم هذه الورقة إجراء قرار جديداً وسليماً لنظرية SMT للمصفوفات الامتدادية مع المصفوفات الثابتة التي تدعم نطاقات فهرسة تعسفية، متجاوزةً بذلك القيود السابقة المتمثلة في الحالات المحدودة أو اللانهائية، وتبرهن على فعاليتها من خلال التنفيذ في برنامج الحل Bitwuzla.
تعمم هذه الورقة البحثية العمل السابق حول المنطق المرتب عبر تقديم نظام من الجهات الملازمة التي تجمع بين منطقيات ذات خصائص بنيوية متفاوتة مثل التضعيف والتقليص، وتثبت أن حساب التتابعات الناتج يقبل حذف القطع وأن صياغة الاستنتاج الطبيعي الخاصة به تدعم التحقق من الإثبات القابل للتقرير.
تقدم هذه الورقة عقود حدود قابلة للتنفيذ لآثار الأحداث الصوتية المتناهية لتمكين القياس الدقيق لسلوكيات الحدود الزمنية، وتثبت من خلال تجارب على مجموعات بيانات متنوعة أن مقاييس التقييم القياسية غالبًا ما تفشل في اكتشاف إخفاقات حدودية محددة يمكن لهذه العقود تحديدها بشكل صريح.
تقدم هذه الورقة حساباً مطوراً قائماً على التراكب لتخليق برامج خالية من التكرار، وهو حساب مُثبت كونه سليماً وكاملاً، مما يضمن اكتشاف حل قابل للحوسبة كلما وجد.
تثبت هذه الورقة أن مسألة القابلية للإرضاء لمنطق جهوي يعبر عن تأكيدات "معرفة الكيفية" عبر خطط خطية هي مسألة (NP-complete)، وهي نتيجة تم تحقيقها من خلال ترجمة المسألة إلى المنطق الجهوي S5.
تقدم هذه الورقة دراسة حالة لصياغة مسألة "الجراد" (Grasshopper) من أولمبياد الرياضيات الدولي لعام 2009 باستخدام لغة Lean 4 عبر واجهة برمجة تطبيقات Aristotle، مما يوضح أنه بينما يمكن للذكاء الاصطناعي التحقق بنجاح من المكونات المحلية لاستراتيجية الإثبات، فإنه يواجه صعوبة حالياً في حل المسائل المتعلقة بالتدقيق الحسابي التوافقي الشامل المطلوب لإتمام المبرهنة الرئيسية.
تقترح هذه الورقة أول نهج مؤتمت باستخدام برمجة مجموعة الإجابات (ASP) لتحسين التخطيط طويل الأمد لشبكة الطاقة، مما يثبت فعاليتها في التعامل مع القيود الطوبولوجية والتركيبية المعقدة من خلال تجارب على كل من البيانات الاصطناعية والواقعية.
تثبت هذه الورقة أن أي حالة من حالات مشكلات تحقيق القيود (CSP) يمكن تقليل كثافتها إلى حجم يتناسب مع عدم تكرارها (أو طول السلسلة في الحالات الموزونة) من خلال إثبات أن البنود الزائدة كافية للتقريب، وهي نتيجة تم تحقيقها عبر تطبيقات مبتكرة لطريقة الإنتروبيا وتقنيات نظرية الترميز التي تحدد بدقة حدود تقليل كثافة مشكلات تحقيق القيود (CSP).
تثبت هذه الورقة أن مسألة القابلية للإشباع لمنطق الإغلاق المتعدي للنفي المحروس (GNTC) هي مسألة كاملة لتعقيد 2ExpTime، وأن مسألة التحقق من النموذج الخاصة بها هي مسألة كاملة لتعقيد ، مما يحل تساؤلات التعقيد التي كانت مفتوحة سابقاً لكل من جزئية النفي الأحادي (UNTC) و.
تُثبت هذه الورقة أن الشجرة الصفائحية (laminar tree) المقابلة لنظام مجموعات صفائحي (laminar set system) يمكن إنشاؤها عبر تحويل المنطق من الدرجة الثانية أحادي المتغير (MSO transduction)، مما يحل مسألة مفتوحة لكورسيل (Courcelle) ويُمكّن من الاشتقاق القائم على منطق (MSO) لمختلف التفككات الرسومية التي كانت تتطلب سابقاً كميات عدّ (counting quantifiers)، مع استكشاف حدود محاكاة هذه الكميات ضمن منطق (MSO) على مثل هذه الأنظمة.