KI_Kuenstliche_Intelligenz/KI_Zusammenfassung
1
0
Fork 0
generated from TH_General/Template_Summary
Code Issues Pull Requests Projects Releases 1 Wiki Activity

lokig abgeschlossen

Browse Source
This commit is contained in:
paul-loedige 2021-02-03 09:44:20 +01:00
parent 9e674220fe
commit b6e1e8b6ff
2 changed files with 28 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
chapters/Logik/Automatische Theorembeweiser.tex Normal file
View File

@ -0,0 +1,26 @@
\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.

3
parts/Logik.tex
View File

@ -5,4 +5,5 @@
\input{chapters/Logik/Logische Systeme.tex}
\input{chapters/Logik/Aussagenlogik.tex}
\input{chapters/Logik/Beweisverfahren.tex}
\input{chapters/Logik/Prädikatenlogik.tex}
\input{chapters/Logik/Prädikatenlogik.tex}
\input{chapters/Logik/Automatische Theorembeweiser.tex}