1215 ورقة بحثية
تقدم هذه الورقة برهاناً آلياً جديداً لعدم القابلية للتقرير في مطابقة بيتا من الرتبة العليا في مثبت روك (Rocq Prover)، والذي يبسط عملية التحقق عبر ترميز نظام إعادة كتابة سلاسل معتمد، ويؤسس بناءً موحداً يربط بين عدم قابلية تقرير مطابقة بيتا، والتعريف اللامداوي، وإشغال نوع التقاطع.
تقدم هذه الورقة سير عمل عملي، ومحافظاً بطبيعته، لبناء تجريدات منفصلة للأنظمة السيبرانية الفيزيائية تضمن ضمانات تحقق سليمة من خلال معالجة العثرات الشائعة عبر عملية نمطية مكونة من أربع خطوات تتضمن تقسيم فضاء الحالة، وبناء الانتقالات المحافظة، وتخفيف السلوكيات الزائفة، ورفع المواصفات السليم.
تثبت هذه الورقة قابلية التقرير للمنطق الجهوي الحدسي لسيمبسون IK4 من خلال بناء إجراء قرار خالٍ من القطع يستفيد من مبرهنة كروستال ولمحة الدعم المحدود لحصر البحث العكسي عن البراهين ضمن مجموعات ذات أساس نهائي ومغلقة تصاعدياً من المتتاليات المتداخلة.
تقترح هذه الورقة خوارزميات ترشيح جديدة ضمن البرمجة المنطقية المقيدة تستفيد من المعلومات الهندسية من الإحداثيات الإقليدية لتحقيق انتشار قيود أقوى وتحسين الأداء الحسابي لمسألة البائع المتجول الإقليدية ومتغيراتها، مثل مسألة البائع المتجول المعممة.
تقدم الورقة البحثية FaithformBench، وهو معيار مرجعي فعال من حيث التكلفة وسليم لتقييم مدى أمانة أنظمة الصياغة الرياضية الآلية، كاشفاً أن العديد من النماذج تظهر سلوك "التملق" عبر التصحيح الصامت للمدخلات غير الصالحة إلى عبارات قابلة للإثبات، مما يسلط الضوء على وجود توتر بين الحفاظ على الصحة والحفاظ على عدم الصلاحية.
تقدم هذه الورقة إطار عمل قائماً على الدوائر الاحتمالية لإكمال الرسوم البيانية للمعرفة، والذي يتعلم مجموعات قواعد مدمجة وعالية الأداء، محققاً خفضاً يصل إلى 96% في عدد القواعد مع الحفاظ على 91% من أداء النموذج المرجعي والتفوق على النماذج المرجعية الكاملة بما يصل إلى 31 ضعفاً باستخدام عدد مماثل من القواعد الدنيا.
تثبت هذه الورقة أن النظرية المعادلية لجبر كليين العلائقي الممتد مع عامل حلقة رسومي (وممتد كذلك مع العناصر العليا، والاختبارات، والمرافق، والأسماء الاسمية) هي مسألة كاملة في فضاء PSPACE، مما يحل مشكلة مفتوحة تتعلق بنظرية جبر كليين العلائقي القائمة على النطاق من خلال تقديم نموذج حلقة-آلية جديد لاختزال هذه النظريات إلى مشكلة احتواء اللغة لآلات الأوتوماتون المتناوبة ثنائية الاتجاه.
تقدم هذه الورقة أنظمة إعادة الكتابة المونودية (MRS) المعرفة فوق مونويدات اختيارية لمعالجة القيود المنطقية للمونويدات الحرة، وتؤسس تضاؤداً ثنائياً كانونياً (2-adjunction) بين الفئة الثنائية (2-category) لأنظمة إعادة الكتابة المونودية "النوثرية المتلاقية" وفئة المونويدات، وتثبت أن القدرة على تحويل أي عرض لمونويد ما إلى عرض آخر عبر تحويلات "تيتزي" الأولية المعممة هي التي تميز المونويدات الحرة.
تقدم هذه الورقة صياغة بديهية من نوع هيلبرت (Hilbert-style) تامة وصحيحة للتعبيرات المنتظمة ذات الاستشراف (lookahead) عبر تقديم متغير من منطق الديناميكا الاقتراحية (propositional dynamic logic) على ترتيبات خطية منتهية ممتدة مع مؤثرات الهوية والمتممة، مما يتيح اختزالاً إلى منطق ديناميكا اقتراحية خالٍ من الهوية مع الحفاظ على التعقيد الحسابي.
تؤسس هذه الورقة إطاراً رسمياً موحداً لبناء تأويلات نموذجية من نظريات البنية التعددية عبر تصنيف عدم الحتمية إلى أنواع معرفية وبنيوية، وإثبات كيف يمكن لآليات استقرار الإغلاق، والإكمال الشامل، والاختيار النموذجي أن تحقق الحتمية في ظل ظروف بنيوية محددة.