Seite parallel anzeigen





Unterscheidungsmerkmale - Einsatzmöglichkeiten eines Kalküls

(Logik Einführung Kapitel 8.3)

Diese Seite nimmt Bezug auf

(Seite parallel anzeigen)
Liste überspringen
Zum Seitenanfang

Betrachten wir einen Kalkül, gibt es einige Fragen, deren Beantwortung essenziell für den möglichen Einsatz in automatischen Beweisern sein kann. Die wesentlichen Unterscheidungsmerkmale für die Algorithmen, die durch die Schlussregeln und Axiome definiert werden, sind:
  • Korrektheit
    Lassen sich nur semantisch gültige Sätze ableiten?
     
  • Vollständigkeit
    Lassen sich alle semantisch gültigen Sätze ableiten?
     
  • Gültigkeit vs. Erfüllbarkeit
    Erinnern wir uns an die Zusammenhänge zwischen Gültigkeit und Erfüllbarkeit: Eine Formel ist genau dann gültig, wenn das Gegenteil der Formel unerfüllbar ist. Ist also das Gegentei der Formel erfüllbar, so kann die Formel nicht gültig sein - ist das Gegenteil unerfüllbar, so muss die Formel gültig sein.
    Es gilt also:
    Eine vollständige und korrekte Prozedur um die Erfüllbarkeit einer Formel zu bestimmen reicht aus, um die Gültigkeit einer Formel zu bestimmen. Das Vorgehen, ein Gültigkeitsproblem in ein Erfüllbarkeitsproblem zu übersetzen, wird als "Reduktion auf Erfüllbarkeit" bezeichnet.
     
  • Direkter vs. indirekter Beweis
    Ein Beweis wird als direkt bezeichnet, wenn er eine Ableitung einer Aussage aus einer Menge von Prämissen ist.
    Ein indirekter Beweis (auch "Reductio ad absurdum") ist eine Ableitung, die das Gegenteil der zu beweisenden Aussage zu einem Widerspruch führt.
    D.h. in einem direkten Beweis formen wir eine Menge an Voraussetzungen so lange um, bis wir das Ergebnis erhalten.
    Bei einem indirekten Beweis nehmen wir das Gegenteil der zu beweisenden Aussage an. Widerspricht diese den Voraussetzungen, so muss sie ungültig und somit die Annahme gültig sein.

    Beispiel - Direkter vs. indirekter Beweis

    Angenommen, wir wollen zeigen, dass nicht alle Menschen Römer sind.
    • In einem direkten Beweis formen wir die unser Wissen so lange um, bis wir die Annahme erhalten.
    • Für den indirekten Beweis nehmen wir das Gegenteil an - also, dass alle Menschen Römer sind.
      Daraus folgt, dass Sokrates Römer ist.
      Nachdem wir allerdings wissen, dass Sokrates Grieche ist, und er weiters nicht Römer und Grieche sein kann, führt diese Annahme zu einem Widerspruch. Das Gegenteil der Annahme muss also gültig sein.
  • Analytizität des Beweisverfahrens
    Analytizität bedeutet, dass die Gültigkeit eines Satzes allein durch seine Teilaussagen (ohne Hinzufügen weiterer Formeln) gezeigt wird - d.h. dem Beweis werden durch Regelanwendungen nur Bestandteile der ursprünglichen Aussage hinzugefügt.
     
  • Don't-care-Indeterminismus des Beweisverfahrens
    Der Don't-care-Indeterminismus (auch "Beweiskonfluenz" genannt) besagt, dass die Reihenfolge der Anwendungen der Schlussregeln für das Ergebnis der Ableitung egal ist.
     
  • Komplexität des Beweisverfahrens
    Grundlegende Fragen zur Komplexität sind u.A. folgende:
    • Mit welcher Komplexität des kürzesten Beweises in Relation zur Komplexität der zu beweisenden Formel ist bei der Berechung einer Lösung zu rechnen? Besitzen einfache Formeln einfache Beweise?
    • Welche Komplexität hat ein Beweis im schlimmsten Fall?
    • Wie viel Speicherplatz wird benötigt? D.h. Ist immer entscheidbar, ob ein Schluss gültig ist?
    • Terminiert das Verfahren immer?