1215 ورقة بحثية
تقترح الورقة نظرية النموذج البنائي الفائق (UCMT)، وهي إطار عمل يستبدل الإرضاء المثالي بالبقاء الخصمي المحدود، حيث يتم التحقق من صحة البنى الجزئية المحدودة من خلال لعبة بين خصم يوجه تحديات قانونية وبناء يقدم إصلاحات، ويتم التصديق عليها في النهاية بواسطة قاضٍ رمزي.
تستخدم هذه الورقة أمثلة مضادة تم التحقق منها آلياً في نظام Isabelle/HOL لدحض ادعاء أوديفردي وغوميز بأن الانهيار الجهتي هو سمة جوهرية للنظريات القائمة على المُرشحات الفائقة، مبيّنةً بدلاً من ذلك أن الانهيار ينشأ من صرامة الإيجابية، مع تصحيح ادعاءين محددين أيضاً فيما يتعلق بنظرية غودل الرابعة وتمدد الإيجابية.
تقترح هذه الورقة منهجية جديدة للتحقق من صحة التعيينات الدلالية بين الأنطولوجيات التأسيسية المختلفة من خلال الاستفادة من التزاماتها الميتافيزيقية لإنشاء قيود الكاردينالية، وهو ما يتم إثباته من خلال دراسة حالة لتعيين IES إلى BFO وتشغيله عبر استعلامات SPARQL.
تنمذج هذه الورقة التنبؤ بالرمز التالي في الشبكات العصبية ذاتية الانحدار باستخدام المنطق الاستدلالي الحدسي وتناظر كوري-هوارد، حيث يتوافق توليد الرموز مع قاعدة الاستلزام (modus ponens) ومعالجة التسلسل مع تمديد البرهان البنائي، مما يؤدي في النهاية إلى اشتقاق بنية عصبية مكافئة للشبكات العصبية المتكررة الضربيه (multiplicative RNNs) والتحقق من خصائصها من خلال مبرهنات برمجية متخصصة.
تقدم هذه الورقة صياغة كاملة، ومحققة آلياً باستخدام لغة Lean 4، للتخمين القائل بأنه لا توجد دالة غير ثابتة مشتقة من دالة الهوية، والثوابت، وعمليات نقطية محدودة (الجمع، والضرب، والرفع إلى أس) ترسم كل عدد صحيح موجب إلى عدد أولي، مما يحول التخمين إلى هدف دقيق وقابل للتحقق بواسطة النواة لأنظمة الاستدلال الآلي.
تُثبت هذه الورقة مبرهنة عظمى بأسلوب ليندستروم لعرض ماروياما لاختبار الحقيقة الدقيقة لمنطق فيتينج الموّلد هينتينغ ذي القيم المتناهية، حيث تثبت أنه أقوى منطق تجريدي يستوفي شروط التراص، وخاصية اتحاد تارسكي، والثبات عبر التماثل، دون اشتراط الخطية أو وجود عنصر ذروة متميز.
تقدم هذه الورقة إطار عمل موحداً لتحليل الإنهاء يستفيد من استكمال كريج (Craig interpolation) لتوليد ثوابت انتقال جيدة الأساس، مما يتيح الإثبات المتزامن لكل من الإنهاء وعدم الإنهاء للأنظمة ذات الحالة اللانهائية بأداء يضاهي الأدوات المتطورة حالياً.
تقدم هذه الورقة عائلة من أنظمة الأنواع الحساسة للتدفق القائمة على "الكمية" (quantale) للمعلومات لفرض سياسات تدفق معلومات انفصالية، مبرهنةً أنه في حين تفشل النهج القياسية القائمة على الشبكة الجزئية (lattice) في التصديق بدقة على مثل هذه السياسات، فإن آلية منقحة تؤجل التخصيص إلى مستوى الحكم تنجح في استعادة السلامة والدقة عبر تجنب فقدان انفصال الفروع.
تقدم هذه الورقة صياغة رسمية كاملة في لغة Lean 4 لنظرية تمديدات الفئات (category dilatations) —وهي بناء يعدل الفئة عبر فرض تحليل مورفيزمات محددة بشكل فريد من خلال خرائط معطاة— إلى جانب قاموس منهجي يربط النظريات الرياضية بإعلانات Lean المقابلة لها.
تثبت هذه الورقة أن النماذج الدلالية لأنظمة الأنواع التي تتبع التكلفة المستهلكة والقدرة الكامنة، مثل -amor، تتميز جوهرياً بعلاقة تلازم بين دالات متدرجة تمثل التكلفة والقدرة الكامنة، وتبرهن على هذا الإطار من خلال ثلاث حالات ملموسة بما في ذلك نموذج جديد قائم على المجموعات المتقابلة (copresheaf).