1215 ورقة بحثية
تقدم هذه الورقة أنظمة عداد إعادة الضبط المتداخلة (NRCS) كامتداد لأنظمة العدادات المتداخلة، حيث تثبت أن مسألة قابلية التغطية الخاصة بها هي -complete للعدادات من الرتبة-، وبذلك تؤسس أول تسلسل هرمي طبيعي للمسائل الكاملة لهذه الفئات التعقيدية مع تحسين الحدود العليا لمختلف التطبيقات في معالجة XML، وتحويل الرسوم البيانية، والتحقق المحدّد بالمعلمات.
تقدم هذه الورقة QSeqSim، وهو محاكي رمزي متكامل مع Qiskit يتيح المحاكاة الفعالة للبرامج الكمومية التي تحتوي على حلقات تكرار (while-loops) عن طريق ترجمتها إلى دوائر متسلسلة واستخدام العد الموزون للنماذج القائم على مخططات قرار بوليان (BDD) لحساب احتمالات القياس للمقارنات المرجعية واسعة النطاق ومتعددة التكرارات.
تقدم هذه الورقة البحثية ، وهي تعميم لإطار تعلم البند الموجه بالصراع (Conflict-Driven Clause Learning) إلى صيغ XNF التي تدعم الاستدلال التكافئي (parity reasoning) وتحاكي نظام برهان حدودياً، مما يظهر تحسينات كبيرة في الأداء مقارنة بالمحللات الموجودة على الاختبارات المعيارية التي تتضمن قيود التكافؤ.
تثبت هذه الورقة أن الجزء المحروس الممتد بعلاقات التكافؤ المتداخلة يحتفظ بخاصية النموذج المحدود ويكون قابلاً للتقرير بتعقيد من فئة TOWER-complete (أو -ExpTime-complete لعدد ثابت من العلاقات)، بينما تظهر أن تخفيف شرط التداخل أو السماح بالمساواة يجعل مسألة القابلية للإرضاء غير قابلة للتقرير.
تُرسخ هذه الورقة علاقة وثيقة بين إنهاء حلقات القيود الخطية أحادية المتغير على الأعداد الصحيحة ومتتاليات كولاتز المعممة، حيث تثبت أن إنهاء الحلقة قابل للتقرير في وقت متعدد الحدود بناءً على حدسية محددة حول هذه المتتاليات، بينما تُظهر أيضاً أن أي إجراء تقريري لمثل هذه الحلقات من شأنه أن يحل حالات مفتوحة من تلك الحدسية.
تقدم هذه الورقة منطقاً صورياً للأقنعة متجذراً في فلسفة كاستاڽدا الداخلية واللايبنيزية، حيث تؤسس لقواعد لغوية، ونظرية نموذج، ونظرية برهان تُعامل فيها العلاقات كمنظورات قصدية مشفرة ضمن حزم من الخصائص بدلاً من كونها روابط سببية خارجية، مما يعالج الظواهر فوق-القصدية ويقدم بديلاً متميزاً للدلالات القصديّة والكلاسيكية ودلالات المواقف.
تقدم هذه الورقة BitModEq، وهي تكتيك جديد في Lean يعمل على أتمتة براهين التكافؤ بين المتجهات الثنائية (bitvectors) والحقول المحدودة (finite fields) باستخدام ليمات النطاق وتحليل الحالات، متفوقاً بذلك على أدوات حل مشكلات التقييد (SMT solvers) الحديثة في التحقق من ترميزات دوائر براهين المعرفة الصفرية.
تقدم هذه الورقة خوارزميات ذات زمن ثابت وكفاءة عمل ضعيفة لتقييم الاستعلامات العلاقاتية على نماذج PRAM من نوع CRCW عبر الاستفادة من تقنيات المجموع التراكمي التقريبي والضغط، محققةً حدود عمل تبلغ للاستعلامات غير الحلقية، واستعلامات شبه الربط، واستعلامات الربط المثلى في الحالة الأسوأ تحت فرضيات بيانات مخففة.
تقدم هذه الورقة تسلسلاً هرمياً من المنطقات كاملة التقييم وذات التتابع الأيسر، تتراوح من المنطق الحر (Free) إلى منطق FEL الساكن (Static FEL)، مع توفير بديهيات كاملة لنسخها ثنائية القيم وثلاثية القيم باستخدام أشجار التقييم كأساس دلالي.
تقدم هذه الورقة حساب "فراكتيرم" (fracterm) للمروج الجزئية (partial meadows) باستخدام منطق الدائرة القصيرة ثلاثي القيم لتوفير صياغة صورية طبيعية للحقول ذات القسمة، مظهرةً أنه بينما لا يمكن للمنطق التعبير عن الطبيعة غير المعرفة للقسمة على صفر، فإن علاقة استتباعه هي شبه قابلة للحوسبة، وتؤدي توسيعات الخاصة به إلى مروج شائعة.