Ein Resolutionskalkül für eine Logik mit unscharf definierten Prädikaten

Abstract

Eine für das menschlichen Denken charakteristische Vorgehensweise ist es, Objekte nach verschiedenen Kriterien zu klassifizieren. Dabei tritt jedoch häufig das Phänomen auf, daß die einzelnen Konzepte nicht scharf gegeneinander abgegrenzt sind. Thema dieser Arbeit ist es, diesen Sachverhalt für das automatische Beweisen zugänglich zu machen. Dazu werden zunächst alle Begriffe, die sich auf dasselbe Kriterium beziehen, zusammengefaßt und auf ein gemeinsames „Tiefenprädikat‘“ abgebildet. Die Abbildung ist rein syntaktischer Natur und wirft keine besonderen Probleme auf. Die Tiefenprädikate besitzen jedoch, um den semantischen Zusammenhang herauszustellen, als zusätzliches Argument Mengen von Werten aus einer für den Diskursbereich charakterischen Größe. Dieses ist kein Term im üblichen prädikatenlogischen Sinne, so daß eine neue Logik, in der diese speziellen Argumente korrekt interpretiert werde, entwickelt werden mußte. Diese Logik ist eine Verallgemeinerung der Prädikatenlogik erster Stufe, wenngleich sie, was die Ausdrucksmächtigkeit betrifft, zu dieser äquivalent ist. Weiterhin wird ein Resolutionskalkül angegeben, der mit den Formeln der neuen Logik operiert. Zwar ließen sich alle Formelmengen auch innerhalb der Prädikatenlogik darstellen, doch die neuen Formelmengen sind nicht nur für einen menschlichen Leser kompakter und daher besser lesbar, sondern auch aus der Sicht eines automatischen Beweisers ist die Ableitung „einfacher“, da ein einzelner Inferenzschritt mehreren Schritten in der prädikatenlogischen Modellierung entspricht. Dadurch werden die Beweise kürzer und (lokal) zielgerichteter.