1215 ورقة بحثية
تقدم هذه الورقة المنطق الديناميكي القضاياي العملياتي (OPDL)، وهو إطار عمل معمم يتغلب على قيود المنطق الديناميكي التقليدي في نمذجة التزامن من خلال فصل البرامج عن آثارها واستخدام دلالات عملياتية معلمية، مدعومة ببرهان حذف القطع جديد لحساب تسلسلي غير جيد التأسيس.
تقدم هذه الورقة الفضاءات الطوبولوجية الملحقة بالحلقات شبه المجموعية لتوسيع منطق الدليل الطوبولوجي عبر صيغ نمطية مفهرسة بالموارد، مما يتيح الاستدلال الصوري للحالات المعرفية تحت قيود محددة للوقت أو الذاكرة أو ميزانية الطاقة مع توفير صياغات بديهية تامة وصحيحة.
إن COBALT-TLA هو حلقة تحقق عصبية-رمزية تدمج نموذج لغوي كبير مع أداة فحص نماذج TLA+ في دورة تغذية راجعة مؤتمتة لاكتشاف ثغرات جسور السلاسل المتعددة بكفاءة، بما في ذلك فئات الهجمات غير المتوقعة، وذلك باستخدام آثار خطأ حتمية لتوجيه توليد المواصفات الرسمية.
تقدم هذه الورقة إطاراً بديهياً شاملاً لقياس التشابه في حجج المنطق من الدرجة الأولى عبر اقتراح نموذج بارامتري رباعي المستويات يدمج نماذج لغوية حساسة للنحو مع أوزان سياقية لمعالجة أوجه القصور في النهج القضايا المعتادة.
تُطوّر هذه الورقة البحثية المُصاغة بلغة Lean 4 نموذج - الهوموتوبي لـ -حساب غير المقيّد، وذلك عبر إثبات أن حزمة تماسك "بذرة أمامية" (front-seed) دنيا تكفي لاستعادة النظريات الدلالية الرئيسية، ومن خلال تقديم صيغ عالمية صريحة ومحققة بالكامل لعمليات التجسيد (reify)، والانعكاس (reflect)، والتطبيق (application) مع هويات إحداثية دقيقة.
تتقصى هذه الورقة مدى تعبير منطق النقطة الثابتة مع العدّ الموسع بواسطة الاختيار المتماثل الملحوظ ومعامل التفسير، مبرهنةً أن الأخير يزيد من القوة عبر الإخفاق في الانغلاق تحت تفسيرات المنطق الأول (FO-interpretations)، وأن تداخل معاملات الاختيار المتماثل الملحوظ يعزز التعبيرية على رسوم بيانية من نوع (CFI).
يقدم هذا البحث منطقاً ميتا-نموذجياً (meta-modal logic) يتضمن جهة (modality) جديدة للقياس الكمي على الحالات المتشابهة بنيوياً (bisimilar states)، حيث يثبت أن التشابهات البنيوية قابلة للتعريف ضمن اللغة، ويقدم صياغة استنباطية (axiomatization) سليمة وكاملة، ويثبت أن مسألة القابلية للإرضاء (satisfiability) هي من فئة PSPACE-complete عبر الترجمة إلى المنطق الموجه القياسي، ويتحقق من جميع النتائج باستخدام Isabelle/HOL.
تقدم هذه الورقة البحثية "المجادلة القائمة على الافتراض المقيد" (CABA)، وهو إطار عمل جديد يوسع نظام "المجادلة القائمة على الافتراض" (ABA) القياسي من خلال دمج متغيرات مقيدة عبر مجالات غير محدودة للتغلب على قيود التمثيلات القائمة على العناصر الأرضية فقط، مع تعريف دلالات غير أرضية تعمم دلالات نظام (ABA) الحالي تعميماً محافظاً.
تقدم هذه الورقة عائلة من المعايير المرجعية القابلة للتوسع والتحقق ذات الحلول المزروعة لمحللات SAT وتحسين إيزينج (Ising optimization)، والمستمدة من قيود تحليل الأعداد الصحيحة، والتي تُظهر نمواً أسياً في وقت التشغيل بالنسبة لطول البتات الخاصة بالعوامل.
تقدم هذه الورقة البحثية LTLF، وهو منطق زمني مبتكر مزود بمكممات نمطية حساسة للقياس ودلالات من طراز كريبكي للتعبير عن خصائص تكرار سلاسل الأحداث ومراقبتها والتنبؤ بها رسميًا، مما يسد الفجوة بين الاستدلال المنطقي والملاحظة التجريبية في الأنظمة الكمية.