0. Einführung

Die Verarbeitung Beweisprüfungsverfahren erlaubt es, die Lösungen von Übungsbeispielen auf ihre Korrektheit zu prüfen. Ist diese Verarbeitungsart gewählt, muss daher im Eingabebereich die Herleitung eines Arguments eingegeben werden. Die Syntax einer Herleitung entspricht im wesentlichen der im weiland Logiktutorium und im Skriptum verwendeten, diese wiederum der aus E.J. Lemmon: ,,Beginning Logic'' und Colin Allen: ,,Logic Primer''.

1. Syntax

Aussagen setzen sich aus Prädikaten, Individuenkonstanten und beliebigen Namen, Individuenvariablen, Konnektiven und Klammern zusammen. Für diese Bestandteile gelten folgende Konventionen:

1.1. Prädikate

Ein Prädikat besteht aus genau einem Großbuchstaben, gefolgt von beliebig vielen (einschließlich null) Kleinbuchstaben oder Ziffern. Beispiele für Prädikate sind ,,P'', ,,Q'', ,,P1'', ,,Q42'', aber auch ,,Hugo'' oder ,,Blubb37''. Hat das Prädikat Argumente, werden sie - durch Beistriche getrennt - in runden Klammern ans Prädikat angeschlossen, z.B. ,,Mensch(Sokrates)'' oder ,,Groesser(Eins,Zwei)''.

1.2. Individuenkonstanten und beliebige Namen

Individuenkonstanten und beliebige Namen bestehen wie Prädikate aus genau einem Großbuchstaben, gefolgt von beliebig vielen (einschließlich null) Kleinbuchstaben und Ziffern. Beispiele sind ,,Sokrates'' oder ,,Platon''. Die Beweisprüfung erkennt aus dem Zusammenhang, ob es sich um eine Individuenkonstante oder um einen beliebigen Namen handelt.

1.3. Individuenvariablen

Individuenvariablen beginnen mit einem Kleinbuchstaben, gefolgt von beliebig vielen (einschließlich null) Kleinbuchstaben und Ziffern. Beispiele sind ,,x'', ,,x42'' und ,,hugo''.

1.4. Konnektive

Aussagen sind aus Negationen, Konjunktionen, Disjunktionen, Konditionalen und Bikonditionalen aufgebaut. Da eine gewöhnliche Computertastatur nicht über die üblicherweise benützten logischen Zeichen verfügt, verwenden Sie bitte folgende Annäherungen:

,,~'', ,,&'', ,,v'', ,,->'', ,,<->''

Alternativ können Sie auch die Wörter ,,nicht'', ,,und'', ,,oder'', ,,dann'' und ,,gdw'' verwenden.

1.5. Quantoren

Als All- bzw. Existenzquantor werden die Wörter ,,alle'' bzw. ,,ein'' verwendet. Dem Quantor folgt in Klammern die durch ihn gebundene Variable und der quantifizierte Ausdruck, voneinander getrennt durch einen Beistrich.

Beispiele: 

alle(x,Mensch(x)->Sterblich(x))
ein(x,Unsterblich(x))
alle(x,ein(y,Liebt(x,y)))

1.6. Klammern

Für die Klammerung verwenden Sie bitte die üblichen runden Klammern, ,,('' und ,,)''. Wenn Sie Klammern weglassen, gilt folgende Auswertungsreihenfolge:

  1. Negationen
  2. Konjunktionen
  3. Disjunktionen
  4. Konditionale
  5. Bikonditionale

Die zweistelligen Konditionale sind linksassoziativ.

2. Schlussregeln