1215 ورقة بحثية
تُثبت هذه الورقة أن التخلص من مُكمِّم كلي واحد في البنى التلقائية يتطلب بطبيعته تضخماً ذا أسٍ مزدوج، مما يثبت أن مشكلة تقرير الفراغ للغة الناتجة هي كاملة بالنسبة لـ EXPSPACE، وتضع حدوداً دنيا جديدة لأجزاء من حساب بوشي.
تعمل هذه الورقة على تحسين تقنية الرسم البياني من النوع الموزون لإثبات توقف أنظمة تحويل الرسم البياني من نوع الدفع المزدوج (DPO) عن طريق زيادة قدرتها، وتعميمها على فئات أخرى، واستيعاب مختلف امتدادات الـ DPO الموجودة في الأدبيات.
تثبت هذه الورقة أن مجموعات الرسوم البيانية تكون قابلة للتعريف بـ CMSO وقابلة للتحليل السياقي إذا وفقط إذا كانت مجموعات معترف بها ذات عرض شجري محدود، قابلة للتحليل عبر تحويلات تعريفية إلى أشجار الاشتقاق، أو صوراً لمجموعات شجرية معترف بها تحت تحويلات تعريفية، وذلك من خلال توحيد التوصيفات المنطقية للغات الرسوم البيانية مع النتائج المتعلقة ببناء التفككات الشجرية المثلى.
تقترح هذه الورقة نهجاً جديداً لإعادة كتابة منطق الخط الزمني الخطي (LTL) للتحقق التركيبي من مكونات البرمجيات غير المتزامنة التي تتفاعل عبر منافذ البيانات، وهو نهج يعالج المسارات اللانهائية والمنتهية عن طريق تحويل الخصائص المحلية إلى خصائص عالمية مع الحفاظ على التكافؤ الدلالي وتحسين حجم الصيغة.
تقدم هذه الورقة توصيفاً كاملاً للغات -المنتظمة الموضعية عبر أوتوماتا التكافؤ، مما يثبت قابليتها للتقرير في وقت حدودي، وخصائص الرفع المختلفة، وإغلاقها تحت عملية الاتحاد، وبذلك تحل حدسية كوبشينسكي لحالة -المنتظمة.
تعمم هذه الورقة تفسير لغات الاستدعاء بالقيمة (call-by-value) ذات فضاءات الدوال ذات التأثيرات من المونادات القوية إلى المونادات المُعلمة (parameterized monads)، وبذلك تُصنف الحراسة (guardedness) كخاصية فئوية جوهرية للبرامج بدلاً من كونها مجرد محمول على فئة.
تقدم هذه الورقة "أوبراد" (operad) من مخططات التوصيل الموجهة المعتمدة لتمكين تركيب الأنظمة اللحظية مثل آلات "ميلي" (Mealy machines) ومخططات التدفق والمخزون المحددة بمعلمات، مما يوفر إطاراً جبرياً رسمياً وتشاكلاً دلالياً يربط هذه المخططات بآلات "ميلي".
تثبت هذه الورقة صراحةً أن الحجم الأمثل للدائرة يتغير بمقدار لا يتجاوز تحت اضطرابات جدول الحقيقة، مما يوسع الحد ليشمل مسافات هامينج العامة ويتحقق من إحكامه عند من خلال تحليل استقصائي قائم على مسألة الإرضاء (SAT).
تقدم هذه الورقة إطار عمل عام يوسع عملية تجميع المعرفة لتشمل "الرضا مع النظريات" (Satisfiability Modulo Theories - SMT) عبر دمج الصيغ المدخلة مع تمثيلات نظرية مسبقة الحساب لتمكين الاستعلام بأسلوب قضايا المنطق (propositional-style) في وقت حدودي على نماذج d-DNNF المجمعة.
تقدم هذه الورقة إطارًا عامًا يضمن قابلية التقرر في وقت حدودي لجزيئات النفي الثابت لنظريات المنطق من الدرجة الأولى، مبرهنةً على فعاليته من خلال إثبات أن حساب بريسر الضعيف والنظريات المقيدة ذات الصلة قابلة للتقرير بكفاءة، وذلك على النقيال من صعوبة (NP-hard) للجزيئات الأكثر تقييدًا من حساب بريسر الكامل.