1215 ورقة بحثية
تقدم هذه الورقة إطاراً مستقلاً عن المنطق قائماً على "الاستنتاجات من نوع g" (g-sequents) والحسابات المجردة لتحليل تفاعلات قواعد الاستدلال، مما يتيح تحويل أي حساب مجرد إلى شبكة من الأنظمة المتكافئة حدودياً والتي تشمل الصيغ المعروفة للاستدلال العميق وصيغ السلسلة المسمّاة للمنطقات من نوع هورن.
تقترح هذه الورقة إطاراً كمياً للاستعلام عن قواعد معرفة المنطق الوصفي الموزونة وغير المتسقة من خلال تعريف الإجابات المؤكدة والممكنة بناءً على تفسيرات مقيدة بالتكلفة أو ذات التكلفة المثلى، وتوفر تحليلاً شاملاً للتعقيد الحسابي لهذه المشكلات عبر منطقيات تتراوح من ELbot إلى ALCO.
تقدم هذه الورقة إطار عمل قائماً على القواعد وتصريحياً يستخدم برمجة مجموعات الإجابة لتحديد وحساب علاقات الأولوية بين الحقائق المتعارضة للاستعلام من قواعد المعرفة غير المتسقة، مع معالجة تحديات التفضيلات الدورية من خلال تحليل اللا دورية وتقنيات إزالة الدورات البراغماتية.
تقدم هذه الورقة "تِيسا" (Tessa)، وهو نهج مبتكر يصيغ عملية التحقق من نماذج سلاسل ماركوف ذات الأفق المحدود في صورة حسابات تنسورية كثيفة للاستفادة من المسرعات العتادية وتحقيق تسريع هائل مقارنة بالطرق الحالية، لا سيما في أنظمة الانتقال الكثيفة.
تقدم هذه الورقة نموذجاً تأسيسياً مدركاً للتماثل لاستنتاج القواعد المنطقية، والذي يُمكّن -من خلال فرض التكافؤ الدقيق عبر آلية تصدير معيارية مبتكرة- نموذجاً تم تدريبه مسبقاً على بيانات اصطناعية صغيرة من تعميم قواعد قابلة للتفسير ودقيقة على مخططات أكبر بكثير دون الحاجة لإعادة التدريب.
تقدم هذه الورقة نظرية تم التحقق منها آلياً في Isabelle/HOL تثبت الحدود الأساسية للتعافي من الانهيار في أنظمة الكتابة المزدوجة، حيث تثبت أن التسليم الموثوق لمرة واحدة بالضبط يتطلب قراءة حالة القبول في المستودع وتوفير ضمانات رسمية بشأن آليات العزل اللازمة وعمر الأدلة.
تقدم هذه الورقة ترميزات SAT وMaxSAT مدمجة لجدولة اجتماعات الأعمال بين الشركات، والتي تستخدم تصفية النطاق والمتغيرات المشتركة لتقليل عدد البنود واستهلاك الذاكرة بشكل كبير مع تقليل نطاقات وقت خمول المشاركين إلى الحد الأدنى، متفوقة بذلك على كل من صيغة MaxSAT المنشورة والمحلل التجاري Gurobi في كفاءة الحل.
تقارن هذه الورقة بين التراجع مع التحسينات الخاصة بالمجال وبين الحل القائم على إرضاء القابلية للتحقق (SAT) لألغاز "هيتوري" (Hitori) و"بينارو" (Binairo)، مما يوضح أن انتشار القيود يعزز أداء التراجع بشكل كبير، بينما يكشف أن حلول SAT تتفوق في ألغاز "بينارو" ولكنها تواجه صعوبة في ألغاز "هيتوري" بسبب التكلفة الحسابية لفحوصات الاتصال التكرارية.
تقدم هذه الورقة تصحيحاً تم التحقق منه آلياً لإطار عمل من عام 2018 خاص بالدلالات المعرفية لسياسات تدفق المعلومات، والذي تم إنجازه بمساعدة مساعد برمجة يعمل بالذكاء الاصطناعي الوكيل، لتوفير أساس متين وعام لتحديد وإنفاذ المتطلبات الأمنية التعبيرية.
تقدم هذه الورقة "مبدأ الثبات النحوي الديناميكي" لإثبات أن افتراضاً ضمنياً محدداً، عند التعامل معه كمتغير وإزالته، يكشف عن تميز بنيوي متكرر عبر مجالات متنوعة —بما في ذلك التشفير، والفيزياء، والقابلية للحوسبة— يؤدي في النهاية إلى تناقض في نظرية المسائل المرضية (SAT)، مما يفرض الاستنتاج بأن .