A Simple Loopcheck for Intuitionistic K

Das Kapitel behandelt die Suche nach intuitionistischen Varianten der klassischen Modallogik, wobei der Schwerpunkt auf der intuitionistischen Modallogik liegt, die ursprünglich von Fischer Servi axiomatisiert wurde. Es wird ein neuartiger Algorithmus eingeführt, der die Beendigung der Beweissuche nach intuitionistischer modaler Logik implementiert und konstruktiv entweder einen Beweis oder ein Gegenmodell für die Formel an der Wurzel hervorbringt. Dieser Algorithmus erweitert Simpsons beschriftete Sequenzen und führt das Konzept der Schrumpfung ein, um die Beendigung der Beweissuche wiederherzustellen. Das Kapitel untersucht auch die Verbindung zwischen vollständig beschrifteten Sequenzen und birelationalen Modellen und wie diese Verbindung genutzt werden kann, um Eigenschaften des Proof-Search-Algorithmus abzuleiten. Der Aufsatz schließt mit den Implikationen des Algorithmus für die Dezidierbarkeit und endliche Modelleigenschaft intuitionistischer modaler Logik und skizziert zukünftige Richtungen für Forschung und Umsetzung.