\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.