1215 ورقة بحثية
تثبت هذه الورقة أن تراتبية مبادئ حمامة الطير اللانهائية، عند تقييدها بمستويات مختلفة من التراتبية الحسابية، هي تراتبية صارمة فوق عبر توظيف بناء تحكم في القفزة المتكررة وتحليل تبعاتها من الدرجة الأولى من منظورات نظرية الحوسبة والرياضيات العكسية.
توسع هذه الورقة إطار إثبات التلاقي في إعادة الكتابة بموجب علاقة تكافؤ ليشمل الأنظمة الشرطية من خلال تقديم ثلاثة أنواع محددة من الأزواج الشرطية —الأزواج الحرجة الشرطية القائمة على المنطق، والأزواج المتغيرة الشرطية البارامترية، والأزواج الشرطية الهابطة— لتحديد معايير نهائية للتحقق من أو دحض التلاقي-E في أنظمة مثل Maude.
تُبين هذه الورقة أن ليست كل اللغات المنتظمة قابلة للتعريف في المنطق من الدرجة الأولى FC، وتوفر توصيفاً قابلاً للتقرير للغات المنتظمة القابلة للتعريف في FC باستخدام معايير جبرية، وآلية، وتعبيرات منتظمة موجزة.
يُعد CircuitProver إطار عمل وكيلًا (agentic) يعتمد على لغة Lean 4، يقوم بأتمتة التحقق من الأجهزة عبر ترجمة التصميمات والمواصفات ذات المعلمات إلى نماذج قابلة للتنفيذ، وبناء براهين مدققة آليًا بشكل تكراري، وتلخيص هذه النتائج في مكتبة قابلة لإعادة الاستخدام تعمل على تحسين كفاءة ونجاح البراهين بشكل كبير مقارنة بالوكلاء التقليديين.
تُقدم هذه الورقة تقريراً عن مشروع مستمر للتحقق الصوري من كتاب "الاحتمالية نظرية القياس" (Measure-Theoretic Probability) باستخدام مبرهن النظريات "لين" (Lean)، بهدف إنشاء رفيق مُتحقق آلياً يربط بين نصوص الكتاب ومكتبة "ماث ليب" (Mathlib) لتعزيز التحقق الرياضي، وتوضيح الافتراضات، ودعم الرياضيات المعتمدة على الذكاء الاصطوتناعي بشكل موثوق.
تُبين هذه الورقة أن أنواع الامتداد، التي توحد مفاهيم متنوعة مثل أنواع المسار وآليات التفكيك المحكوم، يمكن تعريفها ضمن نظرية النوع ثنائية المستوى دون بديهيات أو نماذج جديدة، مما يثبت قواعدها كنظريات، ويؤكد تحفظ عملية اللصق الكيوبي (cubical gluing) على مبدأ التكافؤ (univalence)، ويقدم مساراً لحل المشكلة المفتوحة المتعلقة بما إذا كانت نظريات النوع الكيوبية محفوظة فوق نظرية النوع هوموتوبي (HoTT) المرجعية.
تتقصى هذه الورقة مشكلة تعلم أشكال SHACL العودية في جزء ELI من منطق الوصف من خلال أمثلة عقد موجبة وسالبة، حيث تضع حدوداً عليا زمنية أسية محكمة لحسابات الوجود والملائمة الأكثر تحديداً، مع تحديد حلول زمنية متعددة الحدود لحالات خاصة.
تقدم هذه الورقة "تحديث الاعتقاد الانتقائي المحدود بالمصداقية"، وهو إطار عمل مبتكر يعزز نماذج تحديث الاعتقاد القياسية من خلال تحويل المدخلات المعرفية إلى بدائل أضعف تعتمد على المصدر للسماح بالقبول الانتقائي للأجزاء الموثوقة فقط من المعلومات المركبة، مما يوحد ويعمم بشكل صارم النهجين القائمين على المصداقية المحدودة وكاتسونو-مندلزون.
تقدم هذه الورقة إطار عمل عالي الأداء لـ SAT منتج للبرهان، يحل حالة هيمنة الملكة لـ التي كانت مفتوحة سابقاً ويصحح التعداد لـ من خلال الاستفضاء في ترميز مستنبط هندسياً، وكسر التماثل، ومسار تحقق موحد لضمان صحة قابلة للتحقق بشكل مستقل.
تُثبت هذه الورقة أن الـ setoids المعروضة ضمن نظرية النوع المقصود (المصاغة في Safe Agda) يمكن أن توفر دلالات لنظرية النوع الامتدادي مع الأكوان، مما يثبت اتساق الأخيرة كاستنتاج مباشر.