Die Komplexität der Formelauswertung in intuitionistischen Logiken

Der Intuitionismus ist eine Denkweise, die auf Intuition und Konstruktivismus basiert. Mathematisch gesehen werden hier nur konstruktive Beweise anerkannt und der Begriff der Wahrheit wird durch "beweisbar" ersetzt. Die intuitionistische Logik greift diesen Gedanken in der Form auf, dass das Gesetz des ausgeschlossenen Dritten nicht gültig ist. Eine Aussage "A oder nicht A" gilt nur dann als wahr, wenn entweder A oder das Gegenteil von A bewiesen werden kann. Für die intuitionistische Aussagenlogik gibt es eine Semantik, die jener der Modallogik sehr ähnlich ist. In diesem Sinne kann man sie auch als spezielle Modallogik auffassen. Wir beschäftigen uns in dieser Arbeit im Wesentlichen mit der Formelauswertung in intuitionistischen Logiken und untersuchen ihre Komplexität. Dabei betrachten wir Fragmente, die durch verschiedene Einschränkungen entstehen. Auf der semantischen Seite beschränken wir die zugelassenen Modelle. Auf der syntaktischen Seite kann man die Zahl der Variablen einschränken oder nur bestimmte Operatoren zulassen. Unsere ersten Ergebnisse beziehen sich auf Logiken, bei denen es nur endlich viele paarweise nicht äquivalente Formeln gibt. Hier zeigen wir, dass das Formelauswertungsproblem, das Erfüllbarkeitsproblem und das Tautologieproblem sehr einfach zu lösen sind. Weiter betrachten wir die Logik, bei der nur eine Variable zugelassen ist. Für diese Logik zeigen wir, dass die Formelauswertung AC1-vollständig ist. Dies ermöglicht eine neue Sicht auf die Klasse AC1, da es das erste vollständige natürliche Problem für diese Klasse ist. Außerdem untersuchen wir, für welche Logiken das Formelauswertungsproblem die maximale Komplexität erreicht. Hier geht es insbesondere um die genaue Abgrenzung - also um die Frage, welche Freiheitsgrade man in einer Logik mindestens braucht, damit die Formelauswertung derart komplex ist. Am Ende betrachten wir noch einige Modallogiken, die Begleiter von intuitionistischen Logiken sind.

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.