1215 ورقة بحثية
تقدم هذه الورقة إطار عمل جديداً للتحقق الموحد يوحد ويعمم مختلف التفسيرات المنطقية من خلال تجريد معالجة الصيغ الذرية والمسورات، مما يستوعب كلاً من المتغيرات الكلاسيكية والحديثة مثل تحقق كليين العددي وتحقق التحقق الكلاسيكي.
تقدم هذه الورقة نظريات جبرية معممة توفر توصيفات مجردة، غير معتمدة على القواعد النحوية، لنظرية نوع مارتن-لوف التي تتضمن كلاً من الأبراج الخارجية وتعدد الأشكال الكوني الصريح كنماذج أولية، مما يسلط الض dụng على بنيتها الفئوية عالية المستوى ويقدم رؤى ذات صلة بتخمين الأولية لفويفودسكي.
تقترح هذه الورقة نهجاً تربوياً لمساقات مقدمة في علوم الحاسوب يعطي الأولوية لتدريس تقنيات الإثبات الأساسية والبنى المجردة من خلال أمثلة ملموسة مثل "الاستقرار المتعدي" (transitive closure)، بدلاً من التركيز فقط على موضوعات تأسيسية محددة، وهو أسلوب مستوحى من التجربة التدريسية التعاونية للمؤلفين مع ستيفانو بيراردي.
تقدم هذه الورقة وتوضح ملاحظتين غير منشورتين لستيفانو بيراردي تتعلقان بدلالات الألعاب للمنطق الكلاسيكي.
تثبت هذه الورقة أن في نظرية الأنواع المعتمدة متعددة الأشكال النقية (P2)، لا يمكن تعريف أنواع القسمة البارامترية ومبادئ الاستقراء القوي، وأن مبدأ استمرارية الدوال ضروري تماماً لإثبات مبادئ الاستقراء، وذلك عبر بناء نماذج محددة تفشل فيها هذه المبادئ.
تثبت هذه الورقة أن التعقيد المنطقي للقابلية للإثبات في نظام إثبات الهبوط اللانهائي LKID-omega هو -complete من خلال إثبات تكافؤ الصلاحية في النماذج المصطلحية القياسية والنموذجية، وتوسيع محمول الحقيقة للغات ليشمل التعريفات الاستقرائية.
تتقصى هذه الورقة المحتوى الحسابي والقوة المنطقية لمعايير الانتظام، مبرهنةً قدرتها على الحساب الخوارزمي لأصفار الدوال المستمرة والمسارات في الأشجار اللانهائية، مع إثبات أنه لا يمكن لأي مبدأ غير معياري "أليف" أن يستبدل التراص بالترابط المتري في هذا السياق.
تقترح هذه الورقة منظوراً غير تقليدي حول حساب لامدا من خلال التركيز على فروع الأشجار بدلاً من الأشجار الكاملة، مما يؤدي إلى إعادة صياغة لتقليص بيتا بحيث يتم توسيع المصطلحات بحيث تحتوي شجرة المصطلح المُقلَّص على المصطلح الأصلي كشجرة فرعية.
تبسط هذه الورقة الفهم التاريخي للأنماط الرئيسية في أنظمة أنواع التقاطع من خلال تحديد ثلاث عمليات أولية لبناء اشتقاقات الأنواع وتصميم خوارزمية شبه آلية تحسب الأنماط الرئيسية لجميع حدود لامدا ذات الاستقرار القوي.
تقدم هذه الورقة الشبكات العصبية المنطقية الجهوية المستمرة (CMLNNs)، وهو إطار عمل يسمى "المنطق السائل" (Fluid Logic) يعمل على رفع الاستدلال الجهوي من البنى المنفصلة إلى المتشعبات المستمرة باستخدام المعادلات التفاضلية العشوائية العصبية لدمج القيود المنطقية مباشرة في تدريب الشبكة العصبية، مما يتيح حلولاً متسقة بنيوياً لمهام الاستدلال المعرفي، والزمني، والوجوبي دون الحاجة إلى معادلات حاكمة صريحة.