Auf der Suche nach einem neuen Ansatz für mathematische Beweise? Dieser Artikel stellt einen abstrakten kategorientheoretischen Rahmen für zyklische Beweissysteme vor und bietet eine einheitliche Behandlung, die sich von herkömmlichen Ableitungsbäumen unterscheidet. Zyklische Beweissysteme verwenden endliche Graphen für Ableitungen und stützen sich auf eine Gültigkeitsbedingung wie die globale Spurbedingung (GTC). Die Arbeit erweitert Brotherstons Ansatz unter Verwendung von Aktivierungsalgebren für eine natürlichere Formalisierung von Spurbedingungen. Durch die Berücksichtigung der Zusammensetzung von Spurinformationen werden neuartige Ergebnisse abgeleitet, einschließlich einer Ramsey-artigen Spurbedingung. Darüber hinaus wird die Verbindung zwischen Spur- und Automatentheorie untersucht und bewiesen, dass die Überprüfung der GTC für abstrakte zyklische Beweise mit bestimmten Spurbedingungen PSPACE-vollständig ist. Dies bietet neue Einblicke in die Komplexität und Struktur zyklischer Beweise.
Dieser Artikel ist in Mathematical Structures in Computer Science veröffentlicht. Er passt zum Umfang der Zeitschrift, da er sich mit abstrakten mathematischen Strukturen und deren Anwendungen in der Informatik befasst, insbesondere im Kontext der Beweistheorie und der Berechenbarkeitstheorie.