حل المعادلات الخطية: ألعاب تركيبية لحجم شجري ومساحة

نعتبر نظام الإثبات Res () الذي قدمه إيتسيكسون وسوكولوف (Ann. Pure Appl. Log. '20)، وهو امتداد لنظام إثبات الحلول ويعمل مع تفكيك المعادلات الخطية على F₂. ندرس توصيفات الحجم الشجري والمساحة في دحض Res () باستخدام الألعاب التركيبية. على وجه الخصوص، نقدم فئة من الصيغ القابلة للتوسيع ونثبت حدود الحريم الأدنى للحجم الشجري عليها باستخدام ألعاب Prover-Delayer، فضلاً عن حدود المساحة الأدنى. هذه الفئة تكتسب أهمية خاصة نظرًا لأنها تحتوي على العديد من المبادئ التركيبية الكلاسيكية، بما في ذلك مبدأ الغرف، والترتيب، ومبادئ الترتيب الخطي الكثيف. علاوة على ذلك، نقدم علاقة العرض-المساحة لـ Res () التي تعمم النتائج التي قدمها أتشيراس ودالمو (J. Comput. Syst. Sci. '08) ونسختهم من ألعاب Spoiler-Duplicator.