1215 ورقة بحثية
تقدم هذه الورقة خوارزمية تقوم بتجميع مصطلحات لامدا الكمية الخطية إلى دوائر كمية من خلال الاستففادة من هندسة التفاعل لـ جيرارد لتعظيم الحوسبة الكلاسيكية أثناء عملية التجميع، مع تحديد تدفق التحكم عالي الرتبة كتحدٍ رئيسي وتوصيف المصطلحات القابلة للتجميع بكفاءة من خلال نظام نوعي.
تقدم هذه الورقة خوارزمية فعالة خاصة بنماذج معينة للنماذج العصبية الجمعية (NAMs)، تولد تفسيرات ذات حد أدنى عددي مثبت بـتعقيد استعلام لوغاريتمي، متجاوزة بذلك الاستعصاء الحسابي للشبكات العصبية القياسية ومتفوقة على الأساليب الحالية في كل من حجم التفسير ووقت الحوسبة.
يقدم هذا الفصل نظرة شاملة على الأساليب النظرية للإثبات البنائية والموجهة نحو بناء الجمل، وتحديداً تقنيات "ماهارا" و"بيتس"، لإثبات خصائص "كريج" والاستيفاء الموحد عبر المنطق الكلاسيكي، والحدسي، والمنطقي الوجودي، والمنطقي تحت البنيوي ضمن إطار نظرية الإثبات الشاملة.
تقدم هذه الورقة طريقة لتحويل مجموعات العبارات المشبعة من مبرهنات الاستنتاج الآلي إلى نماذج مضادة لانهائية صريحة وقابلة للتحقق لجزء التكافؤ الأحادي، وتنفذ هذا النهج في مبرهنات Vampire و E، وتثبت فعاليته في مشروع النظريات التكافؤية.
تقدم هذه الورقة طريقة استنتاجية لإثبات قابلية الإرضاء للصيغ التي تجمع بين المكممات الكلية ورموز الدوال غير المفسرة، والتي تنجح في إثبات قابلية الإرضاء في الحالات التي تفشل فيها أدوات حل مسائل المنطق الرياضي (SMT) الحالية بسبب عدم القدرة على بناء نماذج صريحة.
تقدم هذه الورقة فئة فرعية من فئة بيرنايس-شونفيكلد (Bernays-Schoenfield) كاملة بالنسبة لـ PSPACE، تحافظ على دلالات اللعبة ذات اللاعبين للصيغ البولينية المكممة، مما يتيح تصنيف مشكلات مكتبة TPTP عبر مستويات مختلفة من الهرم متعدد الحدود.
تقدم هذه الورقة ICaTT، وهي امتداد محافظ لنظرية النوع CaTT التي تدمج القابلية للعكس الاستقرائية المشتركة لتسهيل الصياغة الموجزة للتكافؤات و-equifibrations، مدعومة بتنفيذ وتفسير دلالي في الفئات الضعيفة المحددة.
تقدم هذه الورقة مفهومًا موحدًا للتعبير للمقارنة بين أطر الحجاج المجردة والمهيكلة ذات القواعد والمقدمات غير المؤكدة، حيث تعرض نتائج سلبية وإيجابية تثبت القدرات النسبية لأطر الحجاج المجردة غير المكتملة ونظام +ASPIC.
تقدم هذه الورقة صياغة رسمية عامة وقابلة لإعادة الاستخدام لمنطق هينيسي-ميلنر ضمن مكتبة علوم الحاسوب "Lean" (CSLib)، والتي تتميز بنظرية ميتا كاملة تتضمن مبرهنة هينيسي-ميلنر وتستفيد من أتمتة "Lean" لدعم أنظمة الانتقال المسمى ذات الصور المحدودة التعسفية.
تثبت الورقة البحثية أن مسألة التحقق من النموذج لمنطق المسارات المنفصلة (+) هي مسألة قابلة للحل في وقت محدد بمعلمة (FPT) على فئات الرسوم البيانية التي تستبعد مينيما طوبولوجي ثابت، مما يحل جوهرياً مسألة القابلية للحل لهذا المنطق على الفئات المغلقة بالرسم الفرعي.