From b6e1e8b6ff1aed1037aebe997b60ff56a08a43d4 Mon Sep 17 00:00:00 2001 From: paul-loedige Date: Wed, 3 Feb 2021 09:44:20 +0100 Subject: [PATCH] lokig abgeschlossen --- .../Logik/Automatische Theorembeweiser.tex | 26 +++++++++++++++++++ parts/Logik.tex | 3 ++- 2 files changed, 28 insertions(+), 1 deletion(-) create mode 100644 chapters/Logik/Automatische Theorembeweiser.tex diff --git a/chapters/Logik/Automatische Theorembeweiser.tex b/chapters/Logik/Automatische Theorembeweiser.tex new file mode 100644 index 0000000..43fbe54 --- /dev/null +++ b/chapters/Logik/Automatische Theorembeweiser.tex @@ -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. \ No newline at end of file diff --git a/parts/Logik.tex b/parts/Logik.tex index eed2569..784b613 100644 --- a/parts/Logik.tex +++ b/parts/Logik.tex @@ -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} \ No newline at end of file +\input{chapters/Logik/Prädikatenlogik.tex} +\input{chapters/Logik/Automatische Theorembeweiser.tex} \ No newline at end of file