تمثيلات الرسوم البيانية للمنطق من الرتبة العليا وإثبات النظريات

يقدم هذا البحث أول استخدام للشبكات العصبية الرسومية (GNNs) في البحث عن البراهين من الرتبة العليا، ويظهر أن الشبكات العصبية الرسومية يمكنها تحسين النتائج المتقدمة في هذا المجال. تسمح البرهانات التفاعلية من الرتبة العليا بتوثيق معظم النظريات الرياضية وقد أثبتت أنها تمثل تحديًا كبيرًا لتعلم الآلة العميق. المنطق من الرتبة العليا شديد التعبير، وحتى مع كونه مهيكل بشكل جيد مع قواعد ودلالات محددة بوضوح، لا يزال هناك عدم وجود طريقة مقبولة على نطاق واسع لتحويل الصيغ إلى تمثيلات رسومية. في هذا البحث، ندرس عدة تمثيلات رسومية للمنطق من الرتبة العليا ونقيمها باستخدام معيار HOList للمبرهنات من الرتبة العليا.