Key points are not available for this paper at this time.
Wir betrachten das Beweisystem Res (), das von Itsykson und Sokolov (Ann. Pure Appl. Log. '20) eingeführt wurde, welches eine Erweiterung des Auflösungsbeweisystems darstellt und mit Disjunktionen linearer Gleichungen über F₂ arbeitet. Wir untersuchen Charakterisierungen von baumartiger Größe und Raum von Res () Widerlegungen unter Verwendung kombinatorischer Spiele. Nämlich führen wir eine Klasse erweiterbarer Formeln ein und beweisen lower bounds für die baumartige Größe mithilfe von Prover-Delayer-Spielen sowie Raum lower bounds. Diese Klasse ist von besonderem Interesse, da sie viele klassische kombinatorische Prinzipien enthält, einschließlich des Schubladenprinzips, der Ordnung und der dichten linearen Ordnung. Darüber hinaus präsentieren wir die Breite-Raum-Beziehung für Res (), die die Ergebnisse von Atserias und Dalmau (J. Comput. Syst. Sci. '08) und deren Variante von Spoiler-Duplicator-Spielen verallgemeinert.
Gryaznov et al. (Fri,) haben diese Frage untersucht.