1215 ورقة بحثية
تتقصى هذه الورقة منطق المعرفة المشتركة الحدسي (ICK)، حيث تقدم استنباطات صائبة وكاملة وحسابات متتاليات حلقية لتوسعات جهوية متنوعة، مع إثبات خاصية النموذج المحدود، والقابلية للتقرير، والتعقيد الزمني الأسي للبحث عن البراهين والصلاحية.
تقدم هذه الورقة صياغة بنيوية لنظرية النوع مع المحو بوصفها نظرية جبرية معممة من الدرجة الثانية (SOGAT) تميز بين البيانات ذات الصلة بوقت التشغيل والبيانات غير ذات الصلة عبر تمييز طوري، مؤسسةً نماذجها الدلالية، وتحفظيتها على نظرية مارتن-لوف للأنواع، وصحتها لاستخراج الكود إلى حساب لامدا غير النمطي.
تتقصى هذه الورقة القيود والظروف المحددة التي يصنف ضمنها بناء مخروط سيربينسكي الخرائط الجزئية داخل النماذج الاصطناعية للفضاء استناداً إلى نظرية النوع التماثلي، وتحدد أكبر عالم فرعي تتحقق فيه هذه الخاصية باعتباره توطيناً ميسراً يقع بدقة داخل أنواع سيغال، وتوسع هذه النتائج لتشمل أسطوانات التعيين.
تُثبت هذه الورقة أن نسخة أضعف من بديهية التماثل (univalence axiom)، والتي تُسمى "التماثل الفئوي" (categorical univalence)، لا تستلزم بديهية امتداد الدوال (function extensionality) من خلال تحليل بناء نموذج فون غلينن متعدد الحدود، والذي يُنتج نماذج لنظرية نوع مارتن-لوف تحقق التماثل الفئوي بينما تفند امتداد الدوال.
تقدم هذه الورقة طرقاً مبسطة وفعالة حاسوبياً لبناء عمليات فك الحلقات (deloopings) للمجموعات المعروضة في نظرية النوع المتماثل (homotopy type theory) باستخدام مجموعات التوليد، وتُقدم إطار عمل لمتعدد الروابط ثنائي الأبعاد (2-polygraph) من منظور نظري للأنواع لتحليل الأنواع الاستقرائية العليا الناتجة ومخططات كايلي (Cayley graphs) والمعقدات المرتبطة بها، مع تطويرات تمت صياغتها رسمياً في لغة Cubical Agda.
تقدم هذه الورقة نهجاً هرمياً للتحسين التكيفي يسرع عملية تخليق السياسات في عمليات ماركوف لاتخاذ القرار واسعة النطاق من خلال الاستهداف الديناميكي للمناطق الهشة، محققةً تسريعًا يصل إلى ضعفي السرعة مقارنة بـ PRISM مع الحفاظ على دقة تقارب المثالية.
تُثبت هذه الورقة الـتطبيع القوي لحساب التأثيرات غير المتزامنة (asynchronous effects calculus) —سواء في شكله النقي أو مع السلوك التكراري المتحكم به— عبر توسيع نهج الرفع الخاص بـ ليندلي وستارك، مع التحقق من جميع النتائج رسميًا في لغة Agda.
تقترح هذه الورقة منطقاً طوبولوجياً جديداً لـ "المعرفة الاستقرائية المشتركة" يُمكّن مجتمعاً من العلماء المنعزلين ذوي القدرات المحدودة على التراجع من تنسيق أحكامهم والتقارب نحو فرضية حقيقية دون حدوث إيجابيات كاذبة، وذلك عبر صياغة حسابية لتفسير لويس للمعايير الاستقرائية المشتركة وتحمل التبديل.
تقترح هذه الورقة امتداداً متسقاً لنظرية النوع المقصود (intensional type theory) مع نوع كبير من الأحجام والمسورات البارامترية لبناء الأنواع الاستقرائية والتعاونية، متجاوزةً بذلك قيود النهج السابق وعدم اتساق تنفيذ الأنواع ذات الأحجام (sized types) الحالي في لغة Agda.
تتقصى هذه الورقة التعقيد الحسابي لملاءمة أنطولوجيات (Horn DL) (تحديداً EL وELI مع وجود أو عدم وجود المفهوم الأدنى) لأمثلة الـ ABox والاستعلامات البوليانية، حيث تُصنف وجود الأنطولوجيات الملائمة عبر المحاكاة وتثبت أن المشكلة تتراوح بين زمن متعدد الحدود (PTime) للاستعلامات الذرية إلى -complete للاستعلامات الاقترانية، أو ExpTime-complete للاستعلامات الاتحادية، على التوالي.