1215 ورقة بحثية
تتناول هذه الورقة "مشكلة اللامركزية" عبر تقديم أنطولوجيا قائمة على الرسوم البيانية تُعرّف اللامركزية رسميًا كخاصية علاقاتية ومحددة موضوعيًا متميزة عن مجرد التوزيع، مصحوبة بمقاييس مبتكرة وأداة قائمة على المتصفح لتمكين تحليل متسق وغير مرتبط بنطاق محدد للأنظمة غير المتجانسة مثل التعلم الاتحادي والبلوكشين.
تُكيّف هذه الورقة نهج إعادة الكتابة الشرطية للكشف عن عدم الإنهاء غير الدوري وتطبيقه على البرمجة المنطقية من خلال تقديم تقنية بسط جديدة تولد أنماطاً تمثل مجموعات لانهائية من تسلسلات إعادة الكتابة المحدودة، والتي تم تقييمها تجريبياً باستخدام أداة NTI.
يقدم GEB-Bench معياراً مرجعياً جديداً يقيم قدرة نماذج الذكاء الاصطناعي على التعرف على الزخارف الهيكلية المجردة ورسم خرائطها عبر وسائط متنوعة، مما يكشف عن فجوة ثابتة ومنتظمة بين التعرف أحادي الصوت والتجريد عابر الأصوات، وهي فجوة تستمر حتى في النماذج الرائدة.
تؤسس هذه الورقة تسلسلاً هرمياً صارماً لـ "الخلاصة السلوكية" للأنظمة التوليدية المزينة ببيانات الأصل، لتحديد متى يمكن التخلص من بيانات الأصل بدقة دون تغيير المسارات المستقبلية المشروعة، مقدمةً إجراءات صقل معيارية تحسب العلاقات التكافؤية الأكثر خشونة التي تحافظ إما على المسارات المتناهية أو على البنية التفرعية الكاملة.
تقدم هذه الورقة طريقة لتقسيم فضاء الحلول القائمة على الاستراتيجية لنظرية المجموعات القصوى، والتي تتفوق على تقنيات الاستشراف غير المرتبطة بنطاق محدد، مما يتيح التحقق من حالات محدودة أكبر لتخمين تشفاتال عند دمجها مع برنامج حل البرمجة الخطية المختلطة (MILP) الدقيق.
تقدم هذه الورقة تكلفة الحصى الزرقاء (blue pebbling cost)، وهي مقياس جديد يحدد بدقة متطلبات مساحة البند (clause space) في استدلالات الشجرة (tree-like) والاستدلال السلبي (negative Resolution)، مما يتيح وضع حدود دقيقة للمساحة لفئات محددة من الصيغ ويثبت وجود تباين كبير في المساحة بين هذين النظامين الاستدلاليين.
تقدم هذه الورقة GR1MINE، وهي أداة قائمة على مشكلة الإرضاء (SAT) تتعلم مواصفات GR(1) بكفاءة من مسارات النظام عبر الاستفادة من الهياكل الزمنية وتعلم البنود التزايدي، محققةً سرعة أكبر في التوليف ومعدلات استرداد أعلى للصيغ القابلة للتحقيق مقارنة بأدوات تعدين LTL الموجودة.
تقدم هذه الورقة برهاناً تركيبياً بالكامل وجديداً لدمج المنطق الجهاتي الكلاسيكي S4 في منطق التضمينات الحزمية البوليانية (BBI) باستخدام حسابات نمط هيلبرت ونظريات الاستنتاج، مما يوفر إطاراً مستقراً يمتد ليشمل مختلف التنويعات البديهية واللغوية لكلا المنطقين.
تقدم هذه الورقة نظام SolVRT، وهو نظام قائم على الأساليب الصورية يقوم تلقائياً بتخليق وحدات تحكم في تجاوز انخفاض الجهد (voltage ride-through) مصممة بأسلوب "صحيح بالبناء" لمراكز البيانات لضمان الامتثال لرموز الشبكة، مع توفير قدرات تشخيصية أيضاً لتحديد وحل حالات عدم القابلية للتحقيق من خلال تعديلات مستهدفة في الأجهزة أو أعباء العمل.
تقدم هذه الورقة صياغة رسمية باستخدام لغة Lean 4 لتحويل لابلاس وعكسه عبر نظرية من نوع برومويتش، مما يبرز تطبيقه على المتذبذب التوافقي مع معالجة التحديات التحليلية والصياغية الرئيسية.