26 lines
2.3 KiB
TeX
26 lines
2.3 KiB
TeX
\chapter{Automatische Theorembeweiser}
|
|
\label{automatische theorembeweiser}
|
|
Falls für eine vollständige Resolution (\ref{praedikatenlogik: resolution}) existiert kann hierfür ein automatischer Theorembeweiser realisiert werden.
|
|
Ein solcher Theorembeweiser erhält Axiome und Anfragen und errechnet daraus einen Beweis.
|
|
Obwohl dies in der Theorie möglich ist stellt die reale Umsetzung ein Problem dar.
|
|
Dies kann mehrere Gründe haben:
|
|
\begin{itemize}
|
|
\item \textbf{Suchbaumproblem:}\\
|
|
Die meisten Suchräume sind sehr groß.
|
|
D.h. es gibt viele Möglichkeiten die Inferenzregeln (\ref{inferenzregeln}, \ref{praedikatenlogik: inferenzregeln}) anzuwenden.
|
|
Auch wenn ein Computer in der Lage dazu ist viele Inferenzen pro Sekunde durchzuführen ist ein erfahrener Mathematiker oft schneller.
|
|
So sind Mathematiker in der Lage dazu Suchräume zu verwenden, die für einen "Brute-Force"-Algorithmus unmöglich wären.
|
|
\item \textbf{Entscheidbarkeit:}\\
|
|
Die Prädikatenlogik (\ref{praedikatenlogik}) ist \textbf{halbentscheidbar}.
|
|
Das bedeutet, dass man nur für allgemeingültige Formeln sicher sein kann, dass ein Beweiser die Wahrheit nach endlicher Zeit feststellt.
|
|
Für eine nicht allgemeingültige Formel ist es möglich, dass der Beweiser niemals hält.
|
|
\item \textbf{Limitierung der Prädikatenlogik 1. Stufe:}\\
|
|
Für viele Zwecke ist die Prädikatenlogik 1. Stufe (\ref{praedikatenlogik: 1.stufe}) nicht mächtig genug.
|
|
Falls die Prädikatenlogik allerdings über die erste Stufe hinaus erweitert wird geht ihre \textbf{Vollständigkeit verloren}.
|
|
\end{itemize}
|
|
Dennoch sind die Theorembeweiser nicht komplett nutzlos.
|
|
Sie können Probleme bis zu einer bestimmten Komplexitätsebene lösen oder einem Mathematiker als halbautomatische Theorembeweiser Hilfestellungen geben.
|
|
Zudem dienen sie der Verifikation von kryptographischen Protokollen.
|
|
Ein weiteres Einsatzgebiet ist die Suche nach Software-Modulen zur Wiederverwendung.
|
|
Hierbei definiert der Programmierer Vor- und Nachbedingungen, woraufhin eine Datenbank nach Software-Modulen durchsucht wird, die diese erfüllen.
|
|
Der Programmierer spart sich hierdurch die eigene Implementierung. |