1215 ورقة بحثية
تُنشئ هذه الورقة تضميناً عكسياً للترتيب لدرجات تورينج في درجات آرثر-نيموي-ميرلين، مما يُعرّف فئة جديدة من "درجات كوتورينج" ويحلل علاقتها من حيث الترتيب مع درجات تورينج المضمنة طبيعياً ضمن هذا الإطار المعمم.
تقدم هذه الورقة PRODSAT-QSAT، وهي خوارزمية بأسلوب CDCL تحدد قابلية إرضاء نماذج quantum -SAT من خلال البحث في كرة بلوخ مقسمة واستخدام محلل نظرية هندسية لتوليد بنود صراع سليمة تثبت عدم قابلية الإرضاء لحالة المنتج (product-state).
تقترح هذه الورقة امتداداً جديداً قابلاً للمعالجة لمنطق الوصف EL، والذي يدمج شكلاً مُضعّفاً من النفي لتمثيل المعرفة الطبية الحيوية السلبية، ويتحقق ذلك من خلال إدخال دلالات فئوية للمنشئات المنطقية والتخلي انتقائياً عن خصائص محددة مسؤولة عن عدم القابلية للمعالجة مع الحفاظ على قدرة تعبيرية أكبر من منطق EL القياسي.
تُثبت هذه الورقة أن حساب بيانو يمكن ترميزه في جزء أدنى من منطق الفصل يحتوي فقط على محمول "يشير إلى" الحدسي، والصفر، ودالة التابع، مما يثبت عدم قابلية القرار للصحة في هذا الجزء ويُظهر قدرته على التعبير عن خصائص معقدة مثل اتساق النظام وعدم التوقف.
تقدم هذه الورقة إطار عمل للتحقق الرسمي باستخدام أدوات حل "نظريات القابلية للإرضاء" (SMT) للتحقق بصرامة من الاتساق الفيزيائي وفرضه في نماذج تعلم الآلة القائمة على الأشجار للتنبؤ بالمخاطر الجيوتقنية، مما يكشف عن مقايضة مستمرة بين دقة التنبؤ والالتزام بمواصفات السلامة، مع إثبات أن التفسيرات اللاحقة لا يمكن أن تكون بديلاً للضمانات الرسمية الشاملة.
تقدم هذه الورقة ACTORCHESTRA، وهو إطار عمل للتحقق في وقت التشغيل للغة Erlang يتتبع تلقائياً العلاقات السببية عبر تفاعلات الممثلين المتعددة من خلال حقن الكود، ويوفر لغة المواصفات WALTZ للكشف عن انتهاكات سلوكية معقدة مع الحد الأدنى من التعديل على النظام.
يقترح المؤلفون لغة مجال محددة ذات أنواع تعتمد على النوع (dependently typed) مدمجة في لغة إدريس (Idris) لالتقاط "قواعد الأبعاد" في الفيزياء الرياضية رسميًا، مما يتيح الصياغة الرسمية الدقيقة للمفاهيم الأساسية مثل التحليل البعدي ونظرية بكنغهام باي (Buckingham's Pi theorem)، مع جسر الفجوة بين علوم الحاسوب والنمذجة الفيزيائية.
تُثبت هذه الورقة أن قابلية الإشباع لـ HyperLTL من الدرجة الثانية، وقابلية الإشباع في الحالة المحدودة، والتحقق من النموذج، مكافئة للحقيقة في الحساب من الدرجة الثالثة، مع تحليل كيفية تغيير تقييد التكميم إلى شظايا محددة أو اعتماد دلالات العالم المغلق لحدود التعقيد هذه إلى مستويات ضمن الحساب من الدرجة الثانية أو التسلسل التحليلي.
تعمم هذه الورقة النتائج الحالية لبناء بروتوكولات واجهة ذات إنهاء ضعيف عبر اشتقاق فئة من العملاء المتوافقين من مواصفات الخادم باستخدام علاقة انعكاس جزئي، وتبرهن على التطبيق العملي لهذه النظرية من خلال أداة مفتوحة المصدر.
تقدم هذه الورقة طريقة مبتكرة لإيجاد المستنتجات في المنطق الكلاسيكي تعتمد على نهج قائم على التفنيد وتستخدم نسخة غير ثنائية من حل النزاعات كآلية أساسية لها.