1215 ورقة بحثية
تقدم هذه الورقة برهاناً مبسطاً على كون مسألة تقرير التباين (injectivity) للخلايا الآلية العكسية على التكوينات المحدودة هي مسألة كاملة في فئة co-NP، وتضع حدوداً دنيا لحجم براهينها القضوية عبر نقل الحدود الدنيا المعروفة لأنظمة فري (Frege) ذات العمق المحدود عبر ترجمة باريس-ويلي (Paris–Wilkie).
تقدم الورقة البحثية XOR-SMOO، وهي خوارزمية مبتكرة تقرب بفعالية حدود باريتو (Pareto frontiers) في التحسين متعدد الأهداف العشوائي من خلال الاستفحتاد من أوراكلل (oracles) لـ SAT والعشوائية لتحقيق ضمانات تقريب ذات عامل ثابت باحتمالية عالية، مما يتفوق بشكل كبير على الأساليب الحالية في كل من الكفاءة الحسابية وجودة الحلول.
تقدم هذه الورقة إطاراً كوجبرياً موحداً يستخدم تقنيات الربط واللصق لنمذجة التماثلات البيزويمتريّة الحساسة للمكافأة التي تدمج بسلاسة الجوانب النوعية والكمية، مما يعمم مفاهيم عديدة قائمة مثل التماثلات البيزويمتريّة القائمة على العلاقات وتلك القائمة على المقاييس.
تقترح هذه الورقة نهج تركيب تكراري يستخدم قيود عد النوافذ لاستغلال رتابة المواصفات، وبالتالي بناء أتمتات ذات تقريبات مفرطة أو ناقصة لتقليل انفجار مساحة الحالة بشكل كبير في البناء الآلي لاستراتيجيات الأنظمة التفاعلية.
تقترح هذه الورقة نهجاً مبتكراً لبناء قيود كسر التماثل الفعالة والقوية للرسوم البيانية من خلال الاستفادة من أنماط الرسوم البيانية المستمدة من تبديلات التناظر (involution permutations)، والتي تحد بفعالية وتستبعد جزءاً كبيراً من الرسوم البيانية غير النموذجية مع الحفاظ على حجم صغير للقيود.
تقدم هذه الورقة "المنطق التوليدي" (Generative Logic)، وهو بنية حوسبة حتمية تقوم بتجميع التعريفات البديهية في شبكة موزعة من كتل المنطق لتوليد براهين ذات تسلسل كامل وموثق وحسابات عددية بشكل منهجي، حيث نجحت في اشتقاق نتائج رياضية معقدة مثل صيغة غاوس للجمع على أجهزة حاسوب عادية.
تُبين هذه الورقة أن تحديد ما إذا كانت مجموعة المجموعات (sumset) لمجموعة نموذجية من المجموعات الجزئية لـ تغطي الأعداد الصحيحة بأكملها هو أمر غير قابل للتقرير، حيث أُثبت أن هذه المسألة تكافئ مشكلة التوقف الشاملة لبرنامج Fractran وهي مرتبطة بحدسية كولاتز.
تقدم هذه الورقة "منطق هوار للوصول" (Access Hoare Logic)، وهو صياغة رسمية جديدة للاستدلال حول التحكم في الوصول والأمن في البرامج الحاسوبية، وتثبت سلامته، واكتماله، وفروقه الجوهرية عن كل من منطق هوار القياسي ومنطق عدم الصحة.
تؤسس هذه الورقة إطار عمل لاستنباط نظام برهان دون أسي مع حذف القطع مباشرة من بنية عصبية مصنفة وحساسة للموارد، مبرهنةً أن الانضباط المنطقي الناتج سليم فيما يتعلق بالقيود البنيوية، وأن البنية نفسها تشكل فئة مونويدية متناظرة.
تقدم هذه الورقة ترميزات CNF جديدة وشبه مثالية لقيود العدد (cardinality constraints) تقلل بشكل كبير من أعداد البنود (clauses) مقارنة بالطرق السابقة، بما في ذلك ترميز جديد لـ AtMostOne يدحض حدسية استمرت طويلاً، ويضع أول حد أدنى غير بديهي غير مشروط للمسألة، ويحسن نتيجة في تعقيد الدوائر عمرها 50 عاماً، بينما يقترح أيضاً تقنية "ضغط الشبكة" (grid compression) لتحقيق ترميزات مدمجة لقيود AtMost العامة.