Nichttheoreme

Die effektive Erkennung von Nichttheoremen ist das zentrale Problem der Entscheidbarkeit von Theorien. Seit der Arbeit von "Church" 1936 gilt die (Hypo-)These, dass diese Erkennbarkeit nicht in allen Fallen moglich ist. Als eine mogliche Forschungsaufgabe bleibt dann die Frage, ob es irgendwelche effektive entscheidbare Kriterien gibt, mittels deren man moglichst grosse Teilklassen von Formeln als zur Klasse der Theoreme oder als zur Klasse der Nichttheoreme zugehorig erkennen kann. Insbesondere Kriterien fur die Zugehorigkeit zur Klasse der Nichttheoreme waren fur automatische Theorembeweiser von grossem praktischen Interesse. In der vorliegenden Arbeit werden Kriterien fur Nichttheoreme gefunden, die sich ausschliesslich an syntaktischen Eigenschaften von Formeln orientieren. Nebenbei wird der Tableaukalkul in der Version von "Smullyan" erstmalig voll formalisiert."