diff --git a/Logik und Logikprogrammierung - Cheatsheet.pdf b/Logik und Logikprogrammierung - Cheatsheet.pdf new file mode 100644 index 0000000..60f6d53 Binary files /dev/null and b/Logik und Logikprogrammierung - Cheatsheet.pdf differ diff --git a/Logik und Logikprogrammierung - Cheatsheet.tex b/Logik und Logikprogrammierung - Cheatsheet.tex new file mode 100644 index 0000000..64e41c6 --- /dev/null +++ b/Logik und Logikprogrammierung - Cheatsheet.tex @@ -0,0 +1,5437 @@ +\documentclass[a4paper]{article} +\usepackage[ngerman]{babel} +\usepackage[utf8]{inputenc} +\usepackage{multicol} +\usepackage{calc} +\usepackage{ifthen} +\usepackage[landscape]{geometry} +\usepackage{amsmath,amsthm,amsfonts,amssymb} +\usepackage{color,graphicx,overpic} +\usepackage{xcolor, listings} +\usepackage[compact]{titlesec} %less space for headers +\usepackage{mdwlist} %less space for lists +\usepackage{pdflscape} +\usepackage{verbatim} +\usepackage[most]{tcolorbox} +\usepackage[hidelinks,pdfencoding=auto]{hyperref} +\usepackage{fancyhdr} +\usepackage{lastpage} +\pagestyle{fancy} +\fancyhf{} +\fancyhead[L]{Logik und Logikprogrammierung} +\fancyfoot[L]{\thepage/\pageref{LastPage}} +\renewcommand{\headrulewidth}{0pt} %obere Trennlinie +\renewcommand{\footrulewidth}{0pt} %untere Trennlinie + +\pdfinfo{ + /Title (Logik und Logikprogrammierung - Cheatsheet) + /Creator (TeX) + /Producer (pdfTeX 1.40.0) + /Author (Robert Jeutter) + /Subject () +} + +%%% Code Listings +\definecolor{codegreen}{rgb}{0,0.6,0} +\definecolor{codegray}{rgb}{0.5,0.5,0.5} +\definecolor{codepurple}{rgb}{0.58,0,0.82} +\definecolor{backcolour}{rgb}{0.95,0.95,0.92} +\lstdefinestyle{mystyle}{ + backgroundcolor=\color{backcolour}, + commentstyle=\color{codegreen}, + keywordstyle=\color{magenta}, + numberstyle=\tiny\color{codegray}, + stringstyle=\color{codepurple}, + basicstyle=\ttfamily, + breakatwhitespace=false, +} +\lstset{style=mystyle, upquote=true} + +%textmarker style from colorbox doc +\tcbset{textmarker/.style={% + enhanced, + parbox=false,boxrule=0mm,boxsep=0mm,arc=0mm, + outer arc=0mm,left=2mm,right=2mm,top=3pt,bottom=3pt, + toptitle=1mm,bottomtitle=1mm,oversize}} + +% define new colorboxes +\newtcolorbox{hintBox}{textmarker, + borderline west={6pt}{0pt}{yellow}, + colback=yellow!10!white} +\newtcolorbox{importantBox}{textmarker, + borderline west={6pt}{0pt}{red}, + colback=red!10!white} +\newtcolorbox{noteBox}{textmarker, + borderline west={3pt}{0pt}{green}, + colback=green!10!white} + +% define commands for easy access +\renewcommand{\note}[2]{\begin{noteBox} \textbf{#1} #2 \end{noteBox}} +\newcommand{\warning}[1]{\begin{hintBox} \textbf{Warning:} #1 \end{hintBox}} +\newcommand{\important}[1]{\begin{importantBox} \textbf{Important:} #1 \end{importantBox}} + + +% This sets page margins to .5 inch if using letter paper, and to 1cm +% if using A4 paper. (This probably isn't strictly necessary.) +% If using another size paper, use default 1cm margins. +\ifthenelse{\lengthtest { \paperwidth = 11in}} + { \geometry{top=.5in,left=.5in,right=.5in,bottom=.5in} } + {\ifthenelse{ \lengthtest{ \paperwidth = 297mm}} + {\geometry{top=1.3cm,left=1cm,right=1cm,bottom=1.2cm} } + {\geometry{top=1.3cm,left=1cm,right=1cm,bottom=1.2cm} } + } + +% Redefine section commands to use less space +\makeatletter +\renewcommand{\section}{\@startsection{section}{1}{0mm}% + {-1ex plus -.5ex minus -.2ex}% + {0.5ex plus .2ex}%x + {\normalfont\large\bfseries}} +\renewcommand{\subsection}{\@startsection{subsection}{2}{0mm}% + {-1explus -.5ex minus -.2ex}% + {0.5ex plus .2ex}% + {\normalfont\normalsize\bfseries}} +\renewcommand{\subsubsection}{\@startsection{subsubsection}{3}{0mm}% + {-1ex plus -.5ex minus -.2ex}% + {1ex plus .2ex}% + {\normalfont\small\bfseries}} +\makeatother + +% Don't print section numbers +\setcounter{secnumdepth}{0} + +\setlength{\parindent}{0pt} +\setlength{\parskip}{0pt plus 0.5ex} +% compress space +\setlength\abovedisplayskip{0pt} +\setlength{\parskip}{0pt} +\setlength{\parsep}{0pt} +\setlength{\topskip}{0pt} +\setlength{\topsep}{0pt} +\setlength{\partopsep}{0pt} +\linespread{0.5} +\titlespacing{\section}{0pt}{*0}{*0} +\titlespacing{\subsection}{0pt}{*0}{*0} +\titlespacing{\subsubsection}{0pt}{*0}{*0} + +\begin{document} + +\raggedright +\begin{multicols}{3}\scriptsize + % multicol parameters + % These lengths are set only within the two main columns + %\setlength{\columnseprule}{0.25pt} + \setlength{\premulticols}{1pt} + \setlength{\postmulticols}{1pt} + \setlength{\multicolsep}{1pt} + \setlength{\columnsep}{2pt} + + \subsubsection{Probleme mit natürlicher Sprache} + + \begin{enumerate} + \item Zuordnung von Wahrheitswerten zu natürlichsprachigen Aussagen ist problematisch. (Ich habe nur ein bißchen getrunken.) + \item Natürliche Sprache ist oft schwer verständlich. + \item Natürliche Sprache ist mehrdeutig. + \item Natürliche Sprache hängt von Kontext ab. + \end{enumerate} + + \section{Aussagenlogik} + In der Aussagenlogik gehen wir von ``Aussagen'' aus, denen wir (zumindest prinzipiell) Wahrheitswerte zuordnen können. + + Für Aussagen verwenden wir die atomaren Formeln $p,q,r$ bzw. + $p_0,p_1,...$ + + Die Aussagen werden durch ``Operatoren'' verbunden. Beispiele - \ldots{} + und\ldots{} - \ldots{} oder\ldots{} - nicht\ldots{} - wenn\ldots{} + dann\ldots{} - entweder\ldots{} oder\ldots{} , aber nicht beide. - mehr + als die Hälfte der Aussagen \ldots{} gilt. + + Für solche zusammengesetzten Aussagen verwenden wir $\varphi,\psi$ usw. + + Durch die Wahl der erlaubten Operatoren erhält man unterschiedliche + ``Logiken''. + + Da der Wahrheitswert einer zusammengesetzten Aussage nur vom + Wahrheitswert der Teilaussagen abhängen soll, sind Operatoren wie + ``weil'' oder ``obwohl'' nicht zulässig. + + \subsection{Syntax der Aussagenlogik}\label{syntax-der-aussagenlogik} + + Eine atomare Formel hat die Form $p_i$ (wobei + $i\in\mathbb{N}=\{0,1,...\}$). Formeln werden durch folgenden induktiven + Prozess definiert: 1. Alle atomaren Formeln und $\bot$ sind Formeln. 2. + Falls $\varphi$ und $\psi$ Formeln sind, sind auch + $(\varphi\wedge\psi),(\varphi\wedge\psi)$($\varphi \rightarrow\psi$)und + $\lnot\varphi$Formeln. 3. Nichts ist Formel, was sich nicht mittels der + obigen Regeln erzeugen läßt. + + Beispielformel: $\lnot((\lnot p_4 \vee p_1)\wedge\bot)$ + + Bezeichnungen: - Falsum: $\bot$ - Konjunktion: $\wedge$ - Disjunktion: + $\vee$ - Implikation: $\rightarrow$ - Negation: $\lnot$ + + Abkürzungen $p,q,r...$ statt $p_0,p_1,p_2...$ + + $(\bigvee_{i=1}^n \varphi_i$ statt + $(...((\varphi_1\vee\varphi_2)\vee\varphi_3)\vee...\vee\varphi_n)$ + + $(\bigwedge_{i=1}^n \varphi_i)$ statt + $(...((\varphi_1\wedge\varphi_2)\wedge\varphi_3)\wedge...\wedge\varphi_n)$ + + $(\varphi \leftrightarrow \psi)$ statt + $((\varphi\rightarrow\psi)\wedge(\psi\rightarrow\varphi))$ + + Präzedenz der Operatoren: - $\leftrightarrow$ bindet am schwächsten - + $\rightarrow$\ldots{} - $\vee$\ldots{} - $\wedge$\ldots{} - $\lnot$ + bindet am stärksten + + Es gilt also z.B.: + $(\alpha\leftrightarrow\beta\vee\lnot\gamma\rightarrow\sigma\wedge\lnot\eta) = (\alpha\leftrightarrow ((\beta\vee\lnot\gamma)\rightarrow(\sigma\wedge\lnot\eta)))$ + + Dennoch: Zu viele Klammern schaden i.A. nicht. + + \subsection{Natürliches Schließen}\label{natuxfcrliches-schlieuxdfen} + + Ein (mathematischer) Beweis zeigt, wie die Behauptung aus den + Voraussetzungen folgt.\\Analog zeigt ein ``Beweisbaum'' (= + ``Herleitung'' = ``Deduktion''), wie eine Formel der Aussagenlogik aus + Voraussetzungen (ebenfalls Formeln der Aussagenlogik) folgt.\\Diese + ``Deduktionen'' sind Bäume, deren Knoten mit Formeln beschriftet sind: - + an der Wurzel steht die Behauptung (= Konklusion $\varphi$) - an den + Blättern stehen Voraussetzungen (= Hypothesen oder Annahmen aus + $\Gamma$) - an den inneren Knoten stehen ``Teilergebnisse'' und + ``Begründungen'' + + + \includegraphics[width=\linewidth]{Assets/Logik-deduktionsbaum.png} + + \subsection{Konstruktion von + Deduktionen}\label{konstruktion-von-deduktionen} + + Aus der Annahme der Aussage $\varphi$ folgt $\varphi$ unmittelbar: eine + triviale Deduktion + + $\varphi$ mit Hypothesen $\{\varphi\}$ und Konklusion $\varphi$. + + Folgend werden wir - überlegen, wie aus ``einfachen mathematischen + Beweisen'' umfangreichere entstehen können und - parallel + dazudefinieren, wie aus einfachen Deduktionen umfangreichere konstruiert + werden können. + + \subsubsection{Konjunktion}\label{konjunktion} + + \paragraph{Konjunktionseinführung in math. + Beweisen}\label{konjunktionseinfuxfchrung-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``$\varphi$ und $\psi$'' sieht + üblicherweise so aus: - ``Zunächst zeige ich $\varphi$: \ldots{} (hier + steckt die eigentliche Arbeit)\\- Jetzt zeige ich $\psi$: \ldots{} + (nochmehr eigentliche Arbeit)\\- Also haben wir''$\varphi$ und $\psi$" + gezeigt. qed" + + \paragraph{Konjunktionseinführung + (ausführlich)}\label{konjunktionseinfuxfchrung-ausfuxfchrlich} + + Ist D eine Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$ und ist E + eine Deduktion von $\psi$ mit Hypothesen aus $\Gamma$, so ergibt sich + die folgende Deduktion von $\varphi\wedge\psi$ mit Hypothesen aus + $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-konjunktionseinführung.png} + + Kurzform: $\frac{\varphi\quad\psi}{\varphi\wedge\psi} (\wedge I)$ + + \paragraph{Konjunktionselimination + (ausführlich)}\label{konjunktionselimination-ausfuxfchrlich} + + Ist D eine Deduktion von $\varphi\wedge\psi$ mit Hypothesen aus + $\Gamma$, so ergeben sich die folgenden Deduktionen von $\varphi$ bzw. + von $\psi$ mit Hypothesen aus $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-Konjunktionselimination.png} + + Kurzform: + $\frac{\varphi\wedge\psi}{\varphi} (\wedge E_1) \quad\quad \frac{\varphi\wedge\psi}{\psi} (\wedge E_2)$ + + \paragraph{Beispiel}\label{beispiel} + + Wir zeigen $\varphi\wedge\psi$ unter der Hypothese + $\psi\wedge\varphi$:\ldots{} + + + \includegraphics[width=\linewidth]{Assets/Logik-Deduktionsbeispiel.png} + + Dies ist eine Deduktion mit Konklusion $\varphi\wedge\psi$ und Hypothese + $\psi\wedge\varphi$ (zweimal verwendet). + + \subsubsection{Implikation}\label{implikation} + + \paragraph{Implikationseinführung in math. + Beweisen}\label{implikationseinfuxfchrung-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``Aus $\varphi$ folgt $\psi$'' + sieht üblicherweise so aus:\\- ``Angenommen, $\varphi$ gilt. - Dann + \ldots{} (hier steckt die eigentliche Arbeit).\\- Damit gilt $\psi$.\\- + Also haben wir gezeigt, dass $\psi$ aus $\varphi$ folgt. qed'' + + Die Aussage $\varphi$ ist also eine ``temporäre Hypothese''. + + \paragraph{Implikationseinführung + (ausführlich)}\label{implikationseinfuxfchrung-ausfuxfchrlich} + + Ist D eine Deduktion von $\psi$ mit Hypothesen aus + $\Gamma\cup\{\varphi\}$, so ergibt sich die folgende Deduktion von + $\varphi\rightarrow\psi$ mit Hypothesen aus $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-Implikationseinführung.png} + + Kurzform $[\varphi]$ $\vdots$ + $\frac{\psi}{\varphi\rightarrow\psi} (\rightarrow I)$ + + Beispiel: \ldots{} Dies ist eine Deduktion von + $\varphi\rightarrow\varphi$ ohne Hypothesen. + + \paragraph{Implikationselimination in math. + Beweisen}\label{implikationselimination-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``$\psi$ gilt'' über eine + Hilfsaussage sieht so aus: - ``Zunächst zeigen wir, dass $\varphi$ gilt: + \ldots{} - Dann beweisen wir, dass $\psi$ aus $\varphi$ folgt: \ldots{} + - Also haben wir $\psi$ gezeigt. qed'' + + \paragraph{Implikationselimination oder modus ponens + (ausführlich)}\label{implikationselimination-oder-modus-ponens-ausfuxfchrlich} + + Ist D eine Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$ und ist E + eine Deduktion von $\varphi\rightarrow\psi$ mit Hypothesen aus $\Gamma$, + so ergibt sich die folgende Deduktion von $\psi$ mit Hypothesen aus + $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-Implikationselimination.png} + + Kurzform: + $\frac{\varphi\quad \varphi\rightarrow\psi}{\psi} (\rightarrow E)$ + + \paragraph{Beispiel}\label{beispiel-1} + + + \includegraphics[width=\linewidth]{Assets/Logik-Implikationseleimination-beispiel.png} + + Bemerkung: die Indizes 1, 2 und 3 machen deutlich, welche Hypothese bei + welcher Regelanwendung gestrichen wurde. Deduktionen können recht groß + werden. + + Diese Deduktion hat keine Hypothesen! + + \subsubsection{Disjunktion}\label{disjunktion} + + \paragraph{Disjunktionselimination oder Fallunterscheidung in math. + Beweisen}\label{disjunktionselimination-oder-fallunterscheidung-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``$\sigma$ gilt'' mittels + Fallunterscheidung sieht üblicherweise so aus: - ``Zunächst zeigen wir, + dass $\varphi\vee\psi$ gilt: \ldots{} - Gilt $\varphi$, so gilt + $\sigma$, denn \ldots{} - Gilt $\psi$, so gilt ebenfalls $\sigma$, denn + \ldots{} - Also haben wir gezeigt, dass $\sigma$ gilt. qed'' + + Die Aussagen $\varphi$ und $\psi$ sind also wieder ``temporäre + Hypothesen''. + + \paragraph{Disjunktionselimination oder Fallunterscheidung + (ausführlich)}\label{disjunktionselimination-oder-fallunterscheidung-ausfuxfchrlich} + + Ist D eine Deduktion von $\varphi\vee\psi$ mit Hypothesen aus $\Gamma$, + ist E eine Deduktion von $\sigma$ mit Hypothesen aus + $\Gamma\cup\{\varphi\}$und ist F eine Deduktion von $\sigma$ mit + Hypothesen aus $\Gamma\cup\{\psi\}$, so ergibt sich die folgende + Deduktion von $\sigma$ mit Hypothesen aus $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-Disjunktionselimination.png} + + Disjunktionselimination Kurzform: $\quad [\psi] \quad[\varphi]$ + $\quad \vdots \quad\vdots$ + $\frac{\varphi\vee\psi \quad\sigma \quad\sigma}{\sigma} (\vee E)$ + + Disjunktionseinführung (Kurzform) + $\frac{\varphi}{\varphi\vee\psi} (\vee I_1) \quad \frac{\psi}{\varphi\vee\psi} (\vee I_2)$ + + \subsubsection{Negation}\label{negation} + + \paragraph{Negationseinführung in math. + Beweisen}\label{negationseinfuxfchrung-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``$\varphi$ gilt nicht'' sieht + so aus:\\- ``Angenommen,$\varphi$gilt.\\- Dann folgt $0=1$, denn + \ldots{}. Mit anderen Worten, dies führt zu einem Widerspruch. - Also + haben wir gezeigt, dass $\varphi$ nicht gilt. qed''\\- Die Aussage + $\varphi$ ist also wieder eine ``temporäre Hypothese''. + + \paragraph{Negationseinführung + (ausführlich)}\label{negationseinfuxfchrung-ausfuxfchrlich} + + Ist D eine Deduktion von $\bot$ mit Hypothesen aus + $\Gamma\cup\{\varphi\}$, so ergibt sich die folgende Deduktion von + $\lnot\varphi$ mit Hypothesen aus $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-Negationseinführung.png} + + Kurzform: $[\varphi]$ $\vdots$ $\frac{\bot}{\lnot\varphi} (\lnot I)$ + + \paragraph{Negationselimination + (ausführlich)}\label{negationselimination-ausfuxfchrlich} + + Ist D eine Deduktion von $\lnot\varphi$ mit Hypothesen aus $\Gamma$ und + ist E eine Deduktion von $\varphi$ mit Hypothesen aus $\gamma$, so + ergibt sich die folgende Deduktion von $\bot$ mit Hypothesen aus + $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-Negationselimination.png} + + Kurzform: $\frac{\lnot\varphi \quad \varphi}{\bot} (\lnot E)$ + + \subsubsection{Falsum}\label{falsum} + + Hat man ``$0=1$'' bewiesen, so ist man bereit, alles zu glauben: ex + falso sequitur quodlibet + + ausführlich: Ist D eine Deduktion von $\bot$ mit Hypothesen aus + $\Gamma$, so ergibt sich die folgende Deduktion von $\varphi$ mit + Hypothesen aus $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-Falsumeinführung.png} + + Kurzform: $\frac{\bot}{\varphi} (\bot)$ + + \paragraph{math. Widerspruchsbeweis}\label{math.-widerspruchsbeweis} + + Ein indirekter Beweis einer Aussage ``$\varphi$ gilt'' sieht + üblicherweise so aus: - ``Angenommen, $\varphi$ gilt nicht, d.h. + $\lnot\varphi$ gilt. - Dann folgt $0=1$, d.h. ein Widerspruch.\\- Also + haben wir gezeigt, dass $\varphi$ gilt. qed'' + + Die Aussage $\lnot\varphi$ ist also wieder eine ``temporäre Hypothese''. + + \paragraph{reductio ad absurdum + (ausführlich)}\label{reductio-ad-absurdum-ausfuxfchrlich} + + Ist D eine Deduktion von $\bot$ mit Hypothesen aus + $\Gamma\cup\{\lnot\varphi\}$, so ergibt sich die folgende Deduktion von + $\varphi$ mit Hypothesen aus $\Gamma$: + + + \includegraphics[width=\linewidth]{Assets/Logik-reductio-ad-absurdum.png} + + Kurzform: $[\lnot\varphi]$ $\vdots$ $\frac{\bot}{\varphi} (raa)$ + + \subsection{Regeln des natürlichen + Schließens}\label{regeln-des-natuxfcrlichen-schlieuxdfens} + + \begin{quote} + Definition + + Für eine Formelmenge $\Gamma$ und eine Formel $\varphi$ schreiben wir + $\Gamma\Vdash\varphi$ wenn es eine Deduktion gibt mit Hypothesen aus + $\Gamma$ und Konklusion $\varphi$. Wir sagen ``$\varphi$ ist eine + syntaktische Folgerung von $\Gamma$''. + + Eine Formel $\varphi$ ist ein Theorem, wenn $\varnothing\Vdash\varphi$ + gilt. + \end{quote} + + \subsubsection{Bemerkung}\label{bemerkung} + + $\Gamma\Vdash\varphi$ sagt (zunächst) nichts über den Inhalt der Formeln + in $\Gamma\cup\{\varphi\}$ aus, sondern nur über die Tatsache, dass + $\varphi$ mithilfe des natürlichen Schließens aus den Formeln aus + $\Gamma$ hergeleitet werden kann. + + Ebenso sagt ``$\varphi$ ist Theorem'' nur, dass $\varphi$ abgeleitet + werden kann, über ``Wahrheit'' sagt dieser Begriff (zunächst) nichts + aus. + + \subsubsection{Satz}\label{satz} + + Für alle Formeln $\varphi$ und $\psi$ gilt + $\{\lnot(\varphi\vee\psi)\}\Vdash\lnot\varphi\wedge\lnot\psi$. + + Beweis: Wir geben eine Deduktion an\ldots{} - + $\{\lnot\varphi\wedge\lnot\psi\}\Vdash\lnot(\varphi\vee\psi)$ + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-1.png} - + $\{\lnot\varphi\vee\lnot\psi\}\Vdash\lnot(\varphi\wedge\psi)$ + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-2.png} - + $\{\varphi\vee\psi\} \Vdash \psi\vee\varphi$ + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-3.png} + + \subsubsection{Satz}\label{satz-1} + + Für jede Formel $\varphi$ ist $\lnot\lnot\varphi\rightarrow\varphi$ ein + Theorem. + + Beweis: Wir geben eine Deduktion mit Konklusion + $\lnot\lnot\varphi\rightarrow\varphi$ ohne Hypothesen an\ldots{} + + + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-5.png} + + \subsubsection{Satz}\label{satz-2} + + Für jede Formel $\varphi$ ist $\varphi\vee\lnot\varphi$ ein Theorem. + + Beweis: Wir geben eine Deduktion mit Konklusion + $\varphi\vee\lnot\varphi$ ohne Hypothesen an\ldots{} + + + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-6.png} + + Bemerkung: Man kann beweisen, dass jede Deduktion der letzten beiden + Theoreme die Regel (raa) verwendet, sie also nicht ``intuitionistisch'' + gelten. + + \subsubsection{Satz}\label{satz-3} + + $\{\lnot(\varphi\wedge\psi)\}\Vdash\lnot\varphi\vee\lnot\psi$ + + + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-4.png} + + \subsection{Semantik}\label{semantik} + + Formeln sollen Verknüpfungen von Aussagen widerspiegeln, wir haben dies + zur Motivation der einzelnen Regeln des natürlichen Schließens genutzt. + Aber die Begriffe ``syntaktische Folgerung'' und ``Theorem'' sind rein + syntaktisch definiert. + + Erst die jetzt zu definierende ``Semantik'' gibt den Formeln + ``Bedeutung''. + + Idee der Semantik: wenn man jeder atomaren Formel $p_i$ einen + Wahrheitswertzuordnet, so kann man den Wahrheitswert jeder Formel + berechnen. + + Es gibt verschiedene Möglichkeiten, Wahrheitswerte zu definieren: - + zweiwertige oder Boolesche Logik $B=\{0,1\}$: Wahrheitswerte ``wahr''=1 + und ``falsch''= 0 - dreiwertige Kleene-Logik $K_3=\{0,\frac{1}{2},1\}$: + zusätzlicher Wahrheitswert ``unbekannt''$=\frac{1}{2}$ - Fuzzy-Logik + $F=[0,1]$: Wahrheitswerte sind ``Grad der Überzeugtheit'' - unendliche + Boolesche Algebra $B_R$= Menge der Teilmengen von $\mathbb{R}$; + $A\subseteq\mathbb{R}$ ist ``Menge der Menschen, die Aussage für wahr + halten'' - Heyting-Algebra $H_R$= Menge der offenen Teilmengen von + $\mathbb{R}$ - Erinnerung: $A\subseteq\mathbb{R}$ offen, wenn + $\forall a\in A\exists\epsilon >0:(a-\epsilon,a+\epsilon)\subseteq A$, + d.h., wenn $A$ abzählbare Vereinigung von offenen Intervallen $(x,y)$ + ist. + + Beispiele: - offen: + $(0,1), \mathbb{R}_{>0}, \mathbb{R}\backslash\{0\}, \mathbb{R}\backslash\mathbb{N}$ + - nicht offen: + $[1,2), \mathbb{R}_{\geq 0}, \mathbb{Q}, \mathbb{N}, \{\frac{1}{n} | n\in\mathbb{N}\}, \mathbb{R}\backslash\mathbb{Q}$ + + Sei W eine Menge von Wahrheitswerten.\textbackslash{} Eine W-Belegung + ist eine Abbildung $B:V\rightarrow W$, wobei + $V\subseteq\{p_0 ,p_1 ,...\}$ eine Menge atomarer Formeln ist. + + Die W-Belegung $B:V\rightarrow W$ paßt zur Formel $\phi$, falls alle + atomaren Formeln aus $\phi$ zu V gehören. + + Sei nun B eine W-Belegung. Was ist der Wahrheitswert der Formel + $p_0\vee p_1$ unter der Belegung B? + + Zur Beantwortung dieser Frage benötigen wir eine Funktion + $\vee_W :W\times W\rightarrow W$ (analog für + $\wedge,\rightarrow,\lnot$). + + \subsection{Wahrheitswertebereiche}\label{wahrheitswertebereiche} + + \begin{quote} + Definition: Sei W eine Menge und $R\subseteq W\times W$ eine binäre + Relation. - R ist reflexiv, wenn $(a,a)\in R$ für alle $a\in W$ gilt. - + R ist antisymmetrisch, wenn $(a,b),(b,a)\in R$ impliziert, dass $a=b$ + gilt (für alle $a,b\in W$). - R ist transitive, wenn $(a,b),(b,c)\in R$ + impliziert, dass $(a,c)\in R$ gilt (für alle $a,b,c\in W$). - R ist eine + Ordnungsrelation, wenn R reflexiv, antisymmetrisch und transitiv ist. In + diesem Fall heißt das Paar $(W,R)$ eine partiell geordnete Menge. + \end{quote} + + Beispiel 1. Sei $\leq$ übliche Ordnung auf $\mathbb{R}$und + $W\subseteq\mathbb{R}$. Dann ist $(W,\leq)$ partiell geordnete Menge. 2. + Sei $X$ eine Menge und $W\subseteq P(X)$. Dann ist $(W,\subseteq)$ + partiell geordnete Menge. 3. Sei $W=P(\sum *)$ und $\leq_p$ die Relation + ``es gibt Polynomialzeitreduktion'' (vgl. ``Automaten, Sprachen und + Komplexität''). Diese Relation ist reflexiv, transitiv, aber nicht + antisymmetrisch (denn $3-SAT\leq_{p} HC$ und $HC\leq_{p} 3-SAT$). + + \begin{quote} + Definition: Sei $(W,\leq)$ partiell geordnete Menge, $M\subseteq W$ und + $a\in W$. - a ist obere Schranke von $M$, wenn $m\leq a$ für alle + $m\in M$ gilt. - a ist kleinste obere Schranke oder Supremum von $M$, + wenn $a$ obere Schranke von $M$ ist und wenn $a\leq b$ für alle oberen + Schranken $b$ von $M$ gilt. Wir schreiben in diesem Fall $a=sup \ M$. - + a ist untere Schranke von $M$, wenn $a\leq m$ für alle $m\in M$ gilt. - + a ist größte untere Schranke oder Infimum von $M$, wenn a untere + Schranke von $M$ ist und wenn $b\leq a$ für alle unteren Schranken $b$ + von $M$ gilt. Wir schreiben in diesem Fall $a=inf\ M$. + \end{quote} + + Beispiel 1. betrachte $(W,\leq)$ mit $W=\mathbb{R}$ und $\leq$ übliche + Ordnung auf $\mathbb{R}$. - Dann gelten $sup[0,1] = sup(0,1) =1$. - + $sup\ W$ existiert nicht (denn $W$ hat keine obere Schranke). 2. + betrachte $(W,\subseteq)$ mit $X$ Menge und $W =P(X)$. - + $sup\ M=\bigcup_{A\in M} A$ für alle $M\subseteq W$ 3. betrachte + $(W,\subseteq)$ mit $W=\{\{0\},\{1\},\{0,1,2\},\{0,1,3\}\}$. - + $sup\{\{0\},\{0,1,2\}\}=\{0,1,2\}$ - $\{0,1,2\}$ und $\{0,1,3\}$ sind + die oberen Schranken von $M=\{\{0\},\{1\}\}$, aber $M$ hat kein Supremum + + \begin{quote} + Definition: Ein (vollständiger) Verband ist eine partiell geordnete + Menge $(W,\leq)$, in der jede Menge $M\subseteq W$ ein Supremum $sup\ M$ + und ein Infimum $inf\ M$ hat. In einem Verband $(W,\leq)$ definieren + wir: - $0_W = inf\ W$ und $1_W= sup\ W$ - $a\wedge_W b= inf\{a,b\}$ und + $a\vee_W b= sup\{a,b\}$ für $a,b\in W$ + \end{quote} + + Bemerkung: In jedem Verband $(W,\leq)$ gelten $0_W= sup\ \varnothing$ + und $1_W= inf\ \varnothing$ (denn jedes Element von $W$ ist obere und + untere Schranke von $\varnothing$). + + \begin{quote} + Definition: Ein Wahrheitswertebereich ist ein Tupel + $(W,\leq,\rightarrow W,\lnot W)$, wobei $(W,\leq)$ ein Verband und + $\rightarrow W:W^2 \rightarrow W$ und $\lnot W:W\rightarrow W$ + Funktionen sind. + \end{quote} + + \subsubsection{Beispiel}\label{beispiel-2} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + Der Boolesche Wahrheitswertebereich B ist definiert durch die + Grundmenge $B=\{0,1\}$, die natürliche Ordnung $\leq$ und die + Funktionen $\lnot_B (a) = 1-a$, $\rightarrow_B(a,b) = max(b, 1 -a)$. + Hier gelten: + + \begin{itemize} + \item + $0_B=0$, $1_B= 1$, + \item + $a\wedge_B b= min(a,b)$, $a\vee_B b= max(a,b)$ + \end{itemize} + \item + Der Kleenesche Wahrheitswertebereich $K_3$ ist definiert durch die + Grundmenge $K_3=\{0,\frac{1}{2},1\}$ mit der natürlichen Ordnung + $\leq$ und durch die Funktionen $\lnot_{K_3} (a) = 1 -a $, + $\rightarrow_{K_3} (a,b) = max(b, 1-a)$. Hier gelten: + \item + $\lnot_{K_3} = 0$, $1_{K_3} = 1$ + \item + $a\wedge_{K_3} b= min(a,b)$, $a\vee_{K_3} b= max(a,b)$ + \item + Der Wahrheitswertebereich F der Fuzzy-Logik ist definiert durch die + Grundmenge $F=[0,1]\subseteq\mathbb{R}$ mit der natürlichen Ordnung + $\leq$ und durch die Funktionen $\lnot_F (a) = 1-a$, + $\rightarrow_F (a,b) = max(b, 1-a)$. Hier gelten: + \item + $0_F= 0$, $1_F= 1$ + \item + $a\wedge_F b= min(a,b)$, $a\vee_F b= max(a,b)$ + \item + Der Boolesche Wahrheitswertebereich $B_R$ ist definiert durch die + Grundmenge $B_R=\{A|A\subseteq \mathbb{R}\}$ mit der Ordnung + $\subseteq$ und durch die Funktionen + $\lnot_{B_R} (A) =\mathbb{R}\backslash A$, + $\rightarrow_{B_R} (A,B) = B\cup\mathbb{R}\backslash A$. Hier gelten: + \item + $0_{B_R}=\varnothing$, $1_{B_R}=\mathbb{R}$ + \item + $A\wedge_{B_R} B=A\cap B$, $A\vee_{B_R} B=A\cup B$ + \item + Der Heytingsche Wahrheitswertebereich $H_R$ ist definiert durch die + Grundmenge + $H_{mathbb{R}} =\{A\subseteq\mathbb{R} | \text{A ist offen}\}$, die + Ordnung $\subseteq$ und durch die Funktionen + $\lnot_{H_R} (A) = Inneres(\mathbb{R}\backslash A)$, + $\rightarrow_{H_R} (A,B) =Inneres(B\cup \mathbb{R}\backslash A)$. Hier + gelten: + \item + $0_{H_R}=\varnothing$, $1_{H_R}=\mathbb{R}$ + \item + $A\wedge_{H_R} B= A\cap B$, $A\vee_{H_R} B=A\cup B$ + \item + Erinnerung: + $Inneres(A) =\{a\in A|\exists \epsilon > 0 : (a-\epsilon,a+\epsilon)\subseteq A\}$ + \item + Beispiele: + $Inneres((0,1))=(0,1)=Inneres([0,1]),Inneres(N)=\varnothing,Inneres(\mathbb{R}_{\geq 0}) = \mathbb{R}_{> 0}$ + \end{itemize} + + Sei W ein Wahrheitswertebereich und B eine W-Belegung. Induktiv über den + Formelaufbau definieren wir den Wahrheitswert $\hat{B}(\phi)\in W$ jeder + zu $B$ passenden Formel $\phi$: - $\hat{B}(\bot) = 0_W$ - + $\hat{B}(p) = B(p)$ falls $p$ eine atomare Formel ist - + $\hat{B}((\phi\wedge \psi )) = \hat{B}(\phi)\wedge_W \hat{B}(\psi )$ - + $\hat{B}((\phi\vee \psi )) = \hat{B}(\phi)\vee_W \hat{B}(\psi )$ - + $\hat{B}((\phi\rightarrow \psi )) = \rightarrow W(\hat{B}(\phi),\hat{B}(\psi ))$ + - $\hat{B}(\lnot\phi) = \lnot W(\hat{B}(\phi))$ + + Wir schreiben im folgenden $B(\phi)$ anstatt $\hat{B}(\phi)$. + + Beispiel: Betrachte die Formel + $\phi= ((p\wedge q)\rightarrow (q\wedge p))$. - Für eine beliebige + B-Belegung $B:\{p,q\}\rightarrow B$ gilt + $B((p\wedge q)\rightarrow (q\wedge p)) = max(B(q\wedge p), 1 -B(p\wedge q)) = max(min(B(q),B(p)), 1 -min(B(p),B(q))) = 1 = 1_B$ + - Für die $K_3$-Belegung $B:\{p,q\}\rightarrow K_3$ mit + $B(p) =B(q) = \frac{1}{2}$\} gilt + $B((p\wedge q)\rightarrow (q\wedge p)) = max(B(q\wedge p), 1 -B(p\wedge q))= max(min(B(q),B(p)), 1 -min(B(p),B(q))) = \frac{1}{2} \not= 1_{K_3}$ + - analog gibt es eine F-Belegung $B:\{p,q\}\rightarrow F$, so dass + $B((p\wedge q)\rightarrow (q\wedge p)) \not = 1_F$ gilt. - Für eine + beliebige $H_{mathbb{R}}$-Belegung $B:\{p,q\}\rightarrow H_R$ gilt + $B((p\wedge q)\rightarrow (q\wedge p)) = Inneres(B(q\wedge p)\cup \mathbb{R}\backslash B(p\wedge q)) = Inneres((B(q)\cap B(p))\cup \mathbb{R}\backslash (B(p)\cap B(q))) = Inneres(\mathbb{R}) = \mathbb{R} = 1_{H_R}$ + + \subsection{Folgerung und Tautologie}\label{folgerung-und-tautologie} + + Sei W ein Wahrheitswertebereich. Eine Formel $\phi$ heißt eine + W-Folgerung der Formelmenge $\Gamma$, falls für jede W-Belegung B, die + zu allen Formeln aus $\Gamma \cup\{\phi\}$ paßt, gilt: + $inf\{B(\gamma )|\gamma \in \Gamma \}\leq B(\phi)$ + + Wir schreiben $\Gamma \Vdash W\phi$, falls $\phi$ eine W-Folgerung von + $\Gamma$ ist. + + Bemerkung: Im Gegensatz zur Beziehung $\Gamma \vdash \phi$, d.h. zur + syntaktischen Folgerung, ist $\Gamma \Vdash W \phi$ eine semantische + Beziehung. + + Eine W-Tautologie ist eine Formel $\phi$ mit $\varnothing \Vdash W\phi$, + d.h. $B(\phi) = 1_W$ für alle passenden W-Belegungen B (denn + $inf\{\hat{B}(\gamma )|\gamma \in \varnothing \}= inf \varnothing = 1_W)$. + + Wahrheitstafel für den Booleschen Wahrheitswertebereich B: + + \begin{tabular}{llllllll} + RL & AK & BK & $AK\vee BK$ & $AK\rightarrow BK$ & $(BK\wedge RL)\rightarrow\lnot AK$ & RL & $\lnot AK$ \\\hline + 0 & 0 & 0 & 0 & 1 & 1 & 0 & 1 \\ + 0 & 0 & 1 & 1 & 1 & 1 & 0 & 1 \\ + 0 & 1 & 0 & 1 & 0 & 1 & 0 & 0 \\ + 0 & 1 & 1 & 1 & 1 & 1 & 0 & 0 \\ + 1 & 0 & 0 & 0 & 1 & 1 & 1 & 1 \\ + 1 & 0 & 1 & 1 & 1 & 1 & 1 & 1 \\ + 1 & 1 & 0 & 1 & 0 & 1 & 1 & 0 \\ + 1 & 1 & 1 & 1 & 1 & 0 & 1 & 0 \\ + \end{tabular} + + Wir erhalten also + $\{(AK\vee BK),(AK\rightarrow BK), ((BK\wedge RL)\rightarrow \lnot AK),RL\} \Vdash_B \lnot AK$ + und können damit sagen: + + ``Wenn die Aussagen''Bauteil A oder Bauteil B ist kaputt" und ``daraus, + dass Bauteil A kaputt ist, folgt, dass Bauteil B kaputt ist'' + und\ldots{} wahr sind, \ldots{} dann kann man die Folgerung ziehen: die + Aussage ``das Bauteil A ist heil'' ist wahr." + + Erinnerung aus der ersten Vorlesung: + $\{(AK\vee BK),(AK\rightarrow BK), ((BK\wedge RL)\rightarrow \lnot AK),RL\} \vdash \lnot AK$ + + Beispiel Sei $\phi$ beliebige Formel mit atomaren Formeln in V. - Sei + $B:V\rightarrow B$ eine B-Belegung. Dann gilt + + \begin{verbatim} +$B(\lnot\lnot\phi\rightarrow\phi) = \rightarrow B(\lnot B\lnot B(B(\phi)),B(\phi)) = max(B(\phi), 1 -( 1 -( 1 -B(\phi)))) = max(B(\phi), 1 -B(\phi)) = 1 = 1_B$. + +Also ist $\lnot\lnot\phi\rightarrow\phi$ eine B-Tautologie (gilt ebenso für den Wahrheitswertebereich $B_R$). +\end{verbatim} + + \begin{itemize} + \item + Sei $B:V\rightarrow H_R$ eine $H_R$-Belegung mit + $B(\phi) =R\backslash\{0\}$. Dann gelten + + \begin{itemize} + \item + $B(\lnot\phi) = Inneres(\mathbb{R}\backslash B(\phi)) = Inneres(\{0\}) =\varnothing$ + \item + $B(\lnot\lnot\phi) = Inneres(\mathbb{R}\backslash B(\lnot\phi)) = Inneres(\mathbb{R}) = \mathbb{R}$ + \item + $B(\lnot\lnot\phi\rightarrow\phi) = \rightarrow_{H_R} (B(\lnot\lnot\phi),B(\phi)) = \rightarrow_{H_R} (\mathbb{R},\mathbb{R}\backslash \{0\}) = Inneres(\mathbb{R}\backslash\{0\}\cup\mathbb{R}\backslash\mathbb{R}) = \mathbb{R}\backslash\{0\}\not =\mathbb{R}= 1_{H_R}$ + \end{itemize} + + Also ist $\lnot\lnot\phi\rightarrow\phi$ keine $H_R$-Tautologie (gilt + ebenso für die Wahrheitswertebereiche $K_3$ und $F$). + \item + Sei $B:V\rightarrow B$ eine B-Belegung. Dann gilt + + $B(\phi\vee\lnot\phi) = max(B(\phi), 1 -B(\phi)) = 1 = 1_B$. + + Also ist $\phi\vee\lnot\phi$ eine B-Tautologie (gilt ebenso für den + Wahrheitswertebereich $B_R$). + \item + Sei $B:V\rightarrow H_R$ eine $H_R$-Belegung mit + $B(\phi)=\mathbb{R}\backslash\{0\}$. Dann gilt + $B(\phi\vee\lnot\phi) = B(\phi)\cup B(\lnot\phi) = \mathbb{R}\backslash\{0\}\cup \varnothing \not= 1_{H_R}$. + + Also ist $\phi\vee\lnot\phi$ keine $H_R$-Tautologie (gilt ebenso für + die Wahrheitswertebereiche $K_3$ und $F$). + \item + Sei $B:V\rightarrow B$ eine B-Belegung. Dann gilt + + $B(\lnot\phi\rightarrow\bot) = \rightarrow_B(B(\lnot\phi),B(\bot)) = max(0,1-B(\lnot \phi)) = 1 -( 1 -B(\phi)) =B(\phi)$. + + Also haben wir $\{\lnot\phi\rightarrow\bot\}\Vdash B\phi$ und + $\{\phi\}\Vdash B\lnot \phi\rightarrow\bot$. + \item + Ebenso erhält man: + + \begin{itemize} + \item + $\{\lnot\phi\rightarrow\bot\}\Vdash_{K_3} \phi$ + \item + $\{\phi\}\Vdash_{K_3} \lnot\phi\rightarrow\bot$ + \item + $\{\lnot\phi\rightarrow\bot\}\Vdash_F\phi$ + \item + $\{\phi\}\Vdash F\lnot\phi\rightarrow\bot$ + \end{itemize} + \item + Sei $B:D\rightarrow H_R$ eine $H_R$-Belegung mit + $B(\phi) =\mathbb{R}\backslash\{0\}$. Dann gilt + $B(\lnot\phi\rightarrow\bot) = Inneres(B(\bot )\cup \mathbb{R}\backslash B(\lnot\phi))= Inneres(\varnothing \cup \mathbb{R}\backslash\varnothing)= \mathbb{R} \not\supseteq B(\phi)$. + + also $\{\lnot\phi\rightarrow\bot\}\not\Vdash_{H_R} \phi$. + + Es gilt aber $\{\phi\}\Vdash_{H_R}\lnot \phi\rightarrow\bot$. + \end{itemize} + + Zusammenfassung der Beispiele + + \begin{tabular}{lllllll} + & B & $B_R$ & $K_3$ & F & $H_R$ & \\\hline + $\varnothing\Vdash_W\lnot\lnot\phi\rightarrow\phi$ & Y & Y & - & - & - & + $\varnothing\vdash \lnot\lnot\phi\rightarrow\phi$ \\ + $\varnothing\Vdash_W\phi\vee\lnot\phi$ & Y & Y & - & - & - & + $\varnothing\vdash\phi\vee\lnot\phi$ \\ + $\{\lnot\phi\rightarrow\bot\}\Vdash_W\phi$ & Y & Y & Y & Y & - & + $\{\lnot\phi\rightarrow\bot\}\vdash\phi$ \\ + $\{\phi\}\Vdash_W\lnot\phi\rightarrow\bot$ & Y & Y & Y & Y & Y & + $\{\phi\}\vdash\lnot\phi\rightarrow\bot$ \\ + \end{tabular} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + $Y$ in Spalte W:W-Folgerung gilt + \item + $-$ in Spalte W:W-Folgerung gilt nicht + \end{itemize} + + \begin{quote} + Überblick: Wir haben definiert - $\Gamma\vdash\phi$ syntaktische + Folgerung - Theorem (``hypothesenlos ableitbar'') - + $\Gamma\Vdash_W \phi$ (semantische) W-Folgerung - W-Tautologie (``wird + immer zu $1_W$ ausgewertet'') + \end{quote} + + Frage: Was ist die Beziehung zwischen diesen Begriffen, insbes. zwischen + ``Theorem'' und ``W-Tautologie''? Da z.B. B-Folgerung + $\not =K_3$-Folgerung, hängt die Anwort von W ab. + + \subsection{Korrektheit}\label{korrektheit} + + Können wir durch mathematische Beweise zu falschen Aussagenkommen? + + Können wir durch das natürliche Schließen zu falschen Aussagen kommen? + + Existiert eine Menge $\Gamma$ von Formeln und eine Formel $\varphi$ mit + $\Gamma\vdash\varphi$ und $\Gamma\not\Vdash_W \varphi$? Für welche + Wahrheitswertebereiche W? + + Frage für diese Vorlesung: Für welche Wahrheitswertebereiche W gilt + $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_W \varphi$ bzw. $\varphi$ + ist Theorem $\Rightarrow\varphi$ ist W-Tautologie? + + Beispiel: Betrachte den Kleeneschen Wahrheitswertebereich $K_3$. - Sei + $p$ atomare Formel. $\frac{[p]^4}{p\rightarrow p}$ Also gilt + $\varnothing\vdash p\rightarrow p$, d.h. $p\rightarrow p$ ist Theorem. - + Sei $B$ $K_3$-Belegung mit $B(p)=\frac{1}{2}$. Dann gilt + $B(p\rightarrow p) = max(B(p), 1-B(p)) =\frac{1}{2}$, also + $inf\{B(\gamma)|\gamma\in\varnothing\}= 1 >\frac{1}{2} = B(p\rightarrow p)$. + Damit haben wir gezeigt $\varnothing\not\Vdash_{K_3} p\rightarrow p$. + + Die Implikation $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_W \varphi$ + gilt also NICHT für den Kleeneschen Wahrheitswertebereich $W=K_3$ und + damit auch NICHT für den Wahrheitswertebereich der Fuzzy-Logik $F$. + + \begin{quote} + Korrektheitslemma für nat. Schließen \& Wahrheitswertebereich B + + Sei $D$ eine Deduktion mit Hypothesen in der Menge $\Gamma$ und + Konklusion $\varphi$. Dann gilt $\Gamma\vdash_B \varphi$, d.h. + $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\varphi)$ für alle passenden + B-Belegungen $B$. + \end{quote} + + Beweis: Induktion über die Größe der Deduktion $D$ (d.h. Anzahl der + Regelanwendungen). - I.A.: die kleinste Deduktion $D$ hat die Form + $\varphi$ mit Hypothese $\varphi$ und Konklusion $\varphi$. Sei $B$ + passendeB-Belegung. Hypothesen von $D$ in + $\Gamma\Rightarrow\varphi\in\Gamma\Rightarrow inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\varphi)\Rightarrow\Gamma\vdash_B \varphi$ + - I.V.: Behauptung gelte für alle Deduktionen, die kleiner sind als $D$. + - I.S.: Wir unterscheiden verschiedene Fälle, je nachdem, welche Regel + als letzte angewandt wurde. - $(\wedge I)$ Die Deduktion hat die Form + $\frac{\alpha\quad\beta}{\alpha\wedge\beta}$ mit + $\varphi=\alpha\wedge\beta$. Sei $B$ passende B-Belegung. Nach IV gelten + $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\alpha)$ und + $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\beta)$ und damit + $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\alpha)\wedge_B B(\beta)=B(\alpha\wedge\beta) =B(\varphi)$. + Da $B$ beliebig war, haben wir $\Gamma\vdash_B \varphi$ gezeigt. - + $(\vee E)$ Die Deduktion $D$ hat die Form + $\frac{\alpha\vee\beta\quad\phi\quad\phi}{\phi}$ Also gibt es Deduktion + $E$ mit Hypothesen in $\Gamma$ und Konklusion $\alpha\vee\beta$ und + Deduktionen $F$ und $G$ mit Hypothesen in $\Gamma\cup\{\alpha\}$ bzw. + $\Gamma\cup\{\beta\}$ und Konklusion $\varphi$. Sei $B$ passende + B-Belegung. Nach IV gelten + $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\alpha\vee\beta)$ (1) + $inf\{B(\gamma)|\gamma\in\Gamma\cup\{\alpha\}\}\leq B(\varphi)$ (2) + $inf\{B(\gamma)|\gamma\in\Gamma\cup\{\beta\}\}\leq B(\varphi)$ (3) Wir + unterscheiden zwei Fälle: - $B(\alpha)\leq B(\beta)$: + $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\alpha\vee\beta) =B(\alpha)\vee_B B(\beta) =B(\beta)$ + impliziert + $inf\{B(\gamma)|\gamma\in\Gamma\}= inf\{B(\gamma)|\gamma\in\Gamma\cup\{\beta\}\}\leq B(\varphi)$ + - $B(\alpha)>B(\beta)$: analog Da $B$ beliebig war, haben wir + $\Gamma\vdash_B \varphi$ gezeigt. - $(\rightarrow I)$ Die DeduktionDhat + die Form $\frac{\beta}{\alpha\rightarrow\beta}$ mit + $\varphi=\alpha\rightarrow\beta$. Sei $B$ eine passende B-Belegung. Nach + IV gilt $inf\{B(\gamma)|\gamma\in\Gamma\cup\{\alpha\}\}\leq B(\beta)$ + Wir unterscheiden wieder zwei Fälle: - + $B(\alpha)=0:inf\{B(\gamma)|\gamma\in\Gamma\}\leq 1 =\rightarrow_B(B(\alpha),B(\beta)) = B(\alpha\rightarrow\beta) =B(\varphi)$ + - + $B(\alpha)=1:inf\{B(\gamma)|\gamma\in\Gamma\}=inf\{B(\gamma)|\gamma\in\Gamma\cup\{\alpha\}\}\leq B(\beta) =\rightarrow_B (B(\alpha),B(\beta)) = B(\alpha\rightarrow\beta) =B(\varphi)$ + Da $B$ beliebig war, habe wir $\Gamma\vdash_B \varphi$ gezeigt. - + $(raa)$ Die DeduktionDhat die Form $\frac{\bot}{\phi}$ Sei $B$ eine + passende B-Belegung. Nach IV gilt + $inf\{B(\gamma)|\gamma\in\Gamma\cup\{\lnot\varphi\}\}\leq B(\bot) = 0$. + Wir unterscheiden wieder zwei Fälle: - + $inf\{B(\gamma)|\gamma\in\Gamma\}=0$: dann gilt + $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\varphi)$. - + $inf\{B(\gamma)|\gamma\in\Gamma\}=1$: Wegen + $inf\{B(\gamma)|\gamma\in\Gamma\cup\{\lnot\varphi\}\}=0$ folgt + $0 =B(\lnot\varphi)=\lnot_B (B(\varphi))$ und daher + $B(\varphi)=1\geq inf\{B(\gamma)|\gamma\in\Gamma\}$. Da $B$ beliebig + war, haben wir $\Gamma\vdash_B \varphi$ gezeigt. + + Ist die letzte Schlußregel in der Deduktion $D$ von der Form + $(\wedge I), (\vee E), (\rightarrow I)$ oder $(raa)$, so haben wir die + Behauptung des Lemmas gezeigt. Analog kann dies für die verbleibenden + Regeln getan werden. + + \begin{quote} + Korrektheitssatz für natürliches Schließen \& Wahrheitswertebereich $B$ + + Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt + $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_B\varphi$. + \end{quote} + + Beweis: Wegen $\Gamma\vdash\varphi$ existiert eine Deduktion $D$ mit + Hypothesen in $\Gamma$ und Konklusion $\varphi$. Nach dem + Korrektheitslemma folgt $\Gamma\vdash_B \varphi$. + + \begin{quote} + Korollar: Jedes Theorem ist eine B-Tautologie. + \end{quote} + + \begin{quote} + Korrektheitssatz für natürliches Schließen \& Wahrheitswertebereich $B$ + + Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt + $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_{B_\mathbb{R}}\varphi$. + \end{quote} + + Beweis: 1. Variante: verallgemeinere den Beweis von Korrektheitslemma + und Korrektheitssatz für $B$ auf $B_\mathbb{R}$ (Problem: wir haben + mehrfach ausgenutzt, dass $B=\{0,1\}$ mit $0<1$) 2. Variante: Folgerung + aus Korrektheitssatz für $B$. + + \begin{quote} + Korollar: Jedes Theorem ist eine $B_\mathbb{R}$-Tautologie. + \end{quote} + + \begin{quote} + Korrektheitslemma für nat. Schließen \& Wahrheitswertebereich + $H_{mathbb{R}}$ + + Sei $D$ eine Deduktion mit Hypothesen in der Menge $\Gamma$ und + Konklusion $\varphi$, die die Regel $(raa)$ nicht verwendet. Dann gilt + $\Gamma\vdash_{H_\mathbb{R}}\varphi$. + \end{quote} + + Beweis: ähnlich zum Beweis des Korrektheitslemmas für den + Wahrheitswertebereich B. Nur die Behandlung der Regel $(raa)$ kann nicht + übertragen werden. + + Beispiel: Sei $p$ eine atomare Formel. + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-7.png} Also gilt + $\{\lnot\lnot p\}\vdash p$, d.h. $p$ ist syntaktische Folgerung von + $\lnot\lnot p$. - Sei $B$ $H_{mathbb{R}}$-Belegung mit + $B(p)=\mathbb{R}\backslash\{0\}$. - + $\Rightarrow B(\lnot\lnot p) =\mathbb{R}\not\subseteq \mathbb{R}\backslash\{0\}=B(p)$ + - $\Rightarrow\lnot\lnot p\not\Vdash_{H_{mathbb{R}}} p$, d.h. $p$ ist + keine $H_{mathbb{R}}$ -Folgerung von $\lnot\lnot p$. + + \begin{quote} + Korrektheitssatz für nat. Schließen \& Wahrheitswertebereich + $H_{mathbb{R}}$ + + Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt + $\Gamma\vdash\varphi$ ohne $(raa)$ + $\Rightarrow\Gamma\vdash_{H_{mathbb{R}}}\varphi$. + \end{quote} + + \begin{quote} + Korollar: Jedes $(raa)$-frei herleitbare Theorem ist eine + $H_{mathbb{R}}$-Tautologie. + \end{quote} + + Folgerung: Jede Deduktion der Theoreme + $\lnot\lnot\varphi\rightarrow\varphi$ und $\varphi\vee\lnot\varphi$ ohne + Hypothesen verwendet $(raa)$. + + \subsection{Vollständigkeit}\label{vollstuxe4ndigkeit} + + Können wir durch mathematische Beweise zu allen korrekten Aussagen + kommen? + + Können wir durch das natürliche Schließen zu allen korrekten Aussagen + kommen? + + Existiert eine Menge $\Gamma$ von Formeln und eine Formel $\varphi$ mit + $\Gamma\vdash_W\varphi$ und $\Gamma\not\vdash\varphi$? Für welche + Wahrheitswertebereiche $W$? + + Frage für diese Vorlesung: Für welche Wahrheitswertebereiche $W$ gilt + $\Gamma\vdash_W \varphi\Rightarrow\Gamma\vdash\varphi$ bzw. $\varphi$ + ist $W$-Tautologie $\Rightarrow\varphi$ ist Theorem? + + \subsubsection{Plan}\label{plan} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + Sei $W$ einer der Wahrheitswertebereiche + $B,K_3 ,F ,B_\mathbb{R}, H_{mathbb{R}}$. + \item + z.z. ist $\Gamma\vdash_W\varphi\Rightarrow\Gamma\vdash\varphi$. + \item + dies ist äquivalent zu + $\Gamma\not\vdash\varphi\Rightarrow\Gamma\not\Vdash_W \varphi$. + \item + hierzu gehen wir folgendermaßen vor: + \item + $\Gamma \not\Vdash_W\varphi$ + \item + $\Leftrightarrow$ $\Gamma\cup\{\lnot\varphi\}$ konsistent + \item + $\Rightarrow$ $\exists\Delta\subseteq\Gamma\cup\{\lnot\varphi\}$ + maximal konsistent + \item + $\Rightarrow$ $\Delta$ erfüllbar + \item + $\Rightarrow$ $\Gamma\cup\{\lnot\varphi\}$ erfüllbar + \item + $\Leftrightarrow$ $\Gamma\not\Vdash_B \varphi$ + \item + $\Rightarrow$ $\Gamma\not\Vdash\varphi$ + \end{itemize} + + \subsubsection{Konsistente Mengen}\label{konsistente-mengen} + + \begin{quote} + Definition + + Sei $\Gamma$ eine Menge von Formeln. $\Gamma$ heißt inkonsistent, wenn + $\Gamma\vdash\bot$ gilt. Sonst heißt $\Gamma$ konsistent. + \end{quote} + + \begin{quote} + Lemma + + Sei $\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt + $\Gamma\not\vdash\varphi \Leftrightarrow \Gamma\cup\{\lnot\varphi\}$ + konsistent. + \end{quote} + + Beweis: Wir zeigen + ``$\Gamma\vdash\varphi\Leftrightarrow \Gamma\cup\{\lnot\varphi\}$ + inkonsistent'': - Richtung ``$\Rightarrow$'', gelte also + $\Gamma \vdash \varphi$. - $\Rightarrow$ es gibt Deduktion $D$ mit + Hypothesen in $\Gamma$ und Konklusion $\varphi$ - $\Rightarrow$ Wir + erhalten die folgende Deduktion mit Hypothesen in + $\Gamma\cup\{\lnot\varphi\}$ und Konklusion $\bot$: + $\frac{\lnot\varphi\quad\varphi}{\bot}$ - + $\Rightarrow\Gamma\cup\{\lnot\varphi\}\vdash\bot$, + d.h.$\Gamma\cup\{\lnot\varphi\}$ ist inkonsistent. - Richtung + ``$\Leftarrow$'', sei also $\Gamma\cup\{\lnot\varphi\}$ inkonsistent. - + $\Rightarrow$ Es gibt Deduktion $D$ mit Hypothesen in + $\Gamma\cup\{\lnot\varphi\}$ und Konklusion $\bot$. - $\Rightarrow$ Wir + erhalten die folgende Deduktion mit Hypothesen in $\Gamma$ und + Konklusion $\varphi$: $\frac{\bot}{\varphi}$ - $\Gamma\vdash\varphi$ + + \subsubsection{Maximal konsistente + Mengen}\label{maximal-konsistente-mengen} + + \begin{quote} + Definition + + Eine Formelmenge $\Delta$ ist maximal konsistent, wenn sie konsistent + ist und wenn gilt ``$\sum\supseteq\Delta$ konsistent + $\Rightarrow\sum = \Delta$''. + \end{quote} + + \begin{quote} + Satz + + Jede konsistente Formelmenge $\Gamma$ ist in einer maximal konsistenten + Formelmenge $\Delta$ enthalten. + \end{quote} + + Beweis: Sei $\varphi_1,\varphi_2,...$ eine Liste aller Formeln (da wir + abzählbar viele atomare Formeln haben, gibt es nur abzählbar viele + Formeln) + + Wir definieren induktiv konsistente Mengen $\Gamma_n$: - Setze + $\Gamma_1 = \Gamma$ - Setze + $\Gamma_{n+1}= \begin{cases} \Gamma_n\cup\{\varphi_n\}\quad\text{ falls diese Menge konsistent} \\ \Gamma_n \quad\text{sonst}\end{cases}$ + + Setze nun $\Delta =\bigcup_{n\geq 1} \Gamma_n$. 1. Wir zeigen indirekt, + dass $\Delta$ konsistent ist: Angenommen, $\Delta\vdash\bot$. - + $\Rightarrow$ Es gibt Deduktion $D$ mit Konklusion $\bot$ und endlicher + Menge von Hypothesen $\Delta'\subseteq\Delta$. - $\Rightarrow$ Es gibt + $n\geq 1$ mit $\Delta'\subseteq\Gamma_n$ - + $\Rightarrow \Gamma_n\vdash\bot$, zu $\Gamma_n$ konsistent. Also ist + $\Delta$ konsistent. 2. Wir zeigen indirekt, dass $\Delta$ maximal + konsistent ist. Sei also $\sum\supseteq\Delta$ konsistent. Angenommen, + $\sum\not=\Delta$. - $\Rightarrow$ es gibt $n\in N$ mit + $\varphi_n\in\sum\backslash\Delta$ - + $\Rightarrow \Gamma_n\cup\{\varphi_n\}\subseteq\Delta\cup\sum= \sum$ + konsistent. - $\Rightarrow \varphi_n \in\Gamma_{n+1}\subseteq \Delta$, + ein Widerspruch, d.h. $\Delta$ ist max. konsistent. + + \begin{quote} + Lemma 1 + + Sei $\Delta$ maximal konsistent und gelte $\Delta\vdash\varphi$. Dann + gilt $\varphi\in\Delta$. + \end{quote} + + Beweis: 1. Zunächst zeigen wir indirekt, dass $\Delta\cup\{\varphi\}$ + konsistent ist: - Angenommen, $\Delta\cup\{\varphi\}\vdash\bot$. - + $\Rightarrow$ $\exists$ Deduktion $D$ mit Hypothesen in + $\Delta\cup\{\varphi\}$ und Konklusion $\bot$. - + $\Delta\vdash \varphi \Rightarrow \exists$ Deduktion $E$ mit Hypothesen + in $\Delta$ und Konklusion $\varphi$. - $\Rightarrow$ Wir erhalten die + folgende Deduktion: $\frac{\Delta \frac{\Delta}{\varphi}}{\bot}$ + + \begin{verbatim} +Also $\Delta\vdash\bot$, ein Widerspruch zur Konsistenz von $\Delta$. Also ist $\Delta\cup\{\varphi\}$ konsistent. +\end{verbatim} + + \begin{enumerate} + \setcounter{enumi}{1} + \itemsep1pt\parskip0pt\parsep0pt + \item + Da $\Delta\cup\{\varphi\}\supseteq\Delta$ konsistent und $\Delta$ + maximal konsistent ist, folgt $\Delta=\Delta\cup\{\varphi\}$, d.h. + $\varphi\in\Delta$. + \end{enumerate} + + \begin{quote} + Lemma 2 + + Sei $\Delta$ maximal konsistent und $\varphi$ Formel. Dann gilt + $\varphi\not\in\Delta\Leftrightarrow\lnot\varphi\in\Delta$. + \end{quote} + + Beweis: - Zunächst gelte $\lnot\varphi\in\Delta$. Angenommen, + $\varphi\in\Delta$. Dann haben wir die Deduktion + $\frac{\lnot\varphi\quad\varphi}{\bot}$ und damit $\Delta\vdash\bot$, + was der Konsistenz von $\Delta$ widerspricht. - Gelte nun + $\varphi\not\in\Delta$. - $\Rightarrow$ + $\Delta(\Delta\cup\{\varphi\}\Rightarrow\Delta\cup\{\varphi\}$ + inkonsistent (da $\Delta$ max. konsistent) - $\Rightarrow$ Es gibt + Deduktion $D$ mit Hypothesen in $\Delta\cup\{\varphi\}$ \&Konklusion + $\bot$. - $\Rightarrow$ Wir erhalten die folgende Deduktion: + $\frac{\bot}{\lnot\varphi}$ - $\Rightarrow$ + $\Delta\vdash\lnot\varphi\Rightarrow\lnot\varphi\in\Delta$ (nach Lemma + 1) + + \subsection{Erfüllbare Mengen}\label{erfuxfcllbare-mengen} + + \begin{quote} + Definition + + Sei $\Gamma$ eine Menge von Formeln. $\Gamma$ heißt erfüllbar, wenn es + eine passende B-Belegung $B$ gibt mit $B(\gamma) = 1_B$ für alle + $\gamma\in\Gamma$. + \end{quote} + + Bemerkung - Die Erfüllbarkeit einer endlichen Menge $\Gamma$ ist + entscheidbar: - Berechne Menge $V$ von in $\Gamma$ vorkommenden atomaren + Formeln - Probiere alle B-Belegungen $B:V\rightarrow B$ durch - Die + Erfüllbarkeit einer endlichen Menge $\Gamma$ ist NP-vollständig (Satz + von Cook) + + \begin{quote} + Satz Sei $\Delta$ eine maximal konsistente Menge von Formeln. Dann ist + $\Delta$ erfüllbar. + \end{quote} + + Beweis: Definiere eine B-Belegung $B$ mittels + $B(p_i) = \begin{cases} 1_B \quad\text{ falls } p_i\in\Delta \\ 0_B \quad\text{ sonst. } \end{cases}$ + Wir zeigen für alle Formeln + $\varphi: B(\varphi) = 1_B \Leftarrow\Rightarrow\varphi\in\Delta$ (*) + + Der Beweis erfolgt per Induktion über die Länge von $\varphi$. + + \begin{enumerate} + \itemsep1pt\parskip0pt\parsep0pt + \item + I.A.: hat $\varphi$ die Länge 1, so ist $\varphi$ atomare Formel. Hier + gilt (*) nach Konstruktion von $B$. + \item + I.V.: Gelte (*) für alle Formeln der Länge $1$. $\Rightarrow$ Es gibt + Formeln $\alpha$ und $\beta$ der Länge$ 0$ und $ar(a) =ar(b) = 0$ - typische + Relationsnamen: $R,S,...$ + + \begin{quote} + Definition + + Die Menge der Variablen ist $Var=\{x_0,x_1 ,...\}$. + \end{quote} + + \begin{quote} + Definition + + Sei $\sum$ eine Signatur. Die Menge $T_{\sum}$ der $\sum$-Terme ist + induktiv definiert: 1. Jede Variable ist ein Term, d.h. + $Var\subseteq T_{\sum}$ 2. ist $f\in\Omega$ mit $ar(f)=k$ und sind + $t_1,...,t_k\in T_{\sum}$, so gilt $f(t_1,...,t_k)\in T_{\sum}$ 3. + Nichts ist $\sum$-Term, was sich nicht mittels der obigen Regeln + erzeugen läßt. + \end{quote} + + Beispiel:In der Signatur der Datenbank von vorhin haben wir u.a. die + folgenden Terme: - $x_1$ und $x_8$ - $f(x_0)$ und $f(f(x_3))$ - $dk()$ + und $f(dk())$ - hierfür schreiben wir kürzer $dk$ bzw. $f(dk)$ + + \begin{quote} + Definition + + Sei $\sum$ Signatur. Die atomaren $\sum$-Formeln sind die Zeichenketten + der Form - $R(t_1,t_2,...,t_k)$ falls $t_1,t_2,...,t_k\in T_{\sum}$ und + $R\in Rel$ mit $ar(R)=k$ oder - $t_1=t_2$ falls $t_1,t_2\in T_{\sum}$ + oder - $\bot$. + \end{quote} + + Beispiel: In der Signatur der Datenbank von vorhin haben wir u.a. die + folgenden atomaren Formeln: - $S(x_1)$ und $LuLP(f(x4))$ - $S(dk)$ und + $AuD(f(dk))$ + + \begin{quote} + Definition + + Sei $\sum$ Signatur. $\sum$-Formeln werden durch folgenden induktiven + Prozeß definiert: 1. Alle atomaren $\sum$-Formeln sind $\sum$-Formeln. + 2. Falls $\varphi$ und $\Psi$ $\sum$-Formeln sind, sind auch + $(\varphi\wedge\Psi)$,$(\varphi\vee\Psi)$ und $(\varphi\rightarrow\Psi)$ + $\sum$-Formeln. 3. Falls $\varphi$ eine $\sum$-Formel ist, ist auch + $\lnot\varphi$ eine $\sum$-Formel. 4. Falls $\varphi$ eine $\sum$-Formel + und $x\in Var$, so sind auch $\forall x\varphi$ und $\exists x\varphi$ + $\sum$-Formeln. 5. Nichts ist $\sum$-Formel, was sich nicht mittels der + obigen Regeln erzeugen läßt. + \end{quote} + + Ist die Signatur $\sum$ aus dem Kontext klar, so sprechen wir einfach + von Termen, atomaren Formeln bzw.Formeln. + + Beispiel:In der Signatur der Datenbank von vorhin haben wir u.a. die + folgenden Formeln: - $\forall x_0 (S(x_0)\vee WM(x_0)\vee Pr(x_0))$ - + $Pr(dk)$ - $\forall x_3 (S(x_3)\rightarrow\lnot Pr(x_3))$ - + $\forall x_0 \forall x_2 ((S(x_0)\wedge Pr(x_2))\rightarrow J(x_0,x_2))$ + - $\exists x_1 (LuLP(x_1)\wedge AuD(x_1))$ - + $\exists x_2 ((\lnot LuLP(x_2)\vee\lnot AuD(x_2))\wedge\lnot WM(x_2))$ - + $\forall x_1 (S(x_1)\rightarrow J(x_1,f(x_1)))$ + + Wir verwenden die aus der Aussagenlogik bekannten Abkürzungen, z.B. + steht $\varphi\leftrightarrow\Psi$ für + $(\varphi\rightarrow\Psi)\wedge(\Psi\rightarrow\varphi)$. + + Zur verbesserten Lesbarkeit fügen wir mitunter hinter quantifizierten + Variablen einen Doppelpunkt ein, z.B. steht $\exists x\forall y:\varphi$ + für $\exists x\forall y\varphi$ + + Ebenso verwenden wir Variablennamen $x$,$y$,$z$ u.ä. + + Präzedenzen: $\lnot,\forall x,\exists x$ binden am stärksten + + Beispiel: + $(\lnot\forall x:R(x,y)\wedge\exists z:R(x,z))\rightarrow P(x,y,z)$ + steht für + $((\lnot(\forall x:R(x,y))\wedge\exists z:R(x,z))\rightarrow P(x,y,z))$ + + \subsection{Aufgabe}\label{aufgabe} + + Im folgenden seien - $P$ ein-stelliges, $Q$ und $R$ zwei-stellige + Relationssymbole, - $a$ null-stelliges und $f$ ein-stelliges + Funktionssymbol und - $x,y$ und $z$ Variable. + + Welche der folgenden Zeichenketten sind Formeln? \textbar{} \textbar{} + \textbar{} \textbar{} --------------------------------------------- + \textbar{} ---- \textbar{} \textbar{} $\forall x P(a)$ \textbar{} ja + \textbar{} \textbar{} $\forall x\exists y(Q(x,y)\vee R(x))$ \textbar{} + nein \textbar{} \textbar{} $\forall x Q(x,x)\rightarrow\exists x Q(x,y)$ + \textbar{} ja \textbar{} \textbar{} $\forall x P(f(x))\vee\forall$ x + Q(x,x)\$ \textbar{} ja \textbar{} \textbar{} + $\forall x(P(y)\wedge\forall y P(x))$ \textbar{} ja \textbar{} + \textbar{} $P(x) \rightarrow\exists x Q(x,P(x))$ \textbar{} nein + \textbar{} \textbar{} $\forall f\exists x P(f(x))$ \textbar{} nein + \textbar{} + + \begin{quote} + Definition + + Sei $\sum$ eine Signatur. Die Menge $FV(\varphi)$ der freien Variablen + einer $\sum$-Formel $\varphi$ ist induktiv definiert: - Ist $\varphi$ + atomare $\sum$-Formel, so ist $FV(\varphi)$ die Menge der in $\varphi$ + vorkommenden Variablen. - + $FV(\varphi\Box\Psi) =FV(\varphi)\cup FV(\Psi)$ für + $\Box\in\{\wedge,\vee,\rightarrow\}$ - $FV(\lnot\varphi) =FV(\varphi)$ - + $FV(\exists x\varphi) =FV(\forall x\varphi) =FV(\varphi)\backslash\{x\}$. + Eine $\sum$-Formel $\varphi$ ist geschlossen oder ein $\sum$-Satz, wenn + $FV(\varphi)=\varnothing$ gilt. + \end{quote} + + Was sind die freien Variablen der folgenden Formeln? Welche Formeln sind + Sätze? \textbar{} \textbar{} freie Variablen? \textbar{} Satz? + \textbar{} \textbar{} + ----------------------------------------------------------------------- + \textbar{} ---------------- \textbar{} ----- \textbar{} \textbar{} + $\forall x P(a)$ \textbar{} nein \textbar{} ja \textbar{} \textbar{} + $\forall x Q(x,x)\rightarrow\exists x Q(x,y)$ \textbar{} y \textbar{} + nein \textbar{} \textbar{} $\forall x P(x)\vee\forall x Q(x,x)$ + \textbar{} nein \textbar{} ja \textbar{} \textbar{} + $\forall x(P(y)\wedge\forall y P(x))$ \textbar{} y \textbar{} nein + \textbar{} \textbar{} $\forall x(\lnot\forall y Q(x,y)\wedge R(x,y))$ + \textbar{} y \textbar{} nein \textbar{} \textbar{} + $\exists z(Q(z,x)\vee R(y,z))\rightarrow\exists y(R(x,y)\wedge Q(x,z))$ + \textbar{} x,y,z \textbar{} nein \textbar{} \textbar{} + $\exists x(\lnot P(x)\vee P(f(a)))$ \textbar{} nein \textbar{} ja + \textbar{} \textbar{} $P(x)\rightarrow\exists x P(x)$ \textbar{} x + \textbar{} nein \textbar{} \textbar{} + $\exists x\forall y((P(y)\rightarrow Q(x,y))\vee\lnot P(x))$ \textbar{} + x \textbar{} nein \textbar{} \textbar{} $\exists x\forall x Q(x,x)$ + \textbar{} nein \textbar{} ja \textbar{} + + Semantik der Prädikatenlogik - Erinnerung: Die Frage ``Ist die + aussagenlogische Formel $\varphi$ wahr oder falsch?'' war sinnlos, denn + wir wissen i.a. nicht, ob die atomaren Aussagen wahr oder falsch sind. - + Analog: Die Frage ``Ist die prädikatenlogische Formel $\varphi$ wahr + oder falsch?'' ist sinnlos, denn wir wissen bisher nicht, über welche + Objekte, über welche ``Struktur'' $\varphi$ spricht. + + \begin{quote} + Definition + + Sei $\sum$ eine Signatur. Eine $\sum$-Struktur ist ein Tupel + $A=(U_A,(f^A)_{f\in\Omega},(R^A)_{R\in Rel})$, wobei - $U_A$ eine + nichtleere Menge, das Universum, - $R^A\supseteq U_A^{ar(R)}$ eine + Relation der Stelligkeit $ar(R)$ für $R\in Rel$ und - + $f^A:U_A^{ar(f)}\rightarrow U_A$ eine Funktion der Stelligkeit $ar(f)$ + für $f\in\Omega$ ist. + \end{quote} + + Bemerkung: $U_A^0=\{()\}$. - Also ist $a^A:U_A^0\rightarrow U_A$ für + $a\in\Omega$ mit $ar(a)=0$ vollständig gegeben durch $a^A(())\in U_A$. + Wir behandeln 0-stellige Funktionen daher als Konstanten. - Weiterhin + gilt $R^A=\varnothing$ oder $R^A=\{()\}$ für $R\in Rel$ mit $ar(R)=0$. + + Beispiel: Graph - Sei $\sum=(\Omega ,Rel,ar)$ mit + $\Omega=\varnothing ,Rel=\{E\}$ und $ar(E)=2$ die Signatur der Graphen. + - Um den Graphen als $\sum$-Struktur $A=(UA,EA)$ zu betrachten, setzen + wir - $UA=\{v_1,v_2,...,v_9\}$ und - + $EA=\{(v_i,v_j)|(v_i,v_j) ist Kante\}$ + + Im folgenden sei $\sum$ eine Signatur, A eine $\sum$-Struktur und + $\rho:Var\rightarrow U_A$ eine Abbildung (eine Variableninterpretation). + Wir definieren eine Abbildung $\rho':T\sum\rightarrow U_A$ induktiv für + $t\in T_{\sum}$: - ist $t\in Var$, so setze $\rho'(t) =\rho(t)$ - + ansonsten existieren $f\in\Omega$ mit $ar(f)=k$ und + $t_1,...,t_k\in T_{\sum}$ mit $t=f(t_1,...,t_k)$. Dann setze + $\rho'(t) =f^A(\rho'(t_1),...,\rho'(t_k))$. Die Abbildung $\rho'$ ist + die übliche ``Auswertungsabbildung''. Zur Vereinfachung schreiben wir + auch $\rho(t)$ an Stelle von $\rho'(t)$. + + Beispiel: - Seien $A=(R,f^A,a^A)$ mit $f^A$ die Subtraktion und $a$ + nullstelliges Funktionssymbol mit $a^A=10$. Seien weiter $x,y\in Var$ + mit $\rho(x)=7$ und $\rho(y)=-2$. Dann gilt + $\rho(f(a,f(x,y))) =\rho(a)-(\rho(x)-\rho(y)) =a^A-(\rho(x)-\rho(y)) = 1$ + - Seien $A= (Z,f^A,a^A)$ mit $f^A$ die Maximumbildung, $a$ nullstelliges + Funktionssymbol mit $a^A=10$. Seien weiter $x,y\in Var$ mit $\rho(x)=7$ + und $\rho(y)=-2$. In diesem Fall gilt + $\rho(f(a,f(x,y))) = max(\rho(a),max(\rho(x),\rho(y)) = max(a^A,max(\rho(x),\rho(y))) = 10$ + + Bemerkung: Wir müssten also eigentlich noch vermerken, in welcher + Struktur $\rho(t)$ gebildet wird - dies wird aber aus dem Kontext immer + klar sein. + + Für eine $\sum$-Formel $\varphi$ definieren wir die Gültigkeit in einer + $\sum$-Struktur $A$ unter der Variableninterpretation $\rho$ (in + Zeichen: $A\Vdash_\rho\varphi$) induktiv: - $A\Vdash_\rho\bot$ gilt + nicht. - $A\Vdash_\rho R(t_1,...,t_k)$ falls + $(\rho(t_1),...,\rho(t_k))\in R^A$ für $R\in Rel$ mit $ar(R)=k$ und + $t_1,...,t_k\in T_{\sum}$. - $A\Vdash_\rho t_1 =t_2$ falls + $\rho(t_1) =\rho(t_2)$ für $t_1,t_2\in T_{\sum}$. + + Für $\sum$-Formeln $\varphi$ und $\Psi$ und $x\in Var$: - + $A\Vdash_p \varphi\wedge\Psi$ falls $A\Vdash_p\varphi$ und + $A\Vdash_p \Psi$. - $A\Vdash_p \varphi\vee\Psi$ falls $A\Vdash_p\varphi$ + oder $A\Vdash_p\Psi$ . - $A\Vdash_p \varphi\rightarrow\Psi$ falls nicht + $A\Vdash_p\varphi$ oder $A\Vdash_p\Psi$ . - $A\Vdash_p \lnot\varphi$ + falls $A\Vdash_p \varphi$ nicht gilt. - $A\Vdash_p \exists x\varphi$ + falls ??? - $A\Vdash_p \forall x\varphi$ falls ??? + + Für $x\in Var$ und $a\in U_A$ sei + $\rho[x\rightarrow a]:Var\rightarrow U_A$ die Variableninterpretation, + für die gilt + $(\rho[x\rightarrow a])(y) = \begin{cases} \rho(y) \quad\text{ falls } x\not=y \\ a \quad\text{ sonst } \end{cases}$ + - $A\Vdash_p \exists x\varphi$ falls es $a\in U_A$ gibt mit + $A\Vdash_{p[x\rightarrow a]}\varphi$. - $A\Vdash_p \forall x\varphi$ + falls $A\Vdash_{p[x\rightarrow a]}\varphi$ für alle $a\in U_A$. + + \begin{quote} + Definition + + Sei $\sum$ eine Signatur, $\varphi$ eine $\sum$-Formel, $\Delta$ eine + Menge von $\sum$-Formeln und $A$ eine $\sum$-Struktur. - + $A\Vdash\varphi$ ($A$ ist Modell von $\varphi$) falls $A\Vdash_p\varphi$ + für alle Variableninterpretationen $\rho$ gilt. - $A\Vdash\Delta$ falls + $A\Vdash\Psi$ für alle $\Psi\in\Delta$. + \end{quote} + + Aufgaben - Sei $A$ die Struktur, die dem vorherigen Graphen entspricht - + Welche der folgenden Formeln $\varphi$ gelten in $A$, d.h. für welche + Formeln gilt $A\Vdash_p\varphi$ für alle Variableninterpretationen + $\rho$? 1. $\exists x\exists y:E(x,y)$ 2. $\forall x\exists y:E(x,y)$ 3. + $\exists x\forall y:(x\not=y\rightarrow E(x,y))$ 4. + $\forall x\forall y:(x\not=y\rightarrow E(x,y))$ 5. + $\exists x\exists y\exists z:(E(x,y)\wedge E(y,z)\wedge E(z,x))$ - In + der Prädikatenlogik ist es also möglich, die Eigenschaften vom Anfang + des Kapitels auszudrücken, ohne den Graphen direkt in die Formel zu + kodieren. + + \begin{quote} + Definition + + Sei $\sum$ eine Signatur, $\varphi$ eine $\sum$-Formel, $\Delta$ eine + Menge von $\sum$-Formeln und $A$ eine $\sum$-Struktur. - $\Delta$ ist + erfüllbar, wenn es $\sum$-Struktur $B$ und Variableninterpretation + $\rho:Var\rightarrow U_B$ gibt mit $B\Vdash_\rho\Psi$ für alle + $\Psi\in\Delta$. - $\varphi$ ist semantische Folgerung von + $\Delta(\Delta\Vdash\varphi)$ falls für alle $\sum$-Strukturen $B$ und + alle Variableninterpretationen $\rho:Var\rightarrow U_B$ gilt: Gilt + $B\Vdash_\rho\Psi$ für alle $\Psi\in\Delta$, so gilt auch + $B\Vdash_\rho \varphi$. - $\varphi$ ist allgemeingültig, falls + $B\Vdash \rho\varphi$ für alle $\sum$-Strukturen $B$ und alle + Variableninterpretationen $\rho$ gilt. + \end{quote} + + Bemerkung: $\varphi$ allgemeingültig gdw. $\varnothing\Vdash\varphi$ + gdw. $\{\lnot\varphi\}$ nicht erfüllbar. Hierfür schreiben wir auch + $\Vdash\varphi$. + + Beispiel: Der Satz + $\varphi=(\forall x:R(x)\rightarrow\forall x:R(f(x)))$ ist + allgemeingültig. + + Beweis: Sei $\sum$ Signatur, so dass $\varphi$ $\sum$-Satz ist. Sei $A$ + $\sum$-Struktur und $\rho$ Variableninterpretation. Wir betrachten zwei + Fälle: 1. Falls $A\not\Vdash_\rho\forall x R(x)$, so gilt + $A\Vdash_p\varphi$. 2. Wir nehmen nun $A\Vdash_p\forall x R(x)$ an. Sei + $a\in U_A$ beliebig und $b=f^A(a)$. + $A\Vdash_p\forall x R(x) \Rightarrow A\Vdash_{p[x\rightarrow b]} R(x) \Rightarrow RA\owns (p[x\rightarrow b])(x) = b = f^A(a) = (\rho[x\rightarrow a])(f(x)) \Rightarrow A\Vdash_{p[x\rightarrow a]}R(f(x))$. + Da $a\in U_A$ beliebig war, haben wir also $A\Vdash_p\forall x:R(f(x))$. + Also gilt auch in diesem Fall $A\Vdash_p\varphi$. Da $A$ und $\rho$ + beliebig waren, ist $\varphi$ somit allgemeingültig. + + Beispiel: - Der Satz $\varphi =\exists x(R(x)\rightarrow R(f(x)))$ ist + allgemeingültig. - Beweis: Sei $\sum$ Signatur, so dass $\varphi$ + $\sum$-Satz ist. Sei $A$ $\sum$-Struktur und $\rho$ + Variableninterpretation. Wir betrachten wieder zwei Fälle: 1. + Angenommen, $R^A=U_A$. Sei $a\in U_A$ beliebig. - + $\Rightarrow f^A(a)\in R^A$ - + $\Rightarrow A\Vdash_{p[x\rightarrow a]} R(f(x))$ - + $\Rightarrow A\Vdash_{p[x\rightarrow a]} R(x)\rightarrow R(f(x))$ - + $\Rightarrow A\Vdash_p\varphi$. 2. Ansonsten existiert + $a\in U_A\backslash R^A$. - + $\Rightarrow A\not\Vdash_{p[x\rightarrow a]} R(x)$ - + $\Rightarrow A\Vdash_{p[x\rightarrow a]} R(x)\rightarrow R(f(x))$ - + $\Rightarrow A\Vdash_p \varphi$. Da $A$ und $\rho$ beliebig waren, ist + $\varphi$ somit allgemeingültig. + + Aufgabe \textbar{} \textbar{} allgemeingültig \textbar{} erfüllbar + \textbar{} unerfüllbar \textbar{} \textbar{} + -------------------------------------------------------------------- + \textbar{} --------------- \textbar{} --------- \textbar{} ----------- + \textbar{} \textbar{} $P(a)$ \textbar{} nein \textbar{} ja \textbar{} + nein \textbar{} \textbar{} $\exists x:(\lnot P(x)\vee P(a))$ \textbar{} + ja \textbar{} ja \textbar{} nein \textbar{} \textbar{} + $P(a)\rightarrow\exists x:P(x)$ \textbar{} ja \textbar{} ja \textbar{} + nein \textbar{} \textbar{} $P(x)\rightarrow\exists x:P(x)$ \textbar{} ja + \textbar{} ja \textbar{} nein \textbar{} \textbar{} + $\forall x:P(x)\rightarrow\exists x:P(x)$ \textbar{} ja \textbar{} ja + \textbar{} nein \textbar{} \textbar{} + $\forall x:P(x)\wedge\lnot\forall y:P(y)$ \textbar{} nein \textbar{} + nein \textbar{} ja \textbar{} \textbar{} + $\forall x:(P(x,x)\rightarrow\exists x\forall y:P(x,y))$ \textbar{} nein + \textbar{} ja \textbar{} nein \textbar{} \textbar{} + $\forall x\forall y:(x=y\rightarrow f(x) =f(y))$ \textbar{} ja + \textbar{} ja \textbar{} nein \textbar{} \textbar{} + $\forall x\forall y:(f(x) =f(y)\rightarrow x=y)$ \textbar{} nein + \textbar{} ja \textbar{} nein \textbar{} \textbar{} + $\exists x\exists y\exists z:(f(x) =y\wedge f(x) =z\wedge y \not=z)$ + \textbar{} nein \textbar{} nein \textbar{} ja \textbar{} \textbar{} + $\exists x\forall x:Q(x,x)$ \textbar{} nein \textbar{} ja \textbar{} + nein \textbar{} + + \subsection{Substitutionen}\label{substitutionen} + + \begin{quote} + Definition + + Eine Substitution besteht aus einer Variable $x\in Var$ und einem Term + $t\in T_{\sum}$, geschrieben $[x:=t]$. + \end{quote} + + Die Formel $\varphi[x:=t]$ ist die Anwendung der Substitution $[x:=t]$ + auf die Formel $\varphi$. Sie entsteht aus $\varphi$, indem alle freien + Vorkommen von $x$ durch $t$ ersetzt werden. Sie soll das über $t$ + aussagen, was $\varphi$ über $x$ ausgesagt hat. Dazu definieren wir + zunächst induktiv, was es heißt, die freien Vorkommen von $x$ im Term + $s\in T_{\sum}$ zu ersetzen: - $x[x:=t] =t$ - $y[x:=t] =y$ für + $y\in Var\backslash\{x\}$ - + $(f(t_1 ,...,t_k))[x:=t] =f(t_1 [x:=t],...t_k[x:=t])$ für $f\in\Omega$ + mit $ar(f) =k$ und $t_1,...,t_k\in T_{\sum}$ + + \begin{quote} + Lemma + + Seien $\sum$ Signatur, $A$ $\sum$-Struktur, $\rho:Var\rightarrow U_A$ + Variableninterpretation, $x\in Var$ und $s,t\in T_{\sum}$. Dann gilt + $\rho(s[x:=t])=\rho[x\rightarrow \rho(t)](s)$. + \end{quote} + + Beweis: Induktion über den Aufbau des Terms $s$ (mit + $\rho'=\rho[x\rightarrow \rho(t)]$ ): - + $s=x:\rho(s[x:=t])=\rho(t) =\rho'(x) =\rho'(s)$ - + $s\in Var\backslash\{x\}:\rho(s[x:=t])=\rho(s) =\rho'(s)$ - + $s=f(t_1 ,...,t_k):\rho((f(t_1 ,...,t_k))[x:=t])= \rho(f(t_1[x:=t],...,t_k[x:=t]))= f^A(\rho(t_1[x:=t]),...,\rho(t_k[x:=t])) = f^A(\rho'(t_1),...,\rho'(t_k))= \rho'(f(t_1 ,...,t_k))=\rho'(s)$ + + Die Definition von $s[x:=t]$ kann induktiv auf $\sum$-Formeln + fortgesetzt werden: - $(t_1 =t_2 )[x:=t] = (t_1 [x:=t] =t_2 [x:=t])$ für + $t_1 ,t_2 \in T_{\sum}$ - + $(R(t_1 ,...,t_k))[x:=t] =R(t_1 [x:=t],...,t_k[x:=t])$ für $R\in Rel$ + mit $ar(R) =k$ und $t_1 ,...,t_k\in T_{\sum}$ - $\bot[x:=t] =\bot$ + + Für $\sum$ -Formeln $\varphi$ und $\Psi$ und $y\in Var$: - + $(\varphi\Box\Psi)[x:=t]=\varphi [x:=t]\Box\Psi[x:=t]$ für + $\Box\in\{\wedge,\vee,\rightarrow\}$ - + $(\lnot\varphi)[x:=t] = \lnot(\varphi[x:=t])$ - + $(Qy\varphi)[x:=t] = \begin{cases} Qy\varphi[x:=t] \quad\text{ falls } x\not=y \\ Qy\varphi \quad\text{ falls } x=y \end{cases} \text{ für } Q\in\{\exists,\forall\}$. + + Beispiel: + $(\exists x P(x,f(y))\vee\lnot\forall yQ(y,g(a,h(z))))[y:=f(u)] = (\exists x P(x,f(f(u)))\vee\lnot\forall yQ(y,g(a,h(z))))$ + + $\varphi [x:=t]$ ``soll das über $t$ aussagen, was $\varphi$ über $x$ + ausgesagt hat.'' + + Gegenbeispiel: Aus $\exists y$ $Mutter(x) =y$ mit Substitution + $[x:=Mutter(y)]$ wird $\exists y$ Mutter$(Mutter(y)) =y$. + + \begin{quote} + Definition + + Sei $[x:=t]$ Substitution und $\varphi$ $\sum$-Formel. Die Substitution + $[x:=t]$ heißt für $\varphi$ zulässig, wenn für alle $y\in Var$ gilt: + $y$ Variable in $t\Rightarrow\varphi$ enthält weder $\exists y$ noch + $\forall y$ + \end{quote} + + \begin{quote} + Lemma + + Sei $\sum$ Signatur, A $\sum$-Struktur, $\rho:Var\rightarrow U_A$ + Variableninterpretation, $x\in Var$ und $t\in T_{\sum}$. Ist die + Substitution $[x:=t]$ für die $\sum$-Formel $\varphi$ zulässig, so gilt + $A\Vdash_p\varphi [x:=t]\Leftrightarrow A\Vdash_{p[x\rightarrow \rho(t)]}\varphi$. + \end{quote} + + Beweis: Induktion über den Aufbau der Formel $\varphi$ (mit + $\rho'=\rho[x\rightarrow \rho(t)])$: - $\varphi = (s_1 =s_2)$: - + $A\Vdash_p(s_1 =s_2)[x:=t] \Leftrightarrow A\Vdash_p s_1[x:=t] =s_2[x:=t]$ + - + $\Leftrightarrow \rho(s_1[x:=t]) =\rho(s_2[x:=t])\Leftrightarrow \rho'(s_1) =\rho'(s_2)$ + - $\Leftrightarrow A\Vdash_{p'} s_1 =s_2$ - andere atomare Formeln + analog - $\varphi =\varphi_1\wedge\varphi_2$: - + $A\Vdash_p(\varphi_1\wedge\varphi_2)[x:=t] \Leftrightarrow A\Vdash_p\varphi_1 [x:=t]\wedge\varphi_2[x:=t]$ + - $\Leftrightarrow A\Vdash_p\varphi_1[x:=t]$ und + $A\Vdash_p\varphi_2[x:=t]$ - $\Leftrightarrow A\Vdash_{p'}\varphi_1$ und + $A\Vdash_{p'}\varphi_2$ - + $\Leftrightarrow A\Vdash_{p'}\varphi_1\wedge\varphi_2$ - + $\varphi=\varphi_1\vee\varphi_2,\varphi =\varphi_1\rightarrow\varphi_2$ + und $\varphi=\lnot\psi$ analog - $\varphi=\forall y\psi$: - Wir + betrachten zunächst den Fall $x=y$: - + $A\Vdash_p(\forall x\psi)[x:=t]\Leftrightarrow A\Vdash_p\forall x\psi \Leftrightarrow A\Vdash_{p'}\forall x\psi$ + (denn $x\not\in FV(\forall x\psi)$ ) - Jetzt der Fall $x\not=y$: - Für + $a\in U_A$ setze $\rho_a=\rho[y\rightarrow a]$. Da $[x:=t]$ für + $\varphi$ zulässig ist, kommt $y$ in $t$ nicht vor. Zunächst erhalten + wir - $\rho_a[x\rightarrow \rho_a(t)] = \rho_a[x\rightarrow \rho(t)]$ da + $y$ nicht in $t$ vorkommt - + $=\rho[y\rightarrow a][x\rightarrow \rho(t)] = \rho[x\rightarrow \rho(t)][y\rightarrow a]$ + da $x\not=y$ - Es ergibt sich + $A\Vdash_p(\forall y\psi)[x:=t]\Leftrightarrow A\Vdash_p\forall y(\psi[x:=t])$ + (wegen $x\not=y$) - $\Leftrightarrow A\Vdash_{pa}\psi[x:=t]$ für alle + $a\in U_A$ - $\Leftrightarrow A\Vdash_{pa[x\rightarrow \rho_a(t)]}\psi$ + für alle $a\in U_A$ - + $\Leftrightarrow A\Vdash_{p[x\rightarrow \rho(t)][y\rightarrow a]}\psi$ + für alle $a\in U_A$ - + $\Leftrightarrow A\Vdash_{p[x\rightarrow \rho(t)]}\forall y\psi$ - + $\varphi=\exists y\psi$ : analog + + \subsection{Natürliches Schließen}\label{natuxfcrliches-schlieuxdfen-1} + + Wir haben Regeln des natürlichen Schließens für aussagenlogische Formeln + untersucht und für gut befunden. Man kann sie natürlich auch für + prädikatenlogische Formeln anwenden. + + Beispiel: Für alle $\sum$-Formel $\varphi$ und $\psi$ gibt es eine + Deduktion mit Hypothesen in $\{\lnot\varphi\wedge\lnot\psi\}$ und + Konklusion $\lnot(\varphi\vee\psi)$: + \includegraphics[width=\linewidth]{Assets/Logik-deduktion-konklusion.png} + + \subsection{Korrektheit}\label{korrektheit-1} + + Können wir durch mathematische Beweise zu falschen Aussagen kommen? + Können wir durch das natürliche Schließen zu falschen Aussagen kommen? + Existiert eine Menge $\Gamma$ von $\sum$-Formeln und eine $\sum$-Formel + $\varphi$ mit $\Gamma\vdash\varphi$ und $\Gamma\not\Vdash\varphi$? + + Frage: Gilt $\Gamma\vdash\varphi\Rightarrow \Gamma\Vdash\varphi$ bzw. + $\varphi$ ist Theorem $\Rightarrow\varphi$ ist allgemeingültig? + + Der Beweis des Korrektheitslemmas für das natürliche Schließen kann ohne + große Schwierigkeiten erweitert werden. Man erhält + + \begin{quote} + Lemma V0 + + Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und + $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit + Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des + natürlichen Schließens der Aussagenlogik verwendet. Dann gilt + $\Gamma\Vdash\varphi$. + \end{quote} + + Umgekehrt ist nicht zu erwarten, dass aus $\Gamma\Vdash\varphi$ folgt, + dass es eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion + $\varphi$ gibt, denn die bisher untersuchten Regeln erlauben keine + Behandlung von $=,\forall$ bzw. $\exists$. Solche Regeln werden wir + jetzt einführen. + + Zunächst kümmern wir uns um Atomformeln der Form $t_1 =t_2$. Hierfür + gibt es die zwei Regeln $(R)$ und $(GfG)$: + + \begin{quote} + Reflexivität (ausführlich) + + Für jeden Termt ist $\frac{}{t=t}$ eine hypothesenlose Deduktion mit + Konklusion $t=t$. \includegraphics[width=\linewidth]{Assets/Logik-reflexivität-kurz.png} + \end{quote} + + \begin{quote} + Gleiches-für-Gleiches in mathematischen Beweisen + + ,,Zunächst zeige ich, dass $s$ die Eigenschaft $\varphi$ hat:\ldots{} + Jetzt zeige ich $s=t$:\ldots{} Also haben wir gezeigt, dass $t$ die + Eigenschaft $\varphi$ hat. qed'' + + Gleiches-für-Gleiches (ausführlich) Seien $s$ und $t$ Terme und + $\varphi$ Formel, so dass die Substitutionen $[x:=s]$ und $[x:=t]$ für + $\varphi$ zulässig sind. Sind $D$ und $E$ Deduktionen mit Hypothesen in + $\Gamma$ und Konklusionen $\varphi[x:=s]$ bzw. $s=t$, so ist das + folgende eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion + $\varphi[x:=t]$: + \includegraphics[width=\linewidth]{Assets/Logik-gleiches-für-gleiches-ausführlich.png} + + Gleiches-für-Gleiches (Kurzform) + \includegraphics[width=\linewidth]{Assets/Logik-gleiches-für-gleiches-kurz.png} Bedingung: + über keine Variable aus $s$ oder $t$ wird in $\varphi$ quantifiziert + \end{quote} + + Die folgenden Beispiele zeigen, dass wir bereits jetzt die üblichen + Eigenschaften der Gleichheit (Symmetrie, Transitivität, Einsetzen) + folgern können. + + Beispiel: Seien $x$ Variable, $s$ Term ohne $x$ und $\varphi=(x=s)$. - + Da $\varphi$ quantorenfrei ist, sind die Substitutionen $[x:=s]$ und + $[x:=t]$ für $\varphi$ zulässig. - Außerdem gelten + $\varphi[x:=s] = (s=s)$ und $\varphi[x:=t] = (t=s)$. - Also ist das + folgende eine Deduktion: + \includegraphics[width=\linewidth]{Assets/Logik-deduktion-beispiel.png} - Für alle + Termesundthaben wir also $\{s=t\}\vdash t=s$. + + Beispiel: Seien $x$ Variable, $r,s$ und $t$ Terme ohne $x$ und + $\varphi=(r=x)$. - Da $\varphi$ quantorenfrei ist, sind die + Substitutionen $[x:=s]$ und $[x:=t]$ für $\varphi$ zulässig. - Außerdem + gelten $\varphi[x:=s]=(r=s)$ und $\varphi[x:=t]=(r=t)$. - Also ist das + folgende eine Deduktion: + \includegraphics[width=\linewidth]{Assets/Logik-deduktion-beispiel-2.png} - Für alle Terme + $r,s$ und $t$ haben wir also $\{r=s,s=t\}\vdash r=t$. + + Beispiel: Seien $x$ Variable, $s$ und $t$ Terme ohne $x$,$f$ + einstelliges Funktionssymbol und $\varphi=(f(s)=f(x))$. - Da $\varphi$ + quatorenfrei ist, sind die Substitutionen $[x:=s]$ und $[x:=t]$ für + $\varphi$ zulässig. - Außerdem gelten $\varphi[x:=s]=(f(s)=f(s))$ und + $\varphi[x:=t]=(f(s)=f(t))$. - Also ist das folgende eine Deduktion: + \includegraphics[width=\linewidth]{Assets/Logik-deduktion-beispiel-3.png} + + \begin{quote} + Lemma V1 + + Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und + $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit + Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des + natürlichen Schließens der Aussagenlogik, $(R)$ und $(GfG)$ verwendet. + Dann gilt $\Gamma\Vdash\varphi$. + \end{quote} + + Beweis: Wir erweitern den Beweis des Korrektheitslemmas bzw. des Lemmas + V0, der Induktion über die Größe der Deduktion $D$ verwendete. - Wir + betrachten nur den Fall, dass $D$ die folgende Form hat: + \includegraphics[width=\linewidth]{Assets/Logik-lemma-v1-beweis.png} - Da dies Deduktion + ist, sind die Substitutionen $[x:=s]$ und $[x:=t]$ für $\varphi$ + zulässig, d.h. in $\varphi$ wird über keine Variable aus $s$ oder $t$ + quantifiziert. - $E$ und $F$ kleinere Deduktionen + $\Rightarrow\Gamma\Vdash\varphi[x:=s]$ und $\Gamma\Vdash s=t$ - Seien A + $\sum$-Struktur und $\rho$ Variableninterpretation mit $A\Vdash_p\gamma$ + für alle $\gamma\in\Gamma$. - $\Rightarrow A\Vdash_p\varphi[x:=s]$ und + $A\Vdash_p s=t$ - $\Rightarrow A\Vdash_{p[x\rightarrow \rho(s)]}\varphi$ + und $\rho(s) =\rho(t)$ - + $\Rightarrow A\Vdash_{p[x\rightarrow \rho(t)]}\varphi$ - + $\Rightarrow A\Vdash_p \varphi[x:=t]$ - Da $A$ und $\rho$ beliebig waren + mit $A\Vdash_p\gamma$ für alle $\gamma\in\Gamma$ haben wir + $\Gamma\Vdash\varphi[x:=t]$ gezeigt. + + \subsubsection{$\forall$ in math. + Beweisen}\label{forall-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``für alle $x$ gilt $\varphi$'' + sieht üblicherweise so aus: ``Sei $x$ beliebig, aber fest. Jetzt zeige + ich $\varphi$ (hier steckt die eigentliche Arbeit). Da $x$ beliebig war, + haben wird''für alle $x$ gilt $\varphi$" gezeigt. qed" + + \begin{quote} + $\forall$ -Einführung + + Sei $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion + $\varphi$ und sei $x$ eine Variable, die in keiner Formel aus $\Gamma$ + frei vorkommt. Dann ist das folgende eine Deduktion mit Hypothesen in + $\Gamma$ und Konklusion + $\forall x\varphi: \frac{\phi}{\forall x\varphi}$ + + Bedingung: $x$ kommt in keiner Hypothese frei vor + \end{quote} + + \begin{quote} + Lemma V2 + + Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und + $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit + Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des + natürlichen Schließens der Aussagenlogik, (R), (GfG) und ($\forall$ -I) + verwendet. Dann gilt $\Gamma\Vdash\varphi$. + \end{quote} + + Beweis: Betrachte die folgende Deduktion $D$ - Insbesondere ist $x$ + keine freie Variable einer Formel aus $\Gamma$ und es gilt nach IV + $\Gamma\Vdash\varphi$ - Sei nun $A$ $\sum$-Struktur und $\rho$ + Variableninterpretation mit $A\Vdash_p y$ für alle $y\in\Gamma$. - Zu + zeigen ist $A\Vdash_p \forall x\varphi$: - Sei also $a\in U_A$ beliebig. + - $\Rightarrow$ für alle $y\in\Gamma$ gilt + $A\Vdash_{p[x\rightarrow a]} y$ da $x\not\in FV(y)$ und $A\Vdash_p y$ - + $\Rightarrow A\Vdash_{\rho[x\rightarrow a]}\varphi$ - Da $a\in U_A$ + beliebig war, haben wir $A\Vdash_\rho\forall x\varphi$ gezeigt - Da $A$ + und $\rho$ beliebig waren mit $A\Vdash_\rho\Gamma$ für alle + $\gamma\in\Gamma$ haben wir also $\Gamma\Vdash\forall x\varphi$ gezeigt. + + \subsubsection{$\forall$ -Elimination in math. + Beweisen}\label{forall--elimination-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``t erfüllt $\varphi$'' kann so + aussehen: ``Zunächst zeige ich $\forall x\varphi$ (hier steckt die + eigentliche Arbeit). Damit erfüllt insbesondere $t$ die Aussage$\varphi$ + , d.h., wir haben''$t$ erfüllt $\varphi$" gezeigt. qed" + + \begin{quote} + $\forall$ -Elimination + + Sei $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion + $\forall x\varphi$ und seit Term, so dass Substitution {[}x:=t{]} für + $\varphi$ zulässig ist. Dann ist das folgende eine Deduktion mit + Hypothesen in $\Gamma$ und Konklusion + $\varphi[x:=t]:\frac{\forall x\varphi}{\varphi[x:=t]}$ + + Bedingung: über keine Variable aus $t$ wird in $\varphi$ quantifiziert + \end{quote} + + \begin{quote} + Lemma V3 + + Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und + $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit + Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des + natürlichen Schließens der Aussagenlogik, (R), (GfG), ($\forall$-I) und + ($\forall$-E) verwendet. \textgreater{} Dann gilt $\Gamma\Vdash\varphi$. + \end{quote} + + Beweis: Analog zum Beweis von Lemma V2. + + \subsubsection{$\exists$ in math. + Beweisen}\label{exists-in-math.-beweisen} + + Ein Beweis von ``$\sigma$ gilt'' kann so aussehen: ``Zunächst zeige ich + $\exists x\varphi$ (hier steckt Arbeit). Jetzt zeige ich, dass $\sigma$ + immer gilt, wenn$\varphi$ gilt (mehr Arbeit). Damit gilt $\sigma$. qed'' + + \begin{quote} + $\exists$ -Elimination + + Sei $\Gamma$ eine Menge von Formeln, die die Variable $x$ nicht frei + enthalten und enthalte die Formel $\sigma$ die Variabel $x$ nicht frei. + Wenn $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion + $\exists x\varphi$ und $E$ eine Deduktion mit Hypothesen in + $\Gamma\cup\{\varphi\}$ und Konklusion $\sigma$ ist, dann ist das + folgende eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion + $\sigma:\frac{\exists x\varphi \quad\quad \sigma}{\sigma}$ + + Bedingung: $x$ kommt in den Hypothesen und in $\sigma$ nicht frei vor + \end{quote} + + \begin{quote} + Lemma V4 Sei $\sigma$ eine Signatur, $\Gamma$ eine Menge von + $\sum$-Formeln und $\varphi$ eine $\sigma$ -Formel. Sei weiter $D$ eine + Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die + Regeln des natürlichen Schließens der Aussagenlogik, (R), (GfG), + ($\forall$-I), ($\forall$-E) und ($\exists$-E) verwendet. Dann gilt + $\Gamma\Vdash\varphi$. + \end{quote} + + Beweis: Sei $D$ die folgende Deduktion - Insbesondere kommt $x$ in den + Formeln aus $\Gamma\cup\{\sigma\}$ nicht frei vor. Außerdem gelten nach + IV $\Gamma\Vdash\exists x\varphi$ und + $\Gamma\cup\{\varphi\}\Vdash\sigma$. - Sei nun $A$ $\sigma$-Struktur und + $\rho$ Variableninterpretation mit $A\Vdash_\rho\Gamma$ für alle + $\gamma\in\Gamma$. - Zu zeigen ist $A\Vdash_\rho\sigma$: - Wegen + $A\Vdash_\rho\exists x\varphi$ existiert $a\in U_A$ mit + $A\Vdash_{\rho[x\rightarrow a]}\varphi$. - $x$ kommt in Formeln aus + $\Gamma$ nicht frei vor + $\Rightarrow A\Vdash_{\rho[x\rightarrow a]}\gamma$ für alle + $\gamma\in\Gamma$. - Aus $\Gamma\cup\{\varphi\}\Vdash\sigma$ folgt + $A\Vdash_{\rho[x\rightarrow a]}\sigma$. - Da $x\not\in FV(\sigma)$ + erhalten wir $A\Vdash_\rho \sigma$. - Da $A$ und $\rho$ beliebig waren + mit $A\Vdash_\rho\gamma$ für alle $\gamma\in\Gamma$ haben wir also + $\Gamma\Vdash\sigma$ gezeigt. + + \subsubsection{$\exists$ -Einführung in math. + Beweisen}\label{exists--einfuxfchrung-in-math.-beweisen} + + Ein mathematischer Beweis einer Aussage ``es gibt ein $x$, das $\varphi$ + erfüllt'' sieht üblicherweise so aus: ``betrachte dieses $t$ (hier ist + Kreativität gefragt). Jetzt zeige ich, daß $t\varphi$ erfüllt (u.U. + harte Arbeit). Also haben wir''es gibt ein $x$, das $\varphi$ erfüllt" + gezeigt. qed" + + \begin{quote} + $\exists$ -Einführung + + Sei die Substitution $[x:=t]$ für die Formel $\varphi$ zulässig. Sei + weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion + $\varphi[x:=t]$. Dann ist das folgende eine Deduktion mit Hypothesen in + $\Gamma$ und Konklusion + $\exists x\varphi:\frac{\varphi[x:=t]}{\exists x\varphi}$ + + Bedingung: über keine Variable in $t$ wird in $\varphi$ quantifiziert + \end{quote} + + \begin{quote} + Korrektheitslemma für das natürliche Schließen in der Prädikatenlogik + + Sei $\sigma$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und + $\varphi$ eine $\sigma$ -Formel. Sei weiter $D$ eine Deduktion mit + Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des + natürlichen Schließens der Aussagenlogik, (R), (GfG), ($\forall$-I), + ($\forall$-E), ($\exists$ -E) und ($\exists$ -I) verwendet. Dann gilt + $\Gamma\Vdash\varphi$. + \end{quote} + + Beweis: analog zu obigen Beweisen. + + \subsubsection{Regeln des natürlichen Schließens + (Erweiterung)}\label{regeln-des-natuxfcrlichen-schlieuxdfens-erweiterung} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + ($R$): $\frac{}{t=t}$ + \item + (GfG): $\frac{\varphi[x:=s] \quad\quad s=t}{\varphi[x:=t]}$ (über + keine Variable aus $s$ oder $t$ wird in $\varphi$ quantifiziert) + \item + ($\forall$-I): $\frac{\varphi}{\forall x\varphi}$ (x nicht frei in + Hypothesen) + \item + ($\forall$-E): $\frac{\forall x\varphi}{\varphi[x:=t]}$ (über keine + Variable aus $t$ wird in $\varphi$ quantifiziert) + \item + ($\exists$-I): $\frac{\varphi [x:=t]}{\exists x\varphi}$ (über keine + Variable aus $t$ wird in $\varphi$ quantifiziert) + \item + ($\exists$-I): $\frac{\exists x\varphi\quad\quad \sigma}{\sigma}$ ($x$ + kommt in Hypothesen und $\sigma$ nicht frei vor) + \end{itemize} + + \begin{quote} + Definition + + Für eine Menge $\Gamma$ von $\sum$-Formeln und eine $\sum$-Formel + $\varphi$ schreiben wir $\Gamma\vdash\varphi$ wenn es eine Deduktion + gibt mit Hypothesen in $\Gamma$ und Konklusion $\varphi$. Wir sagen + ``$\varphi$ ist eine syntaktische Folgerung von $\Gamma$''. Eine Formel + $\varphi$ ist ein Theorem, wenn $\varnothing\vdash\varphi$ gilt. + \end{quote} + + Bemerkung: $\Gamma\vdash\varphi$ sagt (zunächst) nichts über den Inhalt + der Formeln in $\Gamma\cup\{\varphi\}$ aus, sondern nur über den Fakt, + dass $\varphi$ mithilfe des natürlichen Schließens aus den Formeln aus + $\Gamma$ hergeleitet werden kann. Ebenso sagt ``$\varphi$ ist Theorem'' + nur, dass $\varphi$ abgeleitet werden kann, über ``Wahrheit'' sagt + dieser Begriff (zunächst) nichts aus. Wir haben aber ``en passant'' das + folgende gezeigt: + + \begin{quote} + Korrektheitssatz + + Für eine Menge von $\sum$-Formeln $\Gamma$ und eine $\sum$-Formel + $\varphi$ gilt $\Gamma\vdash\varphi \Rightarrow \Gamma\Vdash\varphi$. + \end{quote} + + Beispiel: Seien $\varphi$ Formel und $x$ Variable. Dann gelten + $\{\lnot\exists x\varphi\}\Vdash\forall x\lnot\varphi$ und + $\{\forall x\lnot\varphi\}\Vdash\lnot\exists x\varphi$. - Beweis: + \includegraphics[width=\linewidth]{Assets/Logik-korrekheitssatz.png} + + Beispiel: Seien $\varphi$ Formel und $x$ Variable. Dann gelten + $\{\lnot\forall x\varphi\}\Vdash \exists x\lnot\varphi$ und + $\{\exists x\lnot\varphi\}\Vdash\lnot\forall x\varphi$. - Beweis: + \includegraphics[width=\linewidth]{Assets/Logik-beispiel-korrekheitssatz.png} + + \subsection{Vollständigkeit}\label{vollstuxe4ndigkeit-1} + + Können wir durch mathematische Beweise zu allen korrekten Aussagen + kommen? Können wir durch das natürliche Schließen zu allen korrekten + Aussagen kommen? + + Existiert eine Menge $\Gamma$ von $\sum$-Formeln und eine $\sum$-Formel + $\varphi$ mit $\Gamma\Vdash\varphi$ und $\Gamma\not\vdash\varphi$? + + Frage: Gilt $\Gamma\Vdash\varphi \Rightarrow \Gamma\vdash\varphi$ bzw. + $\varphi$ ist allgemeingültig $\Rightarrow\varphi$ ist Theorem? + + Plan: - z.z. ist $\Gamma\Vdash\varphi \Rightarrow \Gamma\vdash\varphi$. + - dies ist äquivalent zu + $\Gamma\not\vdash\varphi \Rightarrow \Gamma\not\Vdash\varphi$. - hierzu + geht man folgendermaßen vor: - $\Gamma\not\vdash\varphi$ - + $\Leftrightarrow \Gamma\cup\{\lnot\varphi\}$ konsistent - + $\Rightarrow \exists\Delta\supseteq\Gamma\cup\{\lnot\varphi\}$ maximal + konsistent - $\Rightarrow \exists\Delta^+ \supseteq\Delta$ maximal + konsistent mit Konkretisierung - $\Rightarrow \Delta^+$ erfüllbar - + $\Rightarrow \Delta$ erfüllbar - + $\Rightarrow \Gamma\cup\{\lnot\varphi\}$ erfüllbar - + $\Leftrightarrow \Gamma\cup\{\lnot\varphi\}$ + + \begin{quote} + Definition + + Eine Menge $\Delta$ von Formeln hat Konkretisierungen, wenn für alle + $\exists x\varphi\in\Delta$ ein variablenloser Term $t$ existiert mit + $\varphi[x:=t]\in\Delta$. + \end{quote} + + \begin{quote} + Satz + + Sei $\Delta$ eine maximal konsistente Menge von $\sum$-Formeln. Dann + existiert eine Signatur $\sum^+ \supseteq\sum$ und eine maximal + konsistente Menge von $\sum^+$-Formeln mit Konkretisierungen, so dass + $\Delta\subseteq\Delta^+$. + \end{quote} + + Beweis: Wir konstruieren induktiv Signaturen $\sum_n$, maximal + konsistente Menge von $\sum_n$-Formeln $\Delta_n$ und konsistente Mengen + von $\sum_{n+1}$-Formeln $\Delta'_{n+1}$ mit - + $\sum =\sum_0 \subseteq\sum_1 \subseteq\sum_2...$ und - + $\Delta = \Delta_0 \subseteq \Delta'_1 \subseteq\Delta_1 \subseteq\Delta'_2...$ + und setzen dann - $\sum^+ =\bigcup_{n\geq 0} \sum_n$ und + $\Delta^+ = \bigcup_{n\geq 0} \Delta_n$ + + \begin{enumerate} + \itemsep1pt\parskip0pt\parsep0pt + \item + IA: $\sum_0 := \sum$ , $\Delta_0:=\Delta$ + \item + IV: Sei $n\geq 0$ und $\Delta_n$ maximal konsistente Menge von + $\sum_n$-Formeln. $\psi=\exists x\varphi$, ein ``neues'' + Konstantensymbol $c_{\psi}$ + \item + IS: $\sum_{n+1}$: alle Symbole aus $\sum_n$ und, für jede Formel + $\psi\in\Delta_n$ der Form + $\Delta'_{n+1}:= \Delta_n\cup\{\varphi[x:=c_{\psi}]|\psi=\exists x\varphi\in\Delta_n\}$ + + \begin{itemize} + \item + ohne Beweis: $\Delta'_{n+1}$ ist konsistent + \item + Idee: Ist $\varphi$ $\sum_n$-Formel mit + $\Delta'_{n+1}\vdash\varphi$, so gilt $\Delta_n\vdash\varphi$. + \item + Konsistenz von $\Delta'_{n+1}$ folgt mit $\varphi=\bot$ + \item + Analog zum Satz aus Vorlesung 4 existiert + $\Delta_{n+1}\supseteq \Delta'_{n+1}$ maximal konsistent + \end{itemize} + \end{enumerate} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + Damit ist die Konstruktion der Signaturen $\sum_n$ und der maximal + konsistenten Mengen $\Delta_n$ von $\sum_n$-Formeln abgeschlossen. + \item + noch z.z.: $\Delta^+$ hat Konkretisierungen und ist maximal konsistent + \item + $\Delta^+$ hat Konkretisierungen: Sei + $\psi=\exists x\varphi\in\Delta^+$ + + \begin{itemize} + \item + $\Rightarrow$ es gibt $n\geq 0$ mit $\psi\in\Delta_n$ + \item + $\Rightarrow \varphi[x:=c_{\psi}]\in\Delta'_{n+1}\subseteq \Delta_{n+1}\subseteq\Delta^+$. + \end{itemize} + \item + Konsistenz: (indirekt) angenommen, $\Delta^+\vdash\bot$ + + \begin{itemize} + \item + Da jede Deduktion endlich ist, existiert $\Gamma\subseteq\Delta^+$ + endlich mit $\Gamma\vdash\bot$. + \item + $\Rightarrow$ es gibt $n\geq 0$ mit $\Gamma\subseteq\Delta_n$ + \item + $\Rightarrow \Delta_n\vdash\bot$ - im Widerspruch zur Konsistenz von + $\Delta_n$. + \end{itemize} + \item + maximale Konsistenz: (indirekt) angenommen, $\Delta^+$ ist nicht + maximal konsistent + + \begin{itemize} + \item + $\Rightarrow$ es gibt $\Gamma\not\subseteq\Delta^+$ konsistent + \item + $\Rightarrow$ es gibt $\varphi\in\Gamma\backslash\Delta^+$ + \item + $\Rightarrow$ $\Delta^+\cup\{\varphi\}\subseteq\Gamma$ konsistent + \item + $\varphi$ ist $\sum^+$-Formel $\Rightarrow$ es gibt $n\geq 0$, so + dass $\varphi$ eine $\sum_n$-Formel ist. + \item + $\Delta_n$ maximal konsistente Menge von $\sum_n$-Formeln + \item + $\Rightarrow$ $\varphi\in\Delta_n\subseteq\Delta^+$ oder + $\lnot\varphi\in\Delta_n\subseteq\Delta^+$ + \item + $\Rightarrow$ $\lnot\varphi\in\Delta^+\subseteq\Gamma$ + \item + Also $\varphi,\lnot\varphi\in\Gamma$, im Widerspruch zur Konsistenz + von $\Gamma$. + \end{itemize} + \end{itemize} + + \begin{quote} + Satz + + Sei $\Delta^+$ maximal konsistente Menge von $\sum^+$-Formeln mit + Konkretisierungen. Dann ist $\Delta^+$ erfüllbar. + \end{quote} + + Beweisidee: Sei $T$ die Menge der variablenlosen $\sum^+$-Terme. Auf $T$ + definieren wir eine Äquivalenzrelation $\sim $ durch + $s\sim t\Leftrightarrow \Delta^+\vdash(s=t)\Leftrightarrow (s=t)\in\Delta^+$ + Sei $A$ die folgende $\sum^+$-Struktur: - $U_A:=T/\sim $ ist die Menge der + $\sim $-Äquivalenzklassen - + $R^A=\{([t_1],...,[t_k])|t_1 ,...,t_k\in T,R(t_1,...,t_k)\in\Delta^+\}$ + für alle Relationssymbole R aus $\sum^+$ - + $f^A([t_1],...,[t_k]) = [f(t_1,...,t_k)]$ für alle $t_1,...,t_k\in T$ + und alle Funktionssymbole $f$ aus $\sum^+$ (Bemerkung: dies ist + wohldefiniert) Dann gilt tatsächlich $A\Vdash\Delta^+$. + + \begin{quote} + Satz: Vollständigkeitssatz der Prädikatenlogik + + Sei $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine + $\sum$-Formel. Dann gilt + $\Gamma\Vdash\varphi \Rightarrow \Gamma\vdash\varphi$. Insbesondere ist + jede allgemeingültige Formel ein Theorem. + \end{quote} + + Beweis:indirekt - $\Gamma\not\vdash\varphi$ - + $\Gamma\cup\{\lnot\varphi\}$ konsistent - $\Gamma\cup\{\lnot\varphi\}$ + erfüllbar - $\exists\Delta\supseteq\Gamma\cup\{\lnot\varphi\}$ maximal + konsistent - $\exists\Delta^+\supseteq\Delta$ maximal konsistent mit + Konkretisierungen - $\Delta^+$ erfüllbar - $\Delta$ erfüllbar - + $\Gamma\not\Vdash\varphi$ + + Bemerkung - Dieser Satz ist (im wesentlichen) der berühmte Gödelsche + Vollständigkeitssatz von 1930. - Der obige Beweis wurde von Leon Henkin + 1949 veröffentlicht. + + Wir haben gleichzeitig gezeigt: \textgreater{} Satz \textgreater{} + \textgreater{} Sei $\Gamma$ höchstens abzählbar unendliche und + konsistente Menge von Formeln. Dann hat $\Gamma$ ein höchstens abzählbar + unendliches Modell. + + Beweis: $\Gamma$ konsistent heißt $\Gamma\not\vdash\bot$. Obiger Beweis + gibt ein Modell $A$ von $\Gamma\cup\{\lnot\bot\}$ an. Wir zeigen, dass + diese Struktur $A$ höchstens abzählbar unendlich ist: - Sei $\sum$ + Signatur der Relations- und Funktionssymbole aus $\Gamma$. - + $|\Gamma|\leq \mathbb{N}_0 \Rightarrow |\sum|\leq \mathbb{N}_0$ - + $\Rightarrow |\sum_n|\leq \mathbb{N}_0$ und + $|\Delta_n|\leq \mathbb{N}_0$ für alle $n\geq 0$ - + $\Rightarrow |\sum^+|,|\Delta^+| \leq\mathbb{N}_0$ - + $\Rightarrow |T| \leq\mathbb{N}_0$ - $\Rightarrow A$ hat + $\leq\mathbb{N}_0$ viele Elemente - + $\Rightarrow \Gamma\cup\{\lnot\bot\}$ hat ein höchstens abzählbar + unendliches Modell - $\Rightarrow \Gamma$ hat ein höchstens abzählbar + unendliches Modell + + \subsection{Vollständigkeit und Korrektheit für die + Prädikatenlogik}\label{vollstuxe4ndigkeit-und-korrektheit-fuxfcr-die-pruxe4dikatenlogik} + + \begin{quote} + Satz + + Seien $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine + $\sum$-Formel. Dann gilt + $\Gamma\vdash\varphi\Leftrightarrow \Gamma\Vdash\varphi$. Insbesondere + ist eine $\sum$-Formel genau dann allgemeingültig, wenn sie ein Theorem + ist. + \end{quote} + + Beweis: Folgt unmittelbar aus Korrektheitssatz und Vollständigkeitssatz. + + \subsubsection{Folgerung 1: Kompaktheit}\label{folgerung-1-kompaktheit} + + \begin{quote} + Satz + + Seien $\Gamma$ eine u.U. unendliche Menge von $\sum$-Formeln und + $\varphi$ eine $\sum$-Formel mit $\Gamma\Vdash\varphi$. Dann existiert + $\Gamma'\subseteq\Gamma$ endlich mit $\Gamma'\Vdash\varphi$. + \end{quote} + + Beweis: $\Gamma\Vdash\varphi$ - $\Gamma\vdash\varphi$ (nach dem + Vollständigkeitssatz) - es gibt Deduktion von $\varphi$ mit Hypothesen + $\gamma_1,...,\gamma_n\in\Gamma$ - + $\Gamma'=\{\gamma_1,...,\gamma_n\}\subseteq\Gamma$ endlich mit + $\Gamma'\vdash\varphi$ - $\Gamma'\vdash\varphi$ (nach dem + Korrektheitssatz). + + \begin{quote} + Folgerung (Kompaktheits- oder Endlichkeitssatz) + + Sei $\Gamma$ eine u.U. unendliche Menge von $\sum$-Formeln. Dann gilt + $\Gamma$ erfüllbar $\Leftrightarrow \forall\Gamma'\subseteq\Gamma$ + endlich: $\Gamma'$ erfüllbar + \end{quote} + + Beweis: - $\Gamma$ unerfüllbar - + $\Leftrightarrow \Gamma\cup\{\lnot\bot\}$ unerfüllbar - + $\Leftrightarrow \Gamma\Vdash\bot$ - $\Leftrightarrow$ es gibt + $\Gamma'\subseteq\Gamma$ endlich: $\Gamma'\Vdash\bot$ - + $\Leftrightarrow$ es gibt $\Gamma'\subseteq\Gamma$ endlich: + $\Gamma'\cup\{\lnot\bot\}$ unerfüllbar - $\Leftrightarrow$ es gibt + $\Gamma'\subseteq\Gamma$ endlich: $\Gamma'$ unerfüllbar + + \begin{quote} + Satz + + Sei $\Delta$ eine u.U. unendliche Menge von $\sum$-Formeln, so dass für + jedes $n\in\mathbb{N}$ eine endliche Struktur $A_n$ mit $A_\Vdash\Delta$ + existiert, die wenigstens $n$ Elemente hat. Dann existiert eine + unendliche Struktur $A$ mit $A\Vdash\Delta$. + \end{quote} + + Beweis: für $n\in\mathbb{N}$ setze + $\varphi_n=\exists x_1 \exists x_2 ...\exists x_n \bigwedge_{1\leq i< j \leq n} x_i \not= x_j$ + - und $\Gamma =\Delta\cup\{\varphi_n | n\geq 0\}$. - Für + $\Gamma'\subseteq\Gamma$ endlich existiert $n\in\mathbb{N}$ mit + $\varphi_m\not\in\Gamma'$ für alle $m\geq n$ - + $\Rightarrow A_n\Vdash\Gamma'$, d.h. jede endliche Teilmenge von + $\Gamma$ ist erfüllbar. - $\Rightarrow$ es gibt Struktur $A$ mit + $A\Vdash\Gamma$ - $\Rightarrow$ A hat $\geq n$ Elemente (für alle + $n\in\mathbb{N}$) + + \subsubsection{Folgerung 2: + Löwenheim-Skolem}\label{folgerung-2-luxf6wenheim-skolem} + + \begin{quote} + Frage: Gibt es eine Menge $\Gamma$ von $\sum$-Formeln, so dass für alle + Strukturen $A$ gilt: + $A\Vdash\Gamma \Leftrightarrow A\cong (\mathbb{R},+,*, 0 , 1 )$? + \end{quote} + + \begin{quote} + Satz von Löwenheim-Skolem + + Sei $\Gamma$ erfüllbare und höchstens abzählbar unendliche Menge von + $\sum$-Formeln. Dann existiert ein höchstens abzählbar unendliches + Modell von $\Gamma$. + \end{quote} + + Beweis: - $Gamma$ erfüllbar $\Rightarrow \Gamma\not\Vdash\bot$ - + $\Rightarrow$ $\Gamma\not\vdash\bot$, d.h. $\Gamma$ konsistent - + $\Rightarrow \Gamma$ hat ein höchstens abzählbar unendliches Modell. + + Die Frage auf der vorherigen Folie muß also verneint werden: - + angenommen, $\Gamma$ wäre eine solche Menge - + $\Rightarrow |\Gamma|\leq \mathbb{N}_0$ - $\Rightarrow \Gamma$ hat ein + höchstens abzählbar unendliches Modell $A$ - + $\Rightarrow A\not\cong (\mathbb{R},+,*, 0 , 1 )$ + + \subsubsection{Folgerung 3: + Semi-Entscheidbarkeit}\label{folgerung-3-semi-entscheidbarkeit} + + \begin{quote} + Satz + + Die Menge der allgemeingültigen $\sum$-Formeln ist semi-entscheidbar. + \end{quote} + + Beweis:Sei$\varphi$ $\sum$-Formel. Dann gilt - $\varphi$ allgemeingültig + - $\Leftrightarrow \varphi$ Theorem - $\Leftrightarrow$ Es gibt + hypothesenlose Deduktion mit Konklusion $\varphi$ + + Ein Semi-Entscheidungsalgorithmus kann also folgendermaßen vorgehen: + Teste für jede Zeichenkette $w$ nacheinander, ob sie hypothesenlose + Deduktion mit Konklusion $\varphi$ ist. Wenn ja, so gib aus ``$\varphi$ + ist allgemeingültig''. Ansonsten gehe zur nächsten Zeichenkette über. + + \subsubsection{Der Satz von Church}\label{der-satz-von-church} + + Jetzt zeigen wir, daß dieses Ergebnis nicht verbessert werden kann: Die + Menge der allgemeingültigen $\sum$-Formeln ist nicht entscheidbar. Wegen + $\varphi$ allgemeingültig $\Leftrightarrow\lnot\varphi$ unerfüllbar + reicht es zu zeigen, dass die Menge der erfüllbaren Sätze nicht + entscheidbar ist. Genauer zeigen wir dies sogar für ``Horn-Formeln'': + + \begin{quote} + Definition + + Eine Horn-Formel ist eine Konjunktion von $\sum$-Formeln der Form + $\forall x_1 \forall x_2 ...\forall x_n((\lnot\bot \wedge\alpha_1\wedge\alpha_2\wedge...\wedge\alpha_m)\rightarrow\beta)$, + wobei $\alpha_1,...,\alpha_m$ und $\beta$ atomare $\sum$-Formeln sind. + \end{quote} + + Unser Beweis reduziert die unentscheidbare Menge PCP auf die Menge der + erfüllbaren Horn-Formeln. + + Im folgenden sei also $I=((u_1,v_1),(u_2,v_2),...,(u_k,v_k))$ ein + Korrespondenzsystem und $A$ das zugrundeliegende Alphabet. Hieraus + berechnen wir eine Horn-Formel $\varphi_I$, die genau dann erfüllbar + ist, wenn $I$ keine Lösung hat. Wir betrachten die Signatur + $\sum= (\Omega,Rel,ar)$ mit - $\Omega=\{e\}\cup\{f_a|a\in A\}$ mit + $ar(e) =0$ und $ar(f_a) =1$ für alle $a\in A$. - $Rel=\{R\}$ mit + $ar(R)=2$. + + Zur Abkürzung schreiben wir $f_{a_1 a_2 ...a_n} (x)$ für + $f_{a_1}(f_{a_2}(...(f_{a_n}(x))...))$ für alle $a_1,a_2,...,a_n\in A$ + und $n\geq 0$ (insbes. steht $f_{\epsilon}(x)$ für $x$). + + Zunächst betrachten wir die folgende Horn-Formel $\psi_I$: - + $\wedge \bigwedge_{1\leq j \leq k}^{R(e,e)} \forall x,y(R(x,y)\rightarrow R(f_{u_j}(x),f_{v_j}(y)))$ + - $\wedge \bigwedge_{a\in A} \forall x(e=f_a(x)\rightarrow \bot)$ + + Beispiel: Betrachte die $\sum$-Struktur $A$ mit Universum $U_A=A^*$ - + $e^A=\epsilon$ - $f_a^A(u) =au$ - + $R^A=\{(u_{i1} u_{i2} ...u_{in},v_{i1} v_{i2} ...v_{in})|n\geq 0 , 1\geq i_1,i_2,...,i_n\geq k\}$ + - Für $u,v\in A^*$ gilt $f_u^A(v) =uv$. - Dann gilt $A\Vdash \psi_I$. + + \begin{quote} + Lemma + + Angenommen, das Korrespondenzsystem $I$ hat keine Lösung. Dann ist die + Horn-Formel $\varphi_I=\psi_I \wedge \forall x(R(x,x)\rightarrow x=e)$ + erfüllbar. + \end{quote} + + Beweis: Sei $A$ die obige Struktur mit $A\Vdash\psi_I$. - Um + $A\Vdash\forall x(R(x,x)\rightarrow x=e)$ zu zeigen, sei $w\in U_A$ + beliebig mit $(w,w)\in R^A$. - Die Definition von $R^A$ sichert die + Existenz von $n\geq 0$ und $1\leq i_1,i_2,...,i_n\leq k$ mit + $u_{i1} u_{i2}...u_{in}=w=v_{i1} v_{i2} ...v_{in}$. - Da $I$ keine + Lösung hat, folgt $n=0$ und damit $w=\epsilon$. + + \begin{quote} + Lemma + + Sei $B$ Struktur mit $B\Vdash\psi_I$. Dann gilt + $(f_{u_{i_1} u_{i_2} ...u_{i_n}}^B (e^B),f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B))\in R^B$ + für alle $n\geq 0, 1\leq i_1,i_2,...,i_n \leq k$. + \end{quote} + + Beweis: per Induktion über $n\geq 0$. - IA: für $n=0$ gelten + $f_{u_{i_1} u_{i_2} ...u_{i_n}}^B(e^B) =e^B$ und + $f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B) =e^B$ - und damit + $(f_{u_{i_1} u_{i_2} ...u_{i_n}}^B(e^B), f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B) \in R^B$ + - wegen $B\Vdash\psi_I$. - IS: Seien $n>0$ und + $1\leq i_1 ,i_2 ,...,i_n\leq k$. - Mit $u=u_{i2} u_{i3} ...u_{in}$ und + $v=v_{i2} v_{i3} ...v_{in}$ gilt nach IV + $(f_u^B(e^B),f_v^B(e^B))\in R^B$. Wegen $B\Vdash\psi_I$ folgt + $f_{u_{i_1} u_{i_2} ...u_{i_n}}^B(e^B), f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B) = (f_{u_{i1}}^B (f_u^B(e^B)),f_{v_{i1}}^B (f_v^B(e^B)))\in RB$. + + \begin{quote} + Lemma + + Angenommen, $(i_1,...,i_n)$ ist eine Lösung von $I$. Dann ist die + $\sum$-Formel $\varphi_I$ unerfüllbar. + \end{quote} + + \begin{quote} + Satz + + Die Menge der unerfüllbaren Horn-Formeln ist nicht entscheidbar. + \end{quote} + + Beweis: Die Abbildung $I\rightarrow\varphi_I$ ist berechenbar. + + Nach den vorherigen Lemmata ist sie eine Reduktion von PCP auf die Menge + der unerfüllbaren Horn-Formeln. Da PCP unentscheidbar ist (vgl. + Automaten, Sprachen und Komplexität), ist die Menge der unerfüllbaren + Horn-Formeln unentscheidbar. + + \begin{quote} + Folgerung (Church 1936) + + Die Menge der allgemeingültigen $\sum$-Formeln ist nicht entscheidbar. + \end{quote} + + Beweis: Eine $\sum$-Formel $\varphi$ ist genau dann unerfüllbar, wenn + $\lnot\varphi$ allgemeingültig ist. Also ist + $\varphi\rightarrow\lnot\varphi$ eine Reduktion der unentscheidbaren + Menge der unerfüllbaren $\sum$-Formeln auf die Menge der + allgemeingültigen $\sum$-Formeln, die damit auch unentscheidbar ist. + + Allgemeingültige $\sum$-Formeln gelten in allen Strukturen. Was + passiert, wenn wir uns nur auf ``interessante'' StrukturenAeinschränken + (z.B. auf eine konkrete), d.h. wenn wir die Theorie $Th(A)$ von $A$ + betrachten? + + \subsection{Theorie der natürlichen + Zahlen}\label{theorie-der-natuxfcrlichen-zahlen} + + \begin{quote} + Definition + + Sei $A$ eine Struktur. Dann ist $Th(A)$ die Menge der + prädikatenlogischen $\sum$-Formeln $\varphi$ mit $A\Vdash\varphi$. Diese + Menge heißt die(elementare) Theorie von $A$. + \end{quote} + + Beispiel: Sei $N= (N,\leq,+,*, 0 , 1 )$. Dann gelten - + $(\forall x\forall y:x+y=y+x)\in Th(N)$ - + $(\forall x\exists y:x+y= 0 )\not\in Th(N)$ - aber + $(\forall x\exists y:x+y= 0 )\in Th((Z,+, 0 ))$. + + \begin{quote} + Lemma + + Die Menge $Th(N)$ aller Sätze $\varphi$ mit $N\Vdash\varphi$ ist nicht + entscheidbar. + \end{quote} + + \begin{quote} + Zahlentheoretisches Lemma + + Für alle $n\in N,x_0,x_1,...,x_n\in N$ existieren $c,d\in N$, so dass + für alle $0\leq i\leq n$ gilt: $x_i=c\ mod ( 1 +d*(i+ 1 ))$. + \end{quote} + + Beweis:Setze $m= max\{n,x_0,x_1 ,...,x_n\}$ und $d=2*3*4...(m+1)$. Dann + sind die Zahlen $1+d, 1+d*2,..., 1 +d*(n+1)$ paarweise teilerfremd. Nach + dem Chinesischen Restsatz folgt die Existenz einer natürlichen Zahl $c$. + + Bemerkung: Es gibt $\sum$-Formeln - $mod(x_1,x_2 ,y)$ mit + $N\Vdash_{\alpha} mod \Leftrightarrow \alpha (x_1) mod\alpha (x_2) =\alpha (y)$. + - $\gamma(x_1 ,x_2 ,x_3 ,y)$ mit + $N\Vdash_{\alpha} \gamma\Leftrightarrow \alpha(x_1) mod(1+\alpha(x_2)*(\alpha (x3)+1)) =\alpha (y)$. + + \begin{quote} + Satz + + Sei $A$ eine Struktur, so dass $Th(A)$ semi-entscheidbar ist. Dann ist + $Th(A)$ entscheidbar. + \end{quote} + + \begin{quote} + Korollar Die Menge $TH(N)$ der Aussagen $\varphi$ mit $N\Vdash\varphi$ + ist nicht semi-entscheidbar. + \end{quote} + + \begin{quote} + Korollar (1. Gödelscher Unvollständigkeitssatz) + + Sei $Gamma$ eine semi-entscheidbare Menge von Sätzen mit $N\Vdash\gamma$ + für alle $\gamma\in\Gamma$. Dann existiert ein Satz $\varphi$ mit + $\Gamma\not\vdash\varphi$ und $\Gamma\not\vdash\lnot\varphi$ (d.h. + ``$\Gamma$ ist nicht vollständig''). + \end{quote} + + \subsection{2. Semi Entscheidungsverfahren für allgemeingültige + Formeln}\label{semi-entscheidungsverfahren-fuxfcr-allgemeinguxfcltige-formeln} + + bekanntes Verfahren mittels natürlichem Schließen: Suche hypothesenlose + Deduktion mit Konklusion $\psi$. + + Jetzt alternatives Verfahren, das auf den Endlichkeitssatz der + Aussagenlogik zurückgreift: - Berechne aus $\sum$-Formel $\psi$ eine + Menge E von aussagenlogischen Formeln mit $E$ unerfüllbar + $\Leftrightarrow\lnot\psi$ unerfüllbar $\Leftrightarrow\psi$ + allgemeingültig - Suche endliche unerfüllbare Teilmenge $E'$ von $E$ + + Kern des Verfahrens ist es also, aus $\sum$-Formel $\varphi$ eine Menge + $E$ aussagenlogischer Formeln zu berechnen mit $\varphi$ unerfüllbar + $\Leftrightarrow$ E unerfüllbar. + + Hierzu werden wir die Formel $\varphi$ zunächst in zwei Schritten + (Gleichungsfreiheit und Skolem-Form) vereinfachen, wobei die Formel + erfüllbar bzw unerfüllbar bleiben muss. + + \begin{quote} + Definition + + Zwei $\sum$-Formeln $\varphi$ und $\psi$ heißen + erfüllbarkeitsäquivalent, wenn gilt: $\varphi$ ist erfüllbar + $\Leftrightarrow\psi$ ist erfüllbar + \end{quote} + + Unsere Vereinfachungen müssen also erfüllbarkeitsäquivalente Formeln + liefern. + + \subsubsection{Elimination von + Gleichungen}\label{elimination-von-gleichungen} + + \begin{quote} + Definition + + Eine $\sum$-Formel ist gleichungsfrei, wenn sie keine Teilformel der + Form $s=t$ enthält. + \end{quote} + + Ziel: aus einer $\sum$ Formel $\varphi$ soll eine + erfüllbarkeitsäquivalente gleichungsfreue Formel $\varphi'$ berechnet + werden + + Bemerkung: Man kann i.a. keine äquivalente gleichungsfreie Formel + $\varphi'$ angeben, da es eine solche z.B. zu + $\varphi=(\forall x\forall y:x=y)$ nicht gibt. + + Idee: Die Formel $\varphi'$ entsteht aus $\varphi$, indem alle + Teilformeln der Form $x=y$ durch $GI(x,y)$ ersetzt werden, wobei $GI$ + ein neues Relationssymbol ist. + + Notationen - Sei $\sum=(\Omega,Rel,ar)$ endliche Signatur und $\varphi$ + $\sum$-Formel - $\sum_{GI} = (\Omega, Rel\bigcup^+\{GI\},ar_{GI})$ mit + $ar_{GI}(f)$ für alle $f\in\Omega\cup Rel$ und $ar_{GI}(GI)=2$ - Für + eine $\sum$-Formel $\varphi$ bezeichnet $\varphi_{GI}$ die + $\sum_{GI}$-Formel, die aus $\varphi$ entsthet, indem alle Vorkommen und + Teilformen $s=t$ durch $GI(s,t)$ ersetzt werden. + + Behauptung: $\varphi$ erfüllbar $\Rightarrow \varphi_{GI}$ erfüllbar + + Behauptung: es gilt nicht $\varphi$ erfüllbar $\Leftarrow\varphi_{GI}$ + erfüllbar + + \begin{quote} + Definition + + Sei A eine $\sum$-Struktur und $\sim$ eine binäre Relation auf $U_A$. + Die Relation $\sim$ heißt Kongruenz auf A, wenn gilt: - $\sim$ ist eine + Äquivalentrelation (d.h. reflexiv, transitiv und symmetrisch) - für alle + $f\in\Omega$ mit $k=ar(f)$ und alle $a_1,b_1,...,a_k,b_k\in U_A$ gilt + $a_1\sim b_1,a_2\sim b_2,...,a_k\sim b_k\Rightarrow f^A(a_1,...,a_k)\sim f^A(b_1,...,b_k)$ + - für alle $R\in Rel$ mit $k=ar(R)$ und alle + $a_1,b_1,...,a_k,b_k\in U_A$ gilt + $a_1\sim b_1,...,a_k\sim b_k,(a_1,...,a_k)\in R^A\Rightarrow (b_1,...,b_k)\in R^A$. + \end{quote} + + \begin{quote} + Definition + + Sei $A$ eine $\sum$-Struktur und $\sim$ eine Kongruenz auf A. 1. Für + $a\in U_A$ sei $[a]=\{b\in U_A|a\sim b\}$ die Äquivalenzklasse von a + bzgl $\sim$. 2. Dann definieren wir den Quotienten $B=A\backslash \sim$ + von $A$ bzgl $\sim$ wie folgt: - + $U_B=U_A\backslash\sim = \{[a]|a\in U_A\}$ - Für jedes $f\in\Omega$ mit + $ar(f)=k$ und alle $a_1,...,a_k\in U_A$ setzten wir + $f^B([a_1],...,[a_k])=[f^A(a_1,...,a_k)]$ - für jede $R\in Rel$ mit + $ar(R)=k$ setzten wir + $R^B=\{([a_1],[a_2],...,[a_k])|(a_1,...,a_k)\in R^A\}$ 3. Sei + $p:Var\rightarrow U_A$ Variableninterpretation. Dann definieren die + Variableninterpretation + $p\backslash\sim: Var\rightarrow U_B:x\rightarrow[p(x)]$. + \end{quote} + + Veranschaulichung: + \includegraphics[width=\linewidth]{Assets/Logik-variableninterpretation-beispiel.png} + + \begin{quote} + Lemma 1 + + Sei A Struktur, $p:Var\rightarrow U_A$ Variableninterpretation und + $\sim$ Kongruenz. Seien weiter $B=A\backslash\sim$ und + $p_B=p\backslash\sim$. Dann gilt für jeden Term $:[p(t)]=p_B(t)$ + \end{quote} + + Beweis: per Induktion über den Aufbau des Terms t + + \begin{quote} + Lemma 2 + + Sei $A$ $\sum$-Struktur, $\sim$ Kongruenz und $B=A\backslash\sim$. Dann + gilt für alle $R\in Rel$ mit $k=ar(R)$ und alle $c_1,...,c_k\in U_A$: + $([c_1],[c_2],...,[c_k])\in R^B\Leftrightarrow (c_1,c_2,...,c_k)\in R^A$ + \end{quote} + + \begin{quote} + Satz + + Seien $A$ $\sum_{GI}$-Struktur und $p:Var\rightarrow U_A$ + Variableninterpretation, so dass $\sim=GI^A$ Kongruenz auf A ist. Seien + $B=A\backslash\sim$ und $p_B=p\backslash\sim$. Dann gilt für alle + $\sum$-Formeln + $\varphi: A\Vdash_p \varphi_{GI} \Leftrightarrow B\Vdash_{p_B} \varphi$ + \end{quote} + + Beweis: per Induktion über den Aufbau der Formel $\varphi$ + + \begin{quote} + Lemma + + Aus einer endlichen Signatur $\sum$ kann ein gleichungsfreuer Horn-Satz + $Kong_{\sum}$ über $\sum_{GI}$ berechnet werden, so dass für alle + $\sum_{GI}$-Strukturen $A$ gilt: + $A\Vdash Kong_{\sum} \Leftrightarrow GI^A$ ist eine Kongruenz + \end{quote} + + \begin{quote} + Satz + + Aus einer endlichen Signatur $\sum$ und einer $\sum$-Formel $\varphi$ + kann eine gleichungsfreie und erfüllbarkeitsäquivalente + $\sum_{GI}$-Formel $\varphi'$ berechnet werden. Ist $\varphi$ Horn + Formel, so ist auch $\varphi'$ Horn Formel. + \end{quote} + + Beweis: Setzte $\varphi' =\varphi_{GI}\wedge Kong_{\sum}$ und zeige: + $\varphi$ erfüllbar $\Leftrightarrow \varphi'$ erfüllbar. + + \subsection{Skolemform}\label{skolemform} + + Ziel: Jede $\sum$-Formel $\varphi$ ist erfüllbarkeitsäquivalent zu einer + $\sum$'-Formel $\varphi'=\forall x_1\forall x_2 ...\forall x_k \psi$, + wobei $\psi$ kein Quantoren enthält, $\varphi'$ heißt in Skolemform. + + Bemerkung: Betrachte die Formel $\exists x\exists y E(x,y)$. Es gibt + keine Formel in Skolemform, die hierzu äquivalent ist. + + 2 Schritte: 1. Quantoren nach vorne (d.h. Pränexform) 2. + Existenzquantoren eliminieren + + \begin{quote} + Definition + + Zwei $\sum$-Formeln $\varphi$ und $\psi$ sind äquivalent + (kurz:$\varphi\equiv\psi$), wenn für alle $\sum$-Strukturen $A$ und alle + Variableninterpretationen $\rho$ gilt: + $A\Vdash_{\rho} \psi \Leftrightarrow A\Vdash_{\rho}\psi$. + \end{quote} + + \begin{quote} + Lemma + + Seien $Q\in\{\exists ,\forall\}$ und + $\oplus\in\{\wedge,\vee,\rightarrow,\leftarrow\}$. Sei + $\varphi= (Qx \alpha)\oplus\beta$ und sei $y$ eine Variable, die weder + in $\alpha$ noch in $\beta$ vorkommt. Dann gilt + $\varphi \equiv \begin{cases} Qy(\alpha[x:=y]\oplus\beta) \text{ falls } \oplus\in\{\wedge,\vee,\leftarrow\}\\ \forall y(\alpha[x:=y]\rightarrow\beta) \text{ falls } \oplus=\rightarrow,Q=\exists \\ \exists y(\alpha[x:=y]\rightarrow\beta) \text{ falls }\oplus=\rightarrow,Q=\forall\end{cases}$ + \end{quote} + + Notwendigkeit der Bedingung ``$y$ kommt weder in $\alpha$ noch in + $\beta$ vor'': - + $(\exists x:f(x) \not =f(y))\wedge\beta \not\equiv\exists y: (f(y) \not =f(y)\wedge\beta)$ + - + $(\exists x:\lnot P(x))\wedge P(y)\not\equiv \exists y: (\lnot P(y) \wedge P(y))$ + + \begin{quote} + Lemma + + Seien $Q\in\{\exists,\forall\}$ und + $\oplus\in\{\wedge,\vee,\rightarrow,\leftarrow\}$. Sei + $\varphi= (Qx\alpha)\oplus\beta$ und sei $y$ eine Variable, die weder in + $\alpha$ noch in $\beta$ vorkommt. Dann gilt + $\varphi\equiv\begin{cases} Qy(\alpha[x:=y]\oplus\beta) \text{ falls }\oplus\in\{\wedge,\vee,\leftarrow\} \\ \forall y(\alpha[x:=y]\rightarrow\beta) \text{ falls }\oplus=\rightarrow,Q=\exists \\ \exists y(\alpha[x:=y]\rightarrow\beta) \text{ falls }\oplus=\rightarrow,Q=\forall \end{cases}$ + \end{quote} + + Beweis: (für den Fall $Q=\exists$ und $\oplus=\wedge$) - Seien $A$ + $\sum$-Struktur und $\rho$ Variableninterpretation. - Für $a\in U_A$ + setze $\rho_a:=\rho[y\rightarrow a]$. - Dann gilt + $\rho_a[x\rightarrow \rho_a(y)](z) =\rho[x\rightarrow a](z)$ für alle + $z\not=y$ + + Wir erhalten also - $A\vdash_\rho (\exists x\alpha)\wedge\beta$ - + $\Leftrightarrow A\vdash_\rho (\exists x\alpha) $ und + $A\vdash_\rho \beta$ - $\Leftrightarrow$ (es gibt $a\in U_A$ mit + $A\vdash_{\rho[x\rightarrow a]}\alpha$) und (es gilt + $A\vdash_\rho \beta$) - $\Leftrightarrow$ es gibt $a\in U_A$ mit + ($A\vdash_{\rho[x\rightarrow a]}\alpha$ und $A\vdash_\rho \beta$) - + $\Leftrightarrow$ es gibt $a\in U_A$ mit - + $A\vdash_{\rho_a[x\rightarrow \rho_a(y)]}\alpha$ (da $y$ in $\alpha$ + nicht vorkommt) - $A\vdash_{\rho_a} \beta$ (da $y$ in $\beta$ nicht + vorkommt) - $\Leftrightarrow$ es gibt $a\in U_A$ mit - + $A\vdash_{\rho_a} \alpha[x:=y]$ - $A\vdash_{\rho_a} \beta$ - + $\Leftrightarrow$ es gibt $a\in U_A$ mit + $A\vdash_{\rho[y\rightarrow a]}\alpha[x:=y]\wedge\beta$ - + $\Leftrightarrow A\vdash_\rho \exists y(\alpha[x:=y]\wedge\beta)$ + + \begin{quote} + Satz + + Aus einer endlichen Signatur $\sum$ und einer $\sum$-Formel $\varphi$ + kann eine äquivalente $\sum$-Formel + $\varphi'=Q_1 x_1 Q_2 x_2 ...Q_k x_k \psi$ (mit + $Q_i\in\{\exists,\forall\},\psi$ quantorenfrei und $x_i$ paarweise + verschieden) berechnet werden. Eine Formel $\varphi'$ dieser Form heißt + Pränexform. Ist $\varphi$ gleichungsfrei, so ist auch $\varphi'$ + gleichungsfrei. + \end{quote} + + Beweis: Der Beweis erfolgt induktiv über den Aufbau von $\varphi$: - + I.A. $\varphi$ ist atomare Formel: Setze $\varphi'=\varphi$. - I.S. - + $\varphi=\lnot\psi$ : Nach I.V. kann Formel in Pränexform + $\psi\equiv Q_1 x_1 Q_2 x_2 ...Q_m x_m \psi'$ berechnet werden. Mit + $\forall=\exists$ und $\exists=\forall$ setze + $\varphi'=Q_1 x_1 Q_2 x_2 ...Q_m x_m\lnot\psi'$. - + $\varphi=\exists x\psi$: Nach I.V. kann Formel in Pränexform + $\psi\equiv Q_1 x_1 Q_2 x_2 ...Q_m x_m \psi'$ berechnet werden. Setze + $\varphi'= \begin{cases} \exists x Q_1 x_1 Q_2 x_2 ...Q_m x_m\psi'\text{ falls }x\not\in\{x_1,x_2,...,x_m\}\\ Q_1 x_1 Q_2 x_2 ...Q_m x_m\psi'\text{ sonst}\end{cases}$ + - $\varphi=\alpha\wedge\beta$: Nach I.V. können Formeln in Pränexform + $\alpha\equiv Q_1 x_1 Q_2 x_2 ...Q_mx_m \alpha_0; \beta\equiv Q_1'y_1 Q_2'y_2 ...Q_n'y_n \beta_0$ + berechnet werden. + + Ziel: Berechnung einer erfüllbarkeitsäquivalenten Formel in Skolemform + + Idee: 1. wandle Formel in Pränexform um 2. eliminiere + $\exists$-Quantoren durch Einführen neuer Funktionssymbole + + Konstruktion: Sei + $\varphi=\forall x_1\forall x_2...\forall x_m\exists y\psi$ Formel in + Pränexform (u.U. enthält $\psi$ weitere Quantoren). Sei $g\not\in\Omega$ + ein neues m-stelliges Funktionssymbol. Setze + $\varphi'=\forall x_1\forall x_2...\forall x_m \psi[y:=g(x_1,...,x_m)]$. + Offensichtlich hat $\varphi$'einen Existenzquantor weniger als + $\varphi$. Außerdem ist $\varphi'$ keine $\sum$-Formel (denn sie + verwendet $g\not\in\Omega$), sondern Formel über einer erweiterten + Signatur. + + \begin{quote} + Lemma + + Die Formeln $\varphi$ und $\varphi'$ sind erfüllbarkeitsäquivalent. + \end{quote} + + Beweis: ``$\Leftarrow$'' Sei $A'$ Struktur und $\rho'$ + Variableninterpretation mit $A'\vdash_{\rho'}\varphi'$. Wir zeigen + $A'\vdash_{\rho'}\varphi$. Hierzu seien $a_1,...,a_m\in U_{A'}$ + beliebig. + + \begin{quote} + Satz + + Aus einer Formel $\varphi$ kann man eine erfüllbarkeitsäquivalente + Formel $\varphi$ in Skolemform berechnen. Ist $\varphi$ gleichungsfrei, + so auch $\varphi$. + \end{quote} + + Beweis: Es kann zu $\varphi$ äquivalente Formel + $\varphi_0 =Q_1 x_1 Q_2 x_2 ...Q_{\iota} x_{\iota} \psi$ in + Pränexform berechnet werden (mit $n\leq {\iota} $ Existenzquantoren). + Durch wiederholte Anwendung des vorherigen Lemmas erhält man Formeln + $\varphi_1,\varphi_2,...\varphi_n$ mit - $\varphi_i$ und $\varphi_{i+1}$ + sind erfüllbarkeitsäquivalent - $\varphi_{i+1}$ enthält einen + Existenzquantor weniger als $\varphi_i$ - $\varphi_{i+1}$ ist in + Pränexform - ist $\varphi_i$ gleichungsfrei, so auch $\varphi_{i+1}$ + + Dann ist $\bar{\varphi}=\varphi_n$ erfüllbarkeitsäquivalente (ggf. + gleichungsfreie) Formel in Skolemform. + + \subsection{Herbrand-Strukturen und + Herbrand-Modelle}\label{herbrand-strukturen-und-herbrand-modelle} + + Sei $\sum= (\Omega,Rel,ar)$ eine Signatur. Wir nehmen im folgenden an, + dass $\Omega$ wenigstens ein Konstantensymbol enthält. + + Das Herbrand-Universum $D(\sum)$ ist die Menge aller variablenfreien + $\sum$-Terme. + + Beispiel: $\Omega =\{b,f\}$ mit $ar(b) =0$ und $ar(f) =1$. Dann gilt + $D(\sum) =\{b,f(b),f(f(b)),f(f(f(b))),...\}$ + + Eine $\sum$-Struktur $A=(UA,(fA)f\in\Omega,(RA)R\in Rel)$ ist eine + Herbrand-Struktur, falls folgendes gilt: 1. $UA=D(\sum)$, 2. für alle + $f\in\Omega$ mit $ar(f)=k$ und alle $t_1,t_2,...,t_k\in D(\sum)$ ist + $f^A(t_1,t_2,...,t_k) =f(t_1,t_2,...,t_k)$. + + Für jede Herbrand-Struktur $A$, alle Variableninterpretationen $\rho$ + und alle variablenfreien Terme $t$ gilt dann $\rho(t) =t$. + + Ein Herbrand-Modell von $\varphi$ ist eine Herbrand-Struktur, die + gleichzeitig ein Modell von $\varphi$ ist. + + \begin{quote} + Satz + + Sei $\varphi$ eine gleichungsfreie Aussage in Skolemform. $\varphi$ ist + genau dann erfüllbar, wenn $\varphi$ ein Herbrand-Modell besitzt. + \end{quote} + + Beweis: - Falls $\varphi$ ein Herbrand-Modell hat, ist $\varphi$ + natürlich erfüllbar. - Sei nun $\varphi=\forall y_1...\forall y_n\psi$ + erfüllbar. Dann existieren eine $\sum$-Struktur + $A=(U_A,(f^A)_{f\in\Omega},(R^A)_{R\in Rel})$ und eine + Variableninterpretation $\rho$ mit $A\vdash_\rho \varphi$. + + \paragraph{Plan des Beweises}\label{plan-des-beweises} + + Wir definieren eine Herbrand-Struktur + $B=(D(\sum),(f^B)_{f\in\Omega},(R^B)_{R\in Rel})$: - Seien $f\in\Omega$ + mit $ar(f)=k$ und $t_1,...,t_k\in D(\sum)$. Um eine Herbrand-Struktur + $B$ zu konstruieren setzen wir $f^B(t_1,...,t_k) =f(t_1,...,t_k)$ - Sei + $R\in Rel$ mit $ar(R)=k$ und seien $t_1,...,t_k\in D(\sum)$. Dann setze + $(t_1,...,t_k)\in RB:\Leftrightarrow (\rho(t_1),...,\rho(t_k))\in RA$. + + Sei $\rho_B:Var \rightarrow D(\sum)$ beliebige Variableninterpretation. + + \subparagraph{Behauptung 1:}\label{behauptung-1} + + Ist $\psi$ eine quantoren- und gleichungsfreie Aussage, so gilt + $A\vdash_{\rho}\psi \Leftrightarrow B\vdash_{\rho B} \psi$. Diese + Behauptung wird induktiv über den Aufbau von $\psi$ gezeigt. + + \subparagraph{Intermezzo}\label{intermezzo} + + Behauptung 1 gilt nur für quantorenfreie Aussagen + + $\sum = (\Omega,Rel,ar)$ mit $\Omega =\{a\},ar(a) =0$ und + $Rel=\{E\},ar(E) =2$. Betrachte die Formel + $\varphi=\forall x(E(x,x)\wedge E(a,a))$ in Skolemform. + $A\vdash_\rho \varphi$ mit $U^A=\{a^A,m\}$ und + $E^A=\{(m,m),(a^A,a^A)\}$. Die konstruierte Herbrand-Struktur + $B:U_B=D(\sum) =\{a\}$ und $E^B=\{(a,a)\}$. + + Betrachte nun die Formel $\psi=\forall x,y E(x,y)$. Dann gilt + $B\vdash_{\rho B}\psi$ und $A\not\vdash_\rho \psi$. + + Für allgemeine Formeln in Skolemform (also u.U. mit Quantoren) können + wir also Behauptung 1 nicht zeigen, sondern höchstens die folgende + Abschwächung. + + \subparagraph{Behauptung 2:}\label{behauptung-2} + + Ist $\psi$ eine gleichungsfreie Aussage in Skolemform, so gilt + $A\vdash_\rho \psi \Rightarrow B\vdash_{\rho B}\psi$. (hieraus folgt dann + $B\vdash_{\rho B}\varphi$ wegen $A\vdash_\rho \varphi$) + + Diese Behauptung wird induktiv über die Anzahl $n$ der Quantoren in + $\psi$ bewiesen. + + \subsection{Die Herbrand-Expansion}\label{die-herbrand-expansion} + + verbleibende Frage: Wie erkennt man, ob eine gleichungsfreie Aussage in + Skolemform ein Herbrand-Modell hat? + + Beispiel: Seien $\sum=(\{a,f\},\{P,R\},ar)$ und + $\varphi=\forall x\forall y (P(a,x)\wedge\lnot R(f(y)))$. Jedes Herbrand-Modell A von $\varphi$ - hat als Universum das Herbrand-Universum $D(\sum)=\{a,f(a),f^2 (a),...\}=\{f^n(a)|n\geq 0\}$ - erfüllt $f^A(f^n(a))= f^{n+1} (a)$ für alle $n\geq 0$ + + Um ein Herbrand-Modell zu konstruieren, müssen (bzw. können) wir für + alle Elemente $s,t,u\in D(\sum)$ unabhängig und beliebig wählen, ob + $(s,t)\in P^A$ und $u\in R^A$ gilt. Wir fassen dies als + ``aussagenlogische B-Belegung'' B der ``aussagenlogischen atomaren + Formeln'' $P(s,t)$ bzw. $R(u)$ auf. + + Jede solche aussagenlogische B-Belegung $B$ definiert dann eine + Herbrand-Struktur $A_B$: - + $P^{A_B} = \{(s,t)\in D(\sum)^2 |B(P(s,t))= 1\}$ - + $R^{A_B} = \{u\in D(\sum) |B(R(u))= 1\}$ + + Mit $\varphi=\forall x\forall y(P(a,x)\wedge\lnot R(f(y)))$ gilt dann + $A_B \Vdash_\rho \varphi$ - + $\Leftrightarrow A_B \Vdash_{\rho[x\rightarrow f^m(a)][y\rightarrow f^n(a)]} P(a,x)\wedge\lnot R(f(y))$ + f.a. $m,n\geq 0$ - $\Leftrightarrow (a,fm(a))\in P^{A_B}$ und + $f^{n+1}(a)\not\in R^{A_B}$ f.a. $m,n\geq 0$ - + $\Leftrightarrow B(P(a,f^m(a)))= 1$ und $B(R(f^{n+1} (a)))= 0$ f.a. + $m,n\geq 0$ - + $\Leftrightarrow B(P(a,f^m(a))\wedge\lnot R(f^{n+1} (a)))= 1$ f.a. + $m,n\geq 0$ + + Also hat $\varphi$ genau dann ein Herbrand-Modell, wenn es eine + erfüllende B-Belegung $B$ der Menge aussagenlogischer Formeln + $E(\varphi)=\{P(a,f^m(a))\wedge\lnot R(f^{n+1}(a)) | m,n\geq 0\}$ gibt. + + Beispiellösung: Setzt $B(P(s,t))= 1$ und $B(R(s))= 0$ für alle + $s,t\in D(\sum)$. + + Diese B-Belegung erfüllt $E(\varphi)$ und ``erzeugt'' die + Herbrand-Struktur $A_B$ mit $P^{A_B}=D(\sum)^2$ und + $R^{A_B}=\varnothing$. + + Nach obiger Überlegung gilt $A_B\Vdash\varphi$, wir haben also ein + Herbrand-Modell von $\varphi$ gefunden. + + Sei $\varphi=\forall y_1\forall y_2...\forall y_n\psi$ gleichungsfreie + Aussage in Skolemform. + + Ziel: Konstruktion einer Menge aussagenlogischer Formeln, die genau dann + erfüllbar ist, wenn $\varphi$ ein Herbrand-Modell hat. + + Die Herbrand-Expansion von $\varphi$ ist die Menge der Aussagen + $E(\varphi)=\{\psi[y_1:=t_1][y_2:=t_2]...[y_n:=t_n]|t_1,t_2,...,t_n\in D(\sum)\}$ + + Die Formeln von $E(\varphi)$ entstehen also aus $\psi$, indem die + (variablenfreien) Terme aus $D(\sum)$ in jeder möglichen Weise in $\psi$ + substituiert werden. + + Wir betrachten die Herbrand-Expansion von $\varphi$ im folgenden als + eine Menge von aussagenlogischen Formeln. + + Die atomaren Formeln sind hierbei von der Gestalt $P(t_1,...,t_k)$ für + $P\in Rel$ mit $ar(P)=k$ und $t_1,...,t_k\in D(\sum)$. + + \begin{quote} + Konstruktion + + Sei + $B:\{P(t_1,...,t_k)|P\in Rel,k=ar(P),t_1,...,t_k\in D(\sum)\}\rightarrow B$ + eine B-Belegung. Die hiervon induzierte Herbrand-Struktur $A_B$ ist + gegeben durch + $P^{A_B} = \{(t_1,...,t_k)|t_1,...,t_k\in D(\sum),B(P(t_1,...,t_k))= 1\}$ + für alle $P\in Rel$ mit $ar(P)=k$. + \end{quote} + + \begin{quote} + Lemma + + Für jede quantoren- und gleichungsfreie Aussage $\alpha$ und jede + Variableninterpretation $\rho$ in $A_B$ gilt + $A_B\Vdash_\rho\alpha \Leftrightarrow B(\alpha)= 1$. + \end{quote} + + Beweis: - per Induktion über den Aufbau von $\alpha$ - I.A. $\alpha$ ist + atomar, d.h. $\alpha= P(t_1,...,t_k)$ mit $t_1,...,t_k$ variablenlos + $A_B\Vdash_\rho \alpha\Leftrightarrow (\rho(t_1),\rho(t_2),...,\rho(t_k))\in P^{A_B}\Leftarrow B(\alpha)= 1$ + - I.S. - + $\alpha=\beta\wedge\gamma: A_B\Vdash_\rho \alpha\Leftrightarrow A_B \Vdash_\rho\beta$ + und + $A_B\Vdash_\rho\gamma \Leftrightarrow B(\beta)=B(\gamma)= 1 \Leftrightarrow B(\alpha)= 1$ + - $\alpha=\beta\vee\gamma$: analog - $\alpha=\beta\rightarrow\gamma$: + analog - $\alpha=\lnot\beta$: analog + + \begin{quote} + Lemma + + Sei $\varphi=\forall y_1 \forall y_2 ...\forall y_n\psi$ gleichungsfreie + Aussage in Skolemform. Sie hat genau dann ein Herbrand-Modell, wenn die + Formelmenge $E(\varphi)$ (im aussagenlogischen Sinn) erfüllbar ist. + \end{quote} + + Beweis: Seien $A$ Herbrand-Struktur und $\rho$ Variableninterpretation. + Sei $B$ die B-Belegung mit + $B(P(t_1,...,t_k))= 1\Leftrightarrow(t_1,...,t_k)\in P^A$ für alle + $P\in Rel$ mit $k=ar(P)$ und $t_1,...,t_k\in D(\sum)$. Dann gilt + $A=A_B$. + + \begin{quote} + Satz von Gödel-Herbrand-Skolem + + Sei $\varphi$ gleichungsfreie Aussage in Skolemform. Sie ist genau dann + erfüllbar, wenn die Formelmenge $E(\varphi)$ (im aussagenlogischen Sinn) + erfüllbar ist. + \end{quote} + + Beweis: $\varphi$ erfüllbar $\Leftrightarrow$ $\varphi$ hat ein + Herbrand-Modell $\Leftrightarrow$ $E(\varphi)$ ist im aussagenlogischen + Sinne erfüllbar. + + \begin{quote} + Satz von Herbrand + + Eine gleichungsfreie Aussage $\varphi$ in Skolemform ist genau dann + unerfüllbar, wenn es eine endliche Teilmenge von $E(\varphi)$ gibt, die + (im aussagenlogischen Sinn) unerfüllbar ist. + + (Jacques Herbrand (1908-1931)) + \end{quote} + + Beweis: $\varphi$ unerfüllbar $\Leftrightarrow$ $E(\varphi)$ unerfüllbar + $\Leftrightarrow$ es gibt $M\subseteq E(\varphi)$ endlich und + unerfüllbar + + \subsection{Algorithmus von Gilmore}\label{algorithmus-von-gilmore} + + Sei $\varphi$ gleichungsfreie Aussage in Skolemform und sei + $\alpha_1,\alpha_2,\alpha_3,...$ eine Aufzählung von $E(\varphi)$. + + Eingabe: $\varphi$ + + \begin{verbatim} +n:=0; +repeat n := n +1; +until { alpha_1, alpha_2,..., alpha_n } ist unerfüllbar; + (dies kann mit Mitteln der Aussagenlogik, z.B. Wahrheitswertetabelle, getestet werden) +Gib "unerfüllbar" aus und stoppe. +\end{verbatim} + + Folgerung: Sei $\varphi$ eine gleichungsfreie Aussage in Skolemform. + Dann gilt: - Wenn die Eingabeformel $\varphi$ unerfüllbar ist, dann + terminiert der Algorithmus von Gilmore und gibt ``unerfüllbar'' aus. - + Wenn die Eingabeformel $\varphi$ erfüllbar ist, dann terminiert der + Algorithmus von Gilmore nicht, d.h. er läuft unendlich lange. + + Beweis: unmittelbar mit Satz von Herbrand + + Zusammenfassung: alternative Semi-Entscheidungsverfahren für die Menge + der allgemeingültigen Formeln. - Berechne aus $\psi$ eine zu $\lnot\psi$ + erfüllbarkeitsäquivalente gleichungsfreie Formel $\varphi$ in + Skolemform. - Suche mit dem Algorithmus von Gilmore nach einer endlichen + Teilmenge $E'$ von $E(\varphi)$, die unerfüllbar ist. + + \subsection{Berechnung von Lösungen}\label{berechnung-von-luxf6sungen} + + Beispiel - $\gamma = \forall x,y (R(x,f(y))\wedge R(g(x),y))$ - + $\varphi = \forall x,yR(x,y)$ - Gilt $\{\gamma\}\Vdash\varphi$? nein, + denn $A\Vdash\gamma\wedge\lnot\varphi$ mit - $A=(\mathbb{N},f^A,g^A,R)$ + - f\textsuperscript{A(n)=g}A(n)=n+1\$ für alle $n\in\mathbb{N}$ - + $R^A = \mathbb{N}^2 \backslash\{( 0 , 0 )\}$ - Gibt es variablenfreie + Terme $s$ und $t$ mit $\{\gamma\}\Vdash R(s,t)$? - ja: z.B. + $(s,t)=(g(f(a)),g(a))$ oder $(s,t)=(g(a),g(a))$ oder $(s,t)=(a,f(b))$ - + Kann die Menge aller Termpaare $(s,t)$ (d.h. aller ``Lösungen'') mit + $\{\gamma\}\Vdash R(s,t)$ effektiv und übersichtlich angegeben werden? - + Wegen $\{\gamma\}\Vdash R(s,t) \Leftrightarrow\gamma\wedge\lnot R(s,t)$ + unerfüllbar ist die gesuchte Menge der variablenfreien Terme $(s,t)$ + semi-entscheidbar, d.h. durch eine Turing-Maschine beschrieben. - Im + Rest des Logikteils der Vorlesung ``Logik und Logikprogrammierung'' + wollen wir diese Menge von Termpaaren ``besser'' beschreiben (zumindest + in einem Spezialfall, der die Grundlage der logischen Programmierung + bildet). + + \begin{quote} + Erinnerung + + Eine Horn-Klausel der Prädikatenlogik ist eine Aussage der Form + $\forall x_1\forall x_2...\forall x_n ((\lnot\bot\wedge\alpha_1 \wedge\alpha_2 \wedge...\wedge\alpha_m)\rightarrow\beta)$, + mit $m\geq 0$, atomaren Formeln $\alpha_1,...,\alpha_m$ und $\beta$ + atomare Formel oder $\bot$. + \end{quote} + + Aufgabe: $\varphi_1,...,\varphi_n$ gleichungsfreie Horn-Klauseln, + $\psi(x_1,x_2,...,x_{\iota} )=R(t_1,...,t_k)$ atomare Formel, keine + Gleichung. Bestimme die Menge der Tupel $(s_1,...,s_{\iota} )$ von + variablenfreien Termen mit + $\{\varphi_1,...,\varphi_n\}\Vdash\psi(s_1,...,s_{\iota} )=R(t_1,...,t_k)[x_1:=s_1]...[x_{\iota} :=s_{\iota} ]$, + d.h., für die die folgende Formel unerfüllbar ist: + $\bigwedge_{1\leq i\leq n} \varphi_i \wedge \lnot\psi(s_1,...,s_{\iota} ) \equiv \bigwedge_{1\leq i\leq n} \varphi_i\wedge(\psi(s_1,...,s_{\iota} )\rightarrow\bot)$ + + Erinnerung - Eine Horn-Formel der Prädikatenlogik ist eine Konjunktion + von Horn-Klauseln der Prädikatenlogik. - Eine Horn-Klausel der + Aussagenlogik ist eine Formel der Form + $(\lnot\bot\wedge q_1\wedge q_2 \wedge...\wedge q_m)\rightarrow r$ mit + $m\geq 0$, atomaren Formeln $q_1,q_2,...,q_m, r$ atomare Formel od. + $\bot$. + + Beobachtung - Wir müssen die Unerfüllbarkeit einer gleichungsfreien + Horn-Formel der Prädikatenlogik testen. - Ist $\varphi$ gleichungsfreie + Horn-Klausel der Prädikatenlogik, so ist $E(\varphi)$ eine Menge von + Horn-Klauseln der Aussagenlogik. + + Schreib- und Sprechweise - + $\{\alpha_1,\alpha_2,...,\alpha_n\}\rightarrow\beta$ für Horn-Klausel + der Prädikatenlogik + $(\lnot\bot\wedge\alpha_1 \wedge\alpha_2\wedge...\wedge\alpha_n)\rightarrow\beta$ + insbes. $\varnothing\rightarrow\beta$ für $\lnot\bot\rightarrow\beta$ - + $\{(N_i\rightarrow\beta_i) | 1\leq i\leq m\}$ für Horn-Formel + $\bigwedge_{1\leq i\leq m} (N_i\rightarrow\beta_i)$ + + Folgerung: Sei $\varphi =\bigwedge_{1\leq i\leq n} \varphi_i$ + gleichungsfreie Horn-Formel der Prädikatenlogik. Dann ist $\varphi$ + genau dann unerfüllbar, wenn $\bigcup_{1\leq i\leq n} E(\varphi_i)$ im + aussagenlogischen Sinne unerfüllbar ist. + + Beweis: Für $1\leq i\leq n$ sei + $\varphi_i=\forall x_1^i,x_2^i,...,x_{m_i}^i \psi_i$. Zur Vereinfachung + nehme wir an, daß die Variablen $x_j^i$ für $1\leq i\leq n$ und + $1\leq j\leq m_i$ paarweise verschieden sind. + + Folgerung: Eine gleichungsfreie Horn-Formel der Prädikatenlogik + $\varphi=\bigwedge_{1\leq i\leq n} \varphi_i$ ist genau dann + unerfüllbar, wenn es eine SLD-Resolution + $(M_0\rightarrow\bot,M_1\rightarrow\bot,...,M_m\rightarrow\bot)$ aus + $\bigcup_{1\leq i\leq n} E(\varphi_i)$ mit $M_m =\varnothing$ gibt. + + \subsection{Substitutionen}\label{substitutionen-1} + + Eine verallgemeinerte Substitution $\sigma$ ist eine Abbildung der Menge + der Variablen in die Menge aller Terme, so daß nur endlich viele + Variable $x$ existieren mit $\sigma(x) \not=x$. + + Sei $Def(\sigma)=\{x\ Variable|x\not =\sigma(x)\}$ der + Definitionsbereich der verallgemeinerten Substitution $\sigma$. Für + einen Term $t$ definieren wir den Term $t\sigma$ (Anwendung der + verallgemeinerten Substitution $\sigma$ auf den Term $t$) wie folgt + induktiv: - $x\sigma=\sigma(x)$ - + $[f(t_1 ,... ,t_k)]\sigma=f(t_1\sigma,... ,t_k\sigma)$ für Terme + $t_1,... ,t_k,f\in\Omega$ und $k=ar(f)$ Für eine atomare Formel + $\alpha=P(t_1 ,... ,t_k)$ (d.h. $P\in Rel,ar(P) =k,t_1 ,... ,t_k$ Terme) + sei $\alpha\sigma = P(t_1\sigma,... ,t_k\sigma)$ + + Verknüpfungvon verallgemeinerten Substitutionen: Sind $\sigma_1$ und + $\sigma_2$ verallgemeinerte Substitutionen, so definieren wir eine neue + verallgemeinerte Substitution $\sigma_1 \sigma_2$ durch + $(\sigma_1 \sigma_2)(x) = (x\sigma_1)\sigma_2$. + + Beispiel: Sei $x$ Variable und $t$ Term. Dann ist $\sigma$ mit + $\sigma(y) =\begin{cases} t \quad\text{ falls } x=y \\ y \quad\text{ sonst }\end{cases}$ + eine verallgemeinerte Substitution. Für alle Terme $s$ und alle atomaren + Formeln $\alpha$ gilt $s\sigma=s[x:=t]$ und $\alpha\sigma=\alpha[x:=t]$. + Substitutionen sind also ein Spezialfall der verallgemeinerten + Substitutionen. + + Beispiel: Die verallgemeinerte Substitution $\sigma$ mit + $Def(\sigma)=\{x,y,z\}$ und + $\sigma(x) =f(h(x')), \sigma(y) =g(a,h(x')), \sigma(z) =h(x')$ ist + gleich der verallgemeinerten Substitution + $[x:=f(h(x'))] [y:=g(a,h(x'))] [z:=h(x')] = [x:=f(z)] [y:=g(a,z)] [z:=h(x')]$. + Es kann sogar jede verallgemeinerte Substitution $\sigma$ als + Verknüpfung von Substitutionen der Form $[x:=t]$ geschrieben werden. + Vereinbarung: Wir sprechen ab jetzt nur von ``Substitutionen'', auch + wenn wir ``verallgemeinerte Substitutionen'' meinen. + + \begin{quote} + Lemma + + Seien $\sigma$ Substitution, $x$ Variable und $t$ Term, so dass - (i) + $x\not\in Def(\sigma)$ und - (ii) $x$ in keinem der Terme $y\sigma$ mit + $y\in Def(\sigma)$ vorkommt. Dann gilt + $[x:=t]\sigma=\sigma[x:=t\sigma]$. + \end{quote} + + Beispiele: Im folgenden sei $t=f(y)$. - Ist $\sigma=[x:=g(z)]$, so gilt + $x[x:=t]\sigma=t\sigma=t\not=g(z) =g(z)[x:=t\sigma] =x\sigma[x:=t\sigma]$. + - Ist $\sigma= [y:=g(x)]$, so gilt + $y[x:=t]\sigma=y\sigma=g(x) \not=g(f(g(x)))= g(x) [x:=t\sigma] =y\sigma[x:=t\sigma]$. + - Ist $\sigma= [y:=g(z)]$, so gelten + $Def([x:=t]\sigma) =\{x,y\}=Def(\sigma[x:=t\sigma]),[x:=t]\sigma(x) =f(g(z)) =\sigma[x:=t\sigma]$ + und $[x:=t]\sigma(y) =\sigma(z) =\sigma[x:=t\sigma]$, also + $[x:=t]\sigma=\sigma[x:=t\sigma]$. + + Beweis: Wir zeigen $y[x:=t]\sigma=y\sigma[x:=t\sigma]$ für alle + Variablen $y$. - $y=x$: Dann gilt $y[x:=t]\sigma=t\sigma$. Außerdem + $y\sigma=x$ wegen $y=x\not\in Def(\sigma)$ und damit + $y\sigma[x:=t\sigma]=x[x:=t\sigma]=t\sigma$. - $y\not =x$: Dann gilt + $y[x:=t]\sigma=y\sigma$ und ebenso $y\sigma[x:=t\sigma]=y\sigma$, da $x$ + in $y\sigma$ nicht vorkommt. + + \subsection{Unifikator/Allgemeinster + Unifikator}\label{unifikatorallgemeinster-unifikator} + + Gegeben seien zwei gleichungsfreie Atomformeln $\alpha$ und $\beta$. + Eine Substitution $\sigma$ heißt Unifikator von $\alpha$ und $\beta$, + falls $\alpha\sigma=\beta\sigma$. + + Ein Unifikator $\sigma$ von $\alpha$ und $\beta$ heißt allgemeinster + Unifikator von $\alpha$ und $\beta$, falls für jeden Unifikator + $\sigma'$ von $\alpha$ und $\beta$ eine Substitution $\tau$ mit + $\sigma'=\sigma \tau$ existiert. + + Aufgabe: Welche der folgenden Paare $(\alpha,\beta)$ sind unifizierbar? + \textbar{} $\alpha$ \textbar{} $\beta$ \textbar{} Ja \textbar{} Nein + \textbar{} \textbar{} --- \textbar{} --- \textbar{} --- \textbar{} --- + \textbar{} \textbar{} $P(f(x))$ \textbar{} $P(g(y))$ \textbar{} + \textbar{} \textbar{} $P(x)$ \textbar{}$P(f(y))$\textbar{}\textbar{} + \textbar{}$Q(x,f(y))$\textbar{} $Q(f(u),z)$\textbar{}\textbar{} + \textbar{}$Q(x,f(y))$\textbar{} $Q(f(u),f(z))$\textbar{}\textbar{} + \textbar{}$Q(x,f(x))$\textbar{} $Q(f(y),y)$\textbar{}\textbar{} + \textbar{}$R(x,g(x),g^2 (x))$\textbar{} $R(f(z),w,g(w))$ + \textbar{}\textbar{} + + \subsubsection{Zum allgemeinsten + Unifikator}\label{zum-allgemeinsten-unifikator} + + Eine Variablenumbenennung ist eine Substitution $\rho$, die $Def(\rho)$ + injektiv in die Menge der Variablen abbildet. + + \begin{quote} + Lemma + + Sind $\sigma_1$ und $\sigma_2$ allgemeinste Unifikatoren von $\alpha$ + und $\beta$, so existiert eine Variablenumbenennung $\rho$ mit + $\sigma_2=\sigma_1 \rho$. + \end{quote} + + Beweis: $\sigma_1$ und $\sigma_2$ allgemeinste Unifikatoren + $\Rightarrow$ es gibt Substitutionen $\tau_1$ und $\tau_2$ mit + $\sigma_1\tau_1 =\sigma_2$ und $\sigma_2\tau_2 =\sigma_1$. Definiere + eine Substitution $\rho$ durch: + $\rho(y) =\begin{cases} y\tau_1 \quad\text{ falls es x gibt, so dass y in } x\sigma_1 \text{ vorkommt}\\ y \quad\text{ sonst }\end{cases}$ + Wegen $Def(\rho)\subseteq Def(\tau_1)$ ist $Def(\rho)$ endlich, also + $\rho$ eine Substitution. - Für alle Variablen $x$ gilt dann + $x\sigma_1 \rho=x\sigma_1 \tau_1 =x\sigma_2$ und daher + $\sigma_2 =\sigma_1 \rho$. - Wir zeigen, dass $\rho(y)$ Variable und + $\rho$ auf $Def(\rho)$ injektiv ist: Sei $y\in Def(\rho)$. Dann + existiert Variable $x$, so dass $y$ in $x\sigma_1$ vorkommt. Es gilt + $x\sigma_1 =x\sigma_2\tau_2=x\sigma_1\tau_1\tau_2$, und damit + $y=y\tau_1 \tau_2 =y\rho \tau_2 =\rho(y)\tau_2$, d.h. $\rho(y)$ ist + Variable, die Abbildung $\rho:Def(\rho)\rightarrow\{z|z\ Variable\}$ ist + invertierbar (durch $\tau_2$) und damit injektiv. + + \subsubsection{Unifikationsalgorithmus}\label{unifikationsalgorithmus} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + Eingabe: Paar$(\alpha,\beta)$ gleichungsfreier Atomformeln $\sigma:=$ + Substitution mit $Def(\sigma)=\varnothing$ (d.h. Identität) + \item + while $\alpha\sigma\not =\beta\sigma$ do + \item + Suche die erste Position, an der sich $\alpha\sigma$ und $\beta\sigma$ + unterscheiden + \item + if keines der beiden Symbole an dieser Position ist eine Variable + \item + then stoppe mit ``nicht unifizierbar'' + \item + else sei $x$ die Variable und $t$ der Term in der anderen Atomformel + (möglicherweise auch eine Variable) + + \begin{itemize} + \item + if $x$ kommt in $t$ vor + \item + then stoppe mit ``nicht unifizierbar'' + \item + else $\sigma:=\sigma[x:=t]$ + \end{itemize} + \item + endwhile + \item + Ausgabe: $\sigma$ + \end{itemize} + + \begin{quote} + Satz + + \begin{itemize} + \item + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \item + Der Unifikationsalgorithmus terminiert für jede Eingabe. + \end{enumerate} + \item + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \setcounter{enumi}{1} + \item + Wenn die Eingabe nicht unifizierbar ist, so terminiert der + Unifikationsalgorithmus mit der Ausgabe ``nicht unifizierbar''. + \end{enumerate} + \item + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \setcounter{enumi}{2} + \item + Wenn die Eingabe $(\alpha,\beta)$ unifizierbar ist, dann findet der + Unifikationsalgorithmus einen allgemeinsten Unifikator von $\alpha$ + und $\beta$. + \end{enumerate} + \end{itemize} + \end{quote} + + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \setcounter{enumi}{2} + \itemsep1pt\parskip0pt\parsep0pt + \item + besagt insbesondere, daß zwei unifizierbare gleichungsfreie + Atomformeln (wenigstens) einen allgemeinsten Unifikator haben. Nach + dem Lemma oben haben sie also genau einen allgemeinsten Unifikator + (bis auf Umbenennung der Variablen). + \end{enumerate} + + Die drei Teilaussagen werden in getrennten Lemmata bewiesen werden. + + \begin{quote} + Lemma (A) Der Unifikationsalgorithmus terminiert für jede + Eingabe($\alpha$, $\beta$). + \end{quote} + + Beweis: Wir zeigen, daß die Anzahl der in $\alpha\sigma$ oder + $\beta\sigma$ vorkommenden Variablen in jedem Durchlauf der + while-Schleife kleiner wird. Betrachte hierzu einen Durchlauf durch die + while-Schleife. Falls der Algorithmus in diesem Durchlauf nicht + terminiert, so wird $\sigma$ auf $\sigma[x:=t]$ gesetzt. Hierbei kommt + $x$ in $\alpha\sigma$ oder in $\beta\sigma$ vor und der Term $t$ enthält + $x$ nicht. Also kommt $x$ weder in $\alpha\sigma[x:=t]$ noch in + $\beta\sigma[x:=t]$ vor. + + \begin{quote} + Lemma (B) Wenn die Eingabe nicht unifizierbar ist, so terminiert der + Unifikationsalgorithmus mit der Ausgabe ``nicht unifizierbar''. + \end{quote} + + Beweis: Sei die Eingabe $(\alpha,\beta)$ nicht unifizierbar. Falls die + Bedingung $\alpha\sigma\not=\beta\sigma$ der while-Schleife irgendwann + verletzt wäre, so wäre $(\alpha,\beta)$ doch unifizierbar (denn $\sigma$ + wäre ja ein Unifikator). Da nach Lemma (A) der Algorithmus bei Eingabe + $(\alpha,\beta)$ terminiert, muss schließlich ``nicht unifizierbar'' + ausgegeben werden. + + \begin{quote} + Lemma (C1) Sei $\sigma'$ ein Unifikator der Eingabe $(\alpha,\beta)$, so + dass keine Variable aus $\alpha$ oder $\beta$ auch in einem Term aus + $\{y\sigma'|y\in Def(\sigma')\}$ vorkommt. Dann terminiert der + Unifikationsalgorithmus erfolgreich und gibt einen Unifikator $\sigma$ + von $\alpha$ und $\beta$ aus. Außerdem gibt es eine Substitution $\tau$ + mit $\sigma'=\sigma\tau$. + \end{quote} + + Beweis: - Sei $N\in\mathbb{N}$ die Anzahl der Durchläufe der + while-Schleife (ein solches $N$ existiert, da der Algorithmus nach Lemma + (A) terminiert). - Sei $\sigma_0$ Substitution mit + $Def(\sigma_0) =\varnothing$, d.h. die Identität. Für $1\leq i\leq N$ + sei $\sigma_i$ die nach dem $i$-ten Durchlauf der while-Schleife + berechnete Substitution $\sigma$. - Für $1\leq i\leq N$ sei $x_i$ die im + $i$-ten Durchlauf behandelte Variable $x$ und $t_i$ der entsprechende + Term $t$. - Für $0\leq i\leq N$ sei $\tau_i$ die Substitution mit + $\tau_i(x)=\sigma'(x)$ für alle + $x\in Def(\tau_i) =Def(\sigma')\backslash\{x_1,x_2,...,x_i\}$. + + Behauptung: 1. Für alle $0\leq i\leq N$ gilt $\sigma'=\sigma_i\tau_i$. + 2. Im $i$-ten Durchlauf durch die while-Schleife $(1\leq i\leq N)$ + terminiert der Algorithmus entweder erfolgreich (und gibt die + Substitution $\sigma_N$ aus) oder der Algorithmus betritt die beiden + else-Zweige. 3. Für alle $0\leq i\leq N$ enthalten + $\{\alpha\sigma_i,\beta\sigma_i\}$ und $T_i=\{y\tau_i|y\in Def(\tau_i)\}$ + keine gemeinsamen Variablen. + + Aus dieser Behauptung folgt tatsächlich die Aussage des Lemmas: - Nach + (2) terminiert der Algorithmus erfolgreich mit der Substitution + $\sigma_N$. Daher gilt aber $\alpha\sigma_N=\beta\sigma_N$, d.h. + $\sigma_N$ ist ein Unifikator. - Nach (1) gibt es auch eine Substitution + $\tau_n$ mit $\sigma'=\sigma_N\tau_n$. + + \begin{quote} + Lemma (C) Sei die Eingabe $(\alpha,\beta)$ unifizierbar. Dann terminiert + der Unifikationsalgorithmus erfolgreich und gibt einen allgemeinsten + Unifikator $\sigma$ von $\alpha$ und $\beta$ aus. + \end{quote} + + Beweis: Sei $\sigma'$ ein beliebiger Unifikator von $\alpha$ und + $\beta$. Sei $Y=\{y_1,y_2,... ,y_n\}$ die Menge aller Variablen, die in + $\{y\sigma'|y\in Def(\sigma')\}$ vorkommen. Sei $Z=\{z_1,z_2,...,z_n\}$ + eine Menge von Variablen, die weder in $\alpha$ noch in $\beta$ + vorkommen. Sei $\rho$ die Variablenumbenennung mit + $Def(\rho)=Y\cup Z,\rho(y_i) =z_i$ und $\rho(z_i)=y_i$ für alle + $1\leq i\leq n$. Dann ist auch $\sigma'\rho$ ein Unifikator von $\alpha$ + und $\beta$ und keine Variable aus $\alpha$ oder $\beta$ kommt in einem + der Terme aus $\{y\sigma'\rho|y\in Def(\sigma')\}$ vor. Nach Lemma (C1) + terminiert der Unifikationsalgorithmus erfolgreich mit einem Unifikator + $\sigma$ von $\alpha$ und $\beta$, so dass es eine Substitution $\tau$ + gibt mit $\sigma'\rho=\sigma\tau$. Also gilt + $\sigma'=\sigma(\tau\rho^{-1})$. Da $\sigma'$ ein beliebiger Unifikator + von $\alpha$ und $\beta$ war und da die Ausgabe $\sigma$ des Algorithmus + nicht von $\sigma'$ abhängt, ist $\sigma$ also ein allgemeinster + Unifikator. + + \begin{quote} + Satz + + \begin{itemize} + \item + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \item + Der Unifikationsalgorithmus terminiert für jede Eingabe. + \end{enumerate} + \item + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \setcounter{enumi}{1} + \item + Wenn die Eingabe nicht unifizierbar ist, so terminiert der + Unifikationsalgorithmus mit der Ausgabe ``nicht unifizierbar''. + \end{enumerate} + \item + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \setcounter{enumi}{2} + \item + Wenn die Eingabe $(\alpha,\beta)$ unifizierbar ist, dann findet der + Unifikationsalgorithmus immer einen allgemeinsten Unifikator von + $\alpha$ und $\beta$. + \end{enumerate} + \end{itemize} + \end{quote} + + \begin{enumerate} + \def\labelenumi{(\Alph{enumi})} + \setcounter{enumi}{2} + \itemsep1pt\parskip0pt\parsep0pt + \item + besagt insbesondere, daß zwei unifizierbare gleichungsfreie + Atomformeln(wenigstens) einen allgemeinsten Unifikator haben. Damit + haben sie aber genau einen allgemeinsten Unifikator (bis auf + Umbenennung der Variablen). + \end{enumerate} + + \subsection{Prädikatenlogische + SLD-Resolution}\label{pruxe4dikatenlogische-sld-resolution} + + Erinnerung - Eine Horn-Klausel der Prädikatenlogik ist eine Aussage der + Form + $\forall x_1 \forall x_2... \forall x_n ((\lnot\bot \wedge\alpha_1 \wedge\alpha_2 \wedge...\wedge\alpha_m)\rightarrow\beta)=\Psi$ + mit $m\geq 0$, atomaren Formeln $\alpha_1,...,\alpha_m$ und $\beta$ + atomare Formel oder $\bot$. Sie ist definit, wenn $\beta\not =\bot$. - + $E(\varphi) =\{\Psi[x_1 :=t_1 ][x_2 :=t_2 ]...[x_n:=tn]|t_1 ,t_2 ,...,t_n\in D(\sigma)\}$ + - Eine Horn-Klausel der Aussagenlogik ist eine Formel der Form + $(\lnot\bot\wedge q_1 \wedge q_2 \wedge... \wedge q_m)\rightarrow r$ mit + $m\geq 0$, atomaren Formeln $q_1,q_2,...,q_m,r$ atomare Formel oder + $\bot$. + + Schreib- und Sprechweise: Für die Horn-Klausel der Prädikatenlogik + $\forall x_1...\forall x_n(\lnot\bot \wedge \alpha_1 \wedge \alpha_2 \wedge...\wedge \alpha_m)\rightarrow\beta$ + schreiben wir kürzer + $\{\alpha_1,\alpha_2,...,\alpha_m\}\rightarrow\beta$. insbes. + $\varnothing\rightarrow\beta$ für + $\forall x_1...\forall x_n(\lnot\bot\rightarrow\beta)$ + + Erinnerung: Sei $\Gamma$ eine Menge von Horn-Klauseln der Aussagenlogik. + Eine aussagenlogische SLD-Resolution aus $\Gamma$ ist eine Folge + $(M_0 \rightarrow\bot,M_1 \rightarrow\bot,...,M_m\rightarrow\bot)$ von + Hornklauseln mit - $(M_0\rightarrow\bot)\in\Gamma$ und - für alle + $0\leq n +goal + < Frage ohne "?-" einfügen> +\end{verbatim} + + \begin{enumerate} + \setcounter{enumi}{1} + \itemsep1pt\parskip0pt\parsep0pt + \item + Beispiel 2 (BSP2.PRO) + \end{enumerate} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + Kollegen Meier und Müller arbeiten im Raum 1, Kollege Otto im Raum 2 + und Kollege Kraus im Raum 3. + \item + arbeitet\_in(meier,raum\_1). + \item + arbeitet\_in(mueller,raum\_1). + \item + arbeitet\_in(otto,raum\_2). + \item + arbeitet\_in(kraus,raum\_3). + \item + Netzanschlüsse gibt es in den Räumen 2 und 3. + \item + anschluss\_in(raum\_2). + \item + anschluss\_in(raum\_3). + \item + Ein Kollege ist erreichbar, wenn er in einem Raum mit Netzanschluss + arbeitet. + \item + erreichbar(K) :- arbeitet\_in(K,R),anschluss\_in(R). + \item + 2 Kollegen können Daten austauschen, wenn sie im gleichen Raum + arbeiten oder beide erreichbar sind. + \item + koennen\_daten\_austauschen(K1,K2) :- + arbeitet\_in(K1,R),arbeitet\_in(K2,R). + \item + koennen\_daten\_austauschen(K1,K2) :- erreichbar(K1),erreichbar(K2). + \end{itemize} + + Deklarationsteil + + \begin{verbatim} +domains + person, raum: symbol +predicates + arbeitet_in(person,raum) + ansluss_in(raum) + erreichbar(person) + koennen_daten_austauschen(person,person) +clauses + ... +goal + ... +\end{verbatim} + + \paragraph{Verarbeitung Logischer + Programme}\label{verarbeitung-logischer-programme} + + \subparagraph{Veranschaulichung ohne + Unifikation}\label{veranschaulichung-ohne-unifikation} + + + \includegraphics[width=\linewidth]{Assets/Logik-prolog-ohne-unifikation.png} + + Tiefensuche mit Backtrack: Es werden anwendbare Klauseln für das erste + Teilziel gesucht. Gibt es \ldots{} - \ldots{} genau eine, so wird das 1. + Teilziel durch deren Körper ersetzt. - \ldots{} mehrere, so wird das + aktuelle Ziel inklusive alternativ anwendbarer Klauseln im + Backtrack-Keller abgelegt und die am weitesten oben stehende Klausel + angewandt. - \ldots{} keine (mehr), so wird mit dem auf dem + Backtrack-Keller liegendem Ziel die Bearbeitung fortgesetzt. + + Dies geschieht solange, bis - das aktuelle Ziel leer ist oder - keine + Klausel (mehr) anwendbar ist und der Backtrack-Keller leer ist. + + \subparagraph{Veranschaulichung mit + Unifikation}\label{veranschaulichung-mit-unifikation} + + + \includegraphics[width=\linewidth]{Assets/Logik-prolog-mit-unifikation.png} + + Zusätzliche Markierung der Kanten mit der Variablenersetzung (dem + Unifikator). + + \subsubsection{PROLOG aus prozeduraler + Sicht}\label{prolog-aus-prozeduraler-sicht} + + Beispiel: die ``Hackordnung'' 1. chef\_von(mueller,mayer). 2. + chef\_von(mayer,otto). 3. chef\_von(otto,walter). 4. + chef\_von(walter,schulze). 5. weisungsrecht(X,Y) :- chef\_von(X,Y). 6. + weisungsrecht(X,Y) :- chef\_von(X,Z), weisungsrecht(Z,Y). + + \begin{quote} + Deklarative Interpretation In einem Objektbereich + $I=\{mueller, mayer, schulze, ...\}$ bildet das Prädikat + $weisungsrecht(X,Y)$ $[X,Y]$ auf wahr ab, gdw. - das Prädikat + $chef_von(X,Y)$ das Paar $[X,Y]$ auf wahr abbildet oder - es ein + $Z\in I$ gibt, so dass - das Prädikat $chef_von(X,Z)$ das Paar $[X,Z]$ + auf wahr abbildet und - das Prädikat $weisungsrecht(Z,Y)$ das Paar + $[Z,Y]$ auf wahr abbildet. + \end{quote} + + \begin{quote} + Prozedurale Interpretation Die Prozedur $weisungsrecht(X,Y)$ wird + abgearbeitet, indem 1. die Unterprozedur $chef_von(X,Y)$ abgearbeitet + wird. Im Erfolgsfall ist die Abarbeitung beendet; anderenfalls werden 2. + die Unterprozeduren $chef_von(X,Z)$ und $weisungsrecht(Z,Y)$ + abgearbeitet; indem systematisch Prozedurvarianten beider + Unterprozeduren aufgerufen werden.Dies geschieht bis zum Erfolgsfall + oder erfolgloser erschöpfender Suche. + \end{quote} + + \begin{tabular}{ll} + deklarative Interpretation & prozedurale Interpretation \\\hline + Prädikat & Prozedur \\ + Ziel & Prozeduraufruf \\ + Teilziel & Unterprozedur \\ + Klauseln mit gleichem Kopfprädikat & Prozedur-varianten \\ + Klauselkopf & Prozedurkopf \\ + Klauselkörper & Prozedurrumpf \\ + \end{tabular} + + Die Gratwanderung zwischen Wünschenswertem und technisch Machbarem + erfordert mitunter ``Prozedurales Mitdenken'', um 1. eine gewünschte + Reihenfolge konstruktiver Lösungen zu erzwingen, 2. nicht terminierende + (aber - deklarativ, d.h. logisch interpretiert - völlig korrekte) + Programme zu vermeiden, 3. seiteneffektbehaftete Prädikate sinnvoll + einzusetzen, 4. (laufzeit-) effizienter zu programmieren und 5. das + Suchverfahren gezielt zu manipulieren. + + Programm inkl. Deklarationsteil (BSP3.PRO) + + \begin{verbatim} +domains + person = symbol +predicates + chef_von(person,person) + weisungsrecht(person,person) +clauses + chef_von(mueller,mayer). + chef_von(mayer,otto). + chef_von(otto,walter). + chef_von(walter,schulze). + weisungsrecht(X,Y) :- chef_von(X,Y). + weisungsrecht(X,Y) :- chef_von(X,Z), weisungsrecht(Z,Y). +goal + weisungsrecht(Wer,Wem). +\end{verbatim} + + Prädikate zur Steuerung der Suche nach einer Folge von + Resolutionsschritten! + + !(cut) Das Prädikat $!/0$ ist stets wahr. In Klauselkörpern eingefügt + verhindert es ein Backtrack der hinter $!/0$ stehenden Teilziele zu den + vor $!/0$ stehenden Teilzielen sowie zu alternativen Klauseln des + gleichen Kopfprädikats. Die Verarbeitung von $!/0$ schneidet demnach + alle vor der Verarbeitung verbliebenen Lösungswege betreffenden Prozedur + ab. + + Prädikate zur Steuerung der Suche: $!/0$ + \includegraphics[width=\linewidth]{Assets/Logik-prädikate-suche.png} + + Prädikate zur Steuerung der Suche nach einer Folge von + Resolutionsschritten \textbf{fail} Das Prädikat $fail/0$ ist stets + falsch. In Klauselkörpern eingefügt löst es ein Backtrack aus bzw. führt + zum Misserfolg, falls der Backtrack-Keller leer ist, d.h. falls es keine + verbleibenden Lösungswege (mehr) gibt. + \includegraphics[width=\linewidth]{Assets/Logik-prädikate-suche-fail.png} + \includegraphics[width=\linewidth]{Assets/Logik-prädikate-suche-fail-2.png} + + \subsubsection{Listen und rekursive + Problemlösungsstrategien}\label{listen-und-rekursive-problemluxf6sungsstrategien} + + Listen 1. $[]$ ist eine Liste. 2. Wenn $T$ ein Term und $L$ eine Liste + ist, dann ist 1. $[T|L]$ eine Liste. 2. $T.L$ eine Liste. + (ungebräuchlich) 3. $.(T,L)$ eine Liste. (ungebräuchlich) Das erste + Element $T$ heißt Listenkopf, $L$ heißt Listenkörper oder Restliste. 3. + Wenn $t_1, ... ,t_n$ Terme sind, so ist $[t_1,...,t_n]$ eine Liste. 4. + Weitere Notationsformen von Listen gibt es nicht. + + Listen als kompakte Wissensrepräsentation: ein bekanntes Beispiel + (BSP5.PRO) - arbeiten\_in({[}meier, mueller{]}, raum\_1). - + arbeitet\_in(meier, raum\_1). - arbeitet\_in(mueller, raum\_1). - + arbeitet\_in(otto, raum\_2). - arbeiten\_in({[}otto{]}, raum\_2 ). - + arbeitet\_in(kraus, raum\_3). - arbeiten\_in({[}kraus{]}, raum\_3 ). - + anschluesse\_in({[}raum\_2, raum\_3{]}). - anschluss\_in(raum\_2). - + anschluss\_in(raum\_3). + + \textbf{Rekursion} in der Logischen Programmierung Eine Prozedur heißt + (direkt) rekursiv, wenn in mindestens einem der Klauselkörper ihrer + Klauseln ein erneuter Aufruf des Kopfprädikates erfolgt. Ist der + Selbstaufruf die letzte Atomformel des Klauselkörpers der letzten + Klausel dieser Prozedur - bzw. wird er es durch vorheriges + ``Abschneiden'' nachfolgender Klauseln mit dem Prädikat $!/0$ - , so + spricht man von Rechtsrekursion ; anderenfalls von Linksrekursion. Eine + Prozedur heißt indirekt rekursiv, wenn bei der Abarbeitung ihres + Aufrufes ein erneuter Aufruf derselben Prozedur erfolgt. + + Wissensverarbeitung mit Listen: (BSP5.PRO) - erreichbar(K) :- + arbeitet\_in(K,R), anschluss\_in(R). - erreichbar(K) :- + anschluesse\_in(Rs), member(R, Rs), arbeiten\_in(Ks, R), member(K, Ks). + - koennen\_daten\_austauschen(K1,K2) :- + arbeitet\_in(K1,R),arbeitet\_in(K2,R). - + koennen\_daten\_austauschen(K1,K2) :- + arbeiten\_in(Ks,\emph{),member(K1,Ks), member(K2,Ks). - + koennen}daten\_austauschen(K1,K2) :- erreichbar(K1),erreichbar(K2). - + koennen\_daten\_austauschen(K1,K2) :- erreichbar(K1),erreichbar(K2). + + BSP5.PRO + + \begin{verbatim} +domains + person, raum = symbol + raeume = raum* + personen = person* +predicates + arbeiten_in(personen, raum) + anschluesse_in(raeume) + erreichbar(person) + koennen_daten_austauschen(person,person) + member(person,personen) + member(raum,raeume) +clauses + ... (siehe oben) + member(E,[E|_]). + member(E,[_|R]) :- member(E,R). +goal + erreichbar(Wer). +\end{verbatim} + + \textbf{Unifikation 2er Listen} 1. Zwei leere Listen sind (als + identische Konstanten aufzufassen und daher) miteinander unifizierbar. + 1. Zwei nichtleere Listen $[K_1|R_1]$ und $[K_2|R_2]$ sind miteinander + unifizierbar, wenn ihre Köpfe ($K_1$ und $K_2$) und ihre Restlisten + ($R_1$ und $R_2$) jeweils miteinander unifizierbar sind. 3. Eine Liste + $L$ und eine Variable $X$ sind miteinander unifizierbar, wenn die + Variable selbst nicht in der Liste enthalten ist. Die Variable $X$ wird + bei erfolgreicher Unifikation mit der Liste $L$ instanziert: $X:=L$. + + \textbf{Differenzlisten:} eine intuitive Erklärung Eine Differenzliste + $L_1 - L_2$ besteht aus zwei Listen $L_1$ und $L_2$ und wird im + allgemeinen als $[L_1,L_2]$ oder (bei vorheriger Definition eines pre- + bzw. infix notierten Funktionssymbols -/2) als $-(L_1,L_2)$ bzw. + $L_1-L_2$ notiert. + + Sie wird (vom Programmierer, nicht vom PROLOG-System!) als eine Liste + interpretiert, deren Elemente sich aus denen von $L_1$ abzüglich derer + von $L_2$ ergeben. Differenzlisten verwendet man typischerweise, wenn + häufig Operationen am Ende von Listen vorzunehmen sind. + + Eine Definition 1. Die Differenz aus einer leeren Liste und einer + (beliebigen) Liste ist die leere Liste: $[] - L = []$ 2. Die Differenz + aus einer Liste $[E|R]$ und der Liste $L$, welche $E$ enthält, ist die + Liste $D$, wenn die Differenz aus $R$ und $L$ (abzügl. $E$) die Liste + $D$ ist: $[E|R]-L = D$, wenn $E\in L$ und $R-(L-[E]) = D$ 3. Die + Differenz aus einer Liste $[E|R]$ und einer Liste $L$, welche $E$ nicht + enthält, ist die Liste $[E|D]$, wenn die Differenz aus $R$ und $L$ die + Liste $D$ ist: $[E|R] - L = [E|D]$, wenn $E\in L$ und $R-L=D$ + + Differenzlisten: Ein Interpreter + $interpret(Differenzliste,Interpretation)$ (BSP6.PRO) 1. + $interpret([[],_],[]).$ 2. + $interpret([[E|R],L] , D ) :- loesche(E , L, L1),! , interpret( [ R , L1 ] , D ).$ + 3. $interpret([[E|R],L] , [E|D] ) :- interpret([R,L],D).$ 4. + $loesche(E, [E|R], R) :-!.$ 5. + $loesche(E, [K|R], [K|L]) :- loesche(E,R,L).$ + + \subsubsection{Prolog-Fallen}\label{prolog-fallen} + + \paragraph{Nicht terminierende + Programme}\label{nicht-terminierende-programme} + + Ursache: ``ungeschickt'' formulierte (direkte oder indirekte) Rekursion + + \subparagraph{Alternierende + Zielklauseln}\label{alternierende-zielklauseln} + + Ein aktuelles Ziel wiederholt sich und die Suche nach einer Folge von + Resolutionsschritten endet nie: 1. $liegt_auf(X,Y) :- liegt_unter(Y,X).$ + 2. $liegt_unter(X,Y) :- liegt_auf(Y,X).$ - + $?- liegt_auf( skript, pult ).$ - logisch korrekte Antwort: nein - + tatsächliche Antwort: keine Logische Programmierung + + oder die Suche nach Resolutionsschritten endet mit einem Überlauf des + Backtrack-Kellers: (BSP8.PRO) 1. $liegt_auf(X,Y) :- liegt_unter(Y,X).$ + 2. $liegt_auf( skript , pult ).$ 3. + $liegt_unter(X,Y) :- liegt_auf(Y,X).$ - $?- liegt_auf( skript , pult ).$ + - logisch korrekte Antwort: ja - tatsächliche Antwort: keine + + \subparagraph{Expandierende + Zielklauseln}\label{expandierende-zielklauseln} + + Das erste Teilziel wird in jeden Resolutionsschritt durch mehrere neue + Teilziele ersetzt; die Suche endet mit einem Speicherüberlauf: + (BSP9.PRO) 1. $liegt_auf( notebook , pult ).$ 2. + $liegt_auf( skript , notebook ).$ 3. + $liegt_auf(X,Y) :- liegt_auf(X,Z), liegt_auf(Z,Y).$ - + $?- liegt_auf( handy , skript ).$ - logisch korrekte Antwort: nein - + tatsächliche Antwort: keine + + Auch dieses Beispiel lässt sich so erweitern, dass die Hypothese + offensichtlich aus der Wissensbasis folgt, die Umsetzung der + Resolutionsmethode aber die Vollständigkeit zerstört: 1. + $liegt_auf( notebook , pult ).$ 2. $liegt_auf( skript , notebook ).$ 3. + $liegt_auf(X,Y) :- liegt_auf(X,Z), liegt_auf(Z,Y).$ 4. + $liegt_auf( handy , skript ).$ - $?- liegt_auf( handy , pult ).$ - + logisch korrekte Antwort: ja - tatsächliche Antwort: keine + + Auch dieses Beispiel zeigt, dass das Suchverfahren ``Tiefensuche mit + Backtrack'' die Vollständigkeit des Inferenzverfahrens zerstört. + + \paragraph{Metalogische Prädikate und konstruktive + Lösungen}\label{metalogische-pruxe4dikate-und-konstruktive-luxf6sungen} + + Das Prädikat $not/1$ hat eine Aussage als Argument und ist somit eine + Aussage über eine Aussage, also metalogisch. I.allg. ist $not/1$ + vordefiniert, kann aber mit Hilfe von $call/1$ definiert werden. + $call/1$ hat Erfolg, wenn sein Argument - als Ziel interpretiert - + Erfolg hat. + + Beispiel (BSP10.PRO): 1. $fleissig(horst).$ 2. $fleissig(martin).$ 3. + $faul(X) :- not( fleissig(X) ).$ 4. $not(X) :- call(X), !, fail.$ 5. + $not( _ ).$ - $?- faul(horst).$ Antwort: nein - $?- faul(alex).$ + Antwort: ja - $?- faul(Wer).$ Antwort: nein + + Widerspruch \ldots{} und Beweis der Unvollständigkeit durch Metalogik + + \subsubsection{Typische Problemklassen für die Anwendung der Logischen + Programmierung}\label{typische-problemklassen-fuxfcr-die-anwendung-der-logischen-programmierung} + + \paragraph{Rekursive + Problemlösungsstrategien}\label{rekursive-problemluxf6sungsstrategien} + + \begin{quote} + Botschaft 1 Man muss ein Problem nicht in allen Ebenen überblicken, um + eine Lösungsverfahren zu programmieren. Es genügt die Einsicht, 1. wie + man aus der Lösung eines einfacheren Problems die Lösung des präsenten + Problems macht und 2. wie es im Trivialfall zu lösen ist. + \end{quote} + + \textbf{Türme von Hanoi} Es sind N Scheiben von der linken Säule auf die + mittlere Säule zu transportieren, wobei die rechte Säule als + Zwischenablage genutzt wird. Regeln: 1. Es darf jeweils nur eine Scheibe + transportiert werden. 2. Die Scheiben müssen mit fallendem Durchmesser + übereinander abgelegt werden. + + (doppelt) rekursive Lösungsstrategie: - $N = 0:$ Das Problem ist gelöst. + - $N > 0:$ 1. Man löse das Problem für N-Scheiben, die von der + Start-Säule zur Hilfs-Säule zu transportieren sind. 2. Man lege eine + Scheibe von der Start- zur Ziel-Säule. 3. Man löse das Problem für + N-Scheiben, die von der Hilfs-Säule zur Ziel-Säule zu transportieren + sind. + + Prädikate - $hanoi(N)$ löst das Problem für N Scheiben - + $verlege(N,Start,Ziel,Hilf)$ verlegt N Scheiben von Start nach Ziel + unter Nutzung von Hilf als Ablage + + Die Regeln zur Kodierung der Strategie (BSP11.PRO) - + $hanoi( N ) :- verlege( N , s1 , s2 , s3 ).$ - + $verlege( 0 , \_ , \_ , \_ ).$ - $verlege( N , S , Z , H ) :-$ - + $N1 = N - 1,$ - $verlege( N1 , S , H , Z ),$ - + $write("Scheibe von ", S," nach ", Z),$ - $verlege( N1 , H , Z , S ).$ + + \paragraph{Sprachverarbeitung mit + PROLOG}\label{sprachverarbeitung-mit-prolog} + + \begin{quote} + Botschaft 2 Wann immer man Objekte mit Mustern vergleicht, z.B. 1. eine + Struktur durch ``Auflegen von Schablonen'' identifiziert, 2. + Gemeinsamkeiten mehrerer Objekte identifiziert, d.h. ``eine Schablone + entwirft'' oder 3. ``gemeinsame Beispiele für mehrere Schablonen'' + sucht, mache man sich den Unifikations-Mechanismus zu nutzen. + \end{quote} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + Eine kontextfreie Grammatik (Chomsky-Typ 2) besteht aus + \end{itemize} + + \begin{enumerate} + \itemsep1pt\parskip0pt\parsep0pt + \item + einem Alphabet A, welches die terminalen (satzbildenden) Symbole + enthält + \item + einer Menge nichtterminaler (satzbeschreibender) Symbole N (= + Vokabular abzüglich des Alphabets: $N = V \backslash A$) + \item + einer Menge von Ableitungsregeln $R\subseteq N\times (N\cup A)^*$ + \item + dem Satzsymbol $S\in N$ + \end{enumerate} + + \begin{itemize} + \itemsep1pt\parskip0pt\parsep0pt + \item + \ldots{} und in PROLOG repräsentiert werden durch + \end{itemize} + + \begin{enumerate} + \itemsep1pt\parskip0pt\parsep0pt + \item + 1-elementige Listen, welche zu satzbildenden Listen komponiert werden: + $[der],[tisch],[liegt],...$ + \item + Namen, d.h. mit kleinem Buchstaben beginnende Zeichenfolgen: + $nebensatz,subjekt,attribut,...$ + \item + PROLOG-Regeln mit $l\in N$ im Kopf und $r\in(N\cup A)^*$ im Körper + \item + einen reservierten Namen: $satz$ + \end{enumerate} + + Ein Ableitungsbaum beschreibt die grammatische Struktur eines Satzes. + Seine Wurzel ist das Satzsymbol, seine Blätter in Hauptreihenfolge + bilden den Satz. + \includegraphics[width=\linewidth]{Assets/Logik-ableitungsbaum-beispiel.png} + + \begin{enumerate} + \itemsep1pt\parskip0pt\parsep0pt + \item + Alphabet + $ministerium, rektorat, problem, das, loest, ignoriert, verschaerft$ + \item + nichtterminale Symbole + $satz, subjekt, substantiv, artikel, praedikat,objekt$ + \item + Ableitungsregeln (in BACKUS-NAUR-Form) + + \begin{itemize} + \item + $satz ::= subjekt praedikat objekt$ + \item + $subjekt ::= artikel substantiv$ + \item + $objekt ::= artikel substantiv$ + \item + $substantiv ::= ministerium | rektorat | problem$ + \item + $artikel ::= das$ + \item + $praedikat ::= loest | ignoriert | verschaerft$ + \end{itemize} + \item + Satzsymbol $satz$ + \end{enumerate} + + Verketten einer Liste von Listen + + \begin{verbatim} +% die Liste ist leer +verkette( [ ] , [ ] ) . + +% das erste Element ist eine leere Liste +verkette( [ [ ] | Rest ] , L ) :- + verkette( Rest , L ). + +% das erste Element ist eine nichtleere Liste +verkette([ [K | R ] | Rest ] , [ K | L ] ) :- + verkette( [ R | Rest ] , L ).4 +\end{verbatim} + + \paragraph{Die ``Generate - and - Test'' + Strategie}\label{die-generate---and---test-strategie} + + \begin{quote} + Botschaft 3 Es ist mitunter leichter (oder überhaupt erst möglich), für + komplexe Probleme 1. eine potentielle Lösung zu ``erraten'' und dazu 2. + ein Verfahren zu entwickeln, welches diese Lösung auf Korrektheit + testet, als zielgerichtet die korrekte Lösung zu entwerfen. Hierbei kann + man den Backtrack-Mechanismus nutzen. + \end{quote} + + Strategie: Ein Prädikat $moegliche_loesung(L)$ generiert eine + potentielle Lösung, welche von einem Prädikat $korrekte_loesung(L)$ + geprüft wird: - Besteht $L$ diesen Korrektheitstest, ist eine Lösung + gefunden. - Fällt $L$ bei diesem Korrektheitstest durch, wird mit + Backtrack das Prädikat $moegliche_loesung(L)$ um eine alternative + potentielle Lösung ersucht. (vgl.: Lösen NP-vollständiger Probleme, + Entscheidung von Erfüllbarkeit) + + ein Beispiel: konfliktfreie Anordnung von $N$ Damen auf einem + $N\times N$ Schachbrett (BSP13.PRO) - eine Variante: Liste + strukturierter Terme - $[dame(Zeile,Spalte),...,dame(Zeile,Spalte)]$ - + $[dame(1,2), dame(2,4), dame(3,1), dame(4,3) ]$ - noch eine Variante: + Liste von Listen - $[[Zeile, Spalte] , ... , [Zeile,Spalte] ]$ - + $[ [1,2] , [2,4] , [3,1] , [4,3] ]$ - \ldots{} und noch eine (in die + Wissensdarstellung etwas ``natürliche'' Intelligenz investierende, den + Problemraum enorm einschränkende) Variante: Liste der Spaltenindizes - + $[ Spalte_zu_Zeile_1, ..., Spalte_zu_Zeile_N ]$ - $[ 2, 4, 1, 3 ]$ + + \paragraph{Heuristische + Problemlösungsmethoden}\label{heuristische-problemluxf6sungsmethoden} + + \begin{quote} + Botschaft 4 Heuristiken sind 1. eine Chance, auch solche Probleme einer + Lösung zuzuführen, für die man keinen (determinierten) + Lösungsalgorithmus kennt und 2. das klassische Einsatzgebiet zahlreicher + KI-Tools - auch der Logischen Programmierung. + \end{quote} + + Was ist eine Heuristik? Worin unterscheidet sich eine heuristische + Problemlösungsmethode von einem Lösungsalgorithmus? + + Heuristiken bewerten die Erfolgsaussichten alternativer + Problemlösungsschritte. Eine solche Bewertung kann sich z.B. ausdrücken + in - einer quantitativen Abschätzung der ``Entfernung'' zum gewünschten + Ziel oder der ``Kosten'' für das Erreichen des Ziels, - einer + quantitativen Abschätzung des Nutzens und/oder der Kosten der + alternativen nächsten Schritte, - eine Vorschrift zur Rangordnung der + Anwendung alternativer Schritte, z.B. durch Prioritäten oder gemäß einer + sequenziell abzuarbeitenden Checkliste. + + Ein Beispiel: Das Milchgeschäft meiner Großeltern in den 40er Jahren - + Der Milchhof liefert Milch in großen Kannen. - Kunden können Milch nur + in kleinen Mengen kaufen. - Es gibt nur 2 Sorten geeichter Schöpfgefäße; + sie fassen 0.75 Liter bzw. 1.25 Liter. - Eine Kundin wünscht einen Liter + Milch. 1. Wenn das große Gefäß leer ist, dann fülle es. 2. Wenn das + kleine Gefäß voll ist, dann leere es. 3. Wenn beides nicht zutrifft, + dann schütte so viel wie möglich vom großen in das kleine Gefäß. + + Prädikat $miss_ab(VolGr, VolKl, Ziel, InhGr, InhKl)$ mit - VolGr - + Volumen des großen Gefäßes - VolKl - Volumen des kleinen Gefäßes - Ziel + - die abzumessende (Ziel-) Menge - InhGr - der aktuelle Inhalt im großen + Gefäß - InhKl - der aktuelle Inhalt im kleinen Gefäß + + Beispiel-Problem: $?- miss_ab( 1.25 , 0.75 , 1 , 0 , 0 )4$ + + \paragraph{Pfadsuche in gerichteten + Graphen}\label{pfadsuche-in-gerichteten-graphen} + + \begin{quote} + Botschaft 5 1. Für die systematische Suche eines Pfades kann der + Suchprozess einer Folge von Resolutionsschritten genutzt werden. Man + muss den Suchprozess nicht selbst programmieren. 2. Für eine + heuristische Suche eines Pfades gilt Botschaft 4: Sie ist das klassische + Einsatzgebiet zahlreicher KI-Tools - auch der Logischen Programmierung. + \end{quote} + + Anwendungen - Handlungsplanung, z.B. - Suche einer Folge von + Bearbeitungsschritten für ein Produkt, eine Dienstleistung, einen + ``Bürokratischen Vorgang'' - Suche eines optimalen Transportweges in + einem Netzwerk von Straßen-, Bahn-, Flugverbindungen - Programmsynthese + = Handlungsplanung mit \ldots{} - \ldots{} Schnittstellen für die + Datenübergabe zwischen ``Handlungsschritten'' (= Prozeduraufrufen) und - + \ldots{} einem hierarchischen Prozedurkonzept, welches die + Konfigurierung von ``Programmbausteinen'' auf mehreren Hierarchie-Ebenen + + Ein Beispiel: Suche einer zeitoptimalen Flugverbindung (BSP15.PRO) - + Repräsentation als Faktenbasis $verbindung(Start,Zeit1,Ziel,Zeit2,Tag).$ + - Start - Ort des Starts - Zeit1 - Zeit des Starts - Ziel - Ort der + Landung - Zeit2 - Zeit der Landung - Tag - 0, falls Zeit1 und Zeit2 am + gleichen Tag und 1 ansonsten - möglich: - + $verbindung(fra,z(11,45),ptb,z(21,0),0).$ - + $verbindung(fra,z(11,15),atl,z(21,25),0).$ - + $verbindung(ptb,z(24,0),orl,z(2,14),1).$ - + $verbindung(atl,z(23,30),orl,z(0,54),1).$ + + In einer dynamischen Wissensbasis wird die bislang günstigste Verbindung + in Form eines Faktes + $guenstigste([ v(Von,Zeit1,Nach,Zeit2,Tag), ... ], Ankunftszeit, Tag ).$ + festgehalten und mit den eingebauten Prädikaten $assert()$ - zum + Einfügen des Faktes - und $retract ()$ - zum Entfernen des Faktes + - bei Bedarf aktualisiert. Zum Beispiel + $guenstigste([v(fra,z(11,45),ptb,z(21,00),0),v(ptb,z(24,0),orl,z(2,14),1)],z(2,14),1).$ + erklärt den Weg über Pittsburgh zum bislang günstigsten gefundenen Weg. + + \paragraph{``Logeleien'' als + Prolog-Wissensbasen}\label{logeleien-als-prolog-wissensbasen} + + \begin{quote} + Botschaft 6 1. ``Logeleien'' sind oft Aussagen über Belegungen von + Variablen mit endlichem Wertebereich, ergänzt um eine Frage zu einem + nicht explizit gegebenen Wert. 2. Dabei handelt es sich um Grunde um + eine Deduktionsaufgabe mit einer Hypothese zu einem mutmaßlichen Wert + der gesuchten Variablen. Deshalb ist es oft auch mit dem + ``Deduktionstool'' Prolog lösbar, denn Prolog tut im Grunde nichts + anderes als ein ziel-gerichtetes ``Durchprobieren'' legitimer + Deduktionsschritte im ``Generate - and - Test'' - Verfahren. + \end{quote} + + Beispiel das ``Zebra-Rätsel''(BSP16.PRO): 1. Es gibt fünf Häuser. 2. Der + Engländer wohnt im roten Haus. 3. Der Spanier hat einen Hund. 4. Kaffee + wird im grünen Haus getrunken. 5. Der Ukrainer trinkt Tee. 6. Das grüne + Haus ist (vom Betrachter aus gesehen) direkt rechts vom weißen Haus. 7. + Der Raucher von Atem-Gold-Zigaretten hält Schnecken als Haustiere. 8. + Die Zigaretten der Marke Kools werden im gelben Haus geraucht. 9. Milch + wird im mittleren Haus getrunken. 10. Der Norweger wohnt im ersten Haus. + 11. Der Mann, der Chesterfields raucht, wohnt neben dem Mann mit dem + Fuchs. 12. Die Marke Kools wird geraucht im Haus neben dem Haus mit dem + Pferd. 13. Der Lucky-Strike-Raucher trinkt am liebsten Orangensaft. 14. + Der Japaner raucht Zigaretten der Marke Parliament. 15. Der Norweger + wohnt neben dem blauen Haus. + + Jedes Haus ist in einer anderen Farbe gestrichen und jeder Bewohner hat + eine andere Nationalität, besitzt ein anderes Haustier, trinkt ein von + den anderen Bewohnern verschiedenes Getränk und raucht eine von den + anderen Bewohnern verschiedene Zigarettensorte. Fragen: - Wer trinkt + Wasser? - Wem gehört das Zebra? + + \begin{verbatim} +loesung(WT, ZB) :- + haeuser(H), nationen(N), getraenke(G), tiere(T), zigaretten(Z),aussagentest(H,N,G,T,Z), !, wassertrinker(N,G,WT), zebrabesitzer(N,T,ZB). +tiere(X) :- permutation([fuchs, hund, schnecke, pferd, zebra],X). +nationen([norweger|R]) :- permmutation([englaender, spanier, ukrainer, japaner], R). % erfüllt damit Aussage 10 +getraenke(X) :- permutation([kaffee, tee, milch, osaft, wasser], X), a9(X). % erfüllt damit Aussage 9 +zigaretten(X) :- permmutation([atemgold,kools,chesterfield, luckystrike, parliament], X). +haeuser(X) :- permutation([rot, gruen, weiss, gelb, blau], X), a6(X). +% parmutation/2, fuege_ein/3: siehe BSP13-PRO +wassertrinker([WT| _ ], [wasser| _ ], WT ) :- !. +wassertrinker([ _ |R1], [ _ |R2],WT) :- wassertrinker(R1, R2, WT). +zebrabesitzer([ZB| _ ], [zebra| _ ], ZB) :- !. +zebrabesitzer([ _ |R1], [ _ |R2],ZB) :- zebrabesitzer(R1, R2, ZB). +aussagentest(H,N,G,T,Z) :- + a2(H,N), a3(N,T), a4(H,G), a5(N,G), a7(Z,T), a8(H,Z), a11(Z,T), a12(Z,T),a13(Z,G), a14(N,Z), a15(H,N). + +a2([rot| _ ], [englaender| _ ]) :- ! +.a2([ _ |R1], [ _ |R2]) :- a2(R1, R2). +a3([spanier| _ ], [hund| _ ]) :- !. +a3([ _ |R1], [ _ |R2]) :- a3(R1, R2). +a4([gruen| _ ], [kaffee| _ ]) :- !. +a4([ _ |R1], [ _ |R2]) :- a4(R1, R2). +a5([ukrainer| _ ], [tee| _ ]) :- !. +a5([ _ |R1], [ _ |R2]) :- a5(R1, R2). +a6([weiss, gruen| _ ]) :- !. +a6([weiss| _ ]) :- !, fail.a6([ _ |R]) :- a6(R). +a7([atemgold| _ ], [schnecke| _ ]) :- !. +a7([ _ |R1], [ _ |R2]) :- a7(R1, R2). +a8([gelb| _ ], [kools| _ ]) :- !. +a8([ _ |R1], [ _ |R2]) :- a8(R1, R2). +a9([ _ , _ , milch, _ , _ ]). +a11([chesterfield| _ ], [ _ ,fuchs| _ ]) :-!. +a11([ _ , chesterfield| _ ], [fuchs| _ ]) :- !. +a11([ _ |R1], [ _ |R2]) :- a11(R1, R2). +a12([kools| _ ], [ _ , pferd| _ ]) :- !. +a12([ _ , kools| _ ], [pferd| _ ] ) :- !. +a12([ _ |R1], [ _ |R2]) :- a12(R1, R2). +a13([luckystrike| _ ], [osaft| _ ]) :- !. +a13([ _ |R1], [ _ |R2]) :- a13(R1, R2). +a14([japaner| _ ], [parliament| _ ]) :- !. +a14([ _ |R1], [ _ |R2]) :- a14(R1, R2). +%a15([blau| _ ], [ _, norweger| _ ]) :- !. +a15([ _ , blau| _ ], [norweger| _ ]) :- !. +%a15([ _ |R1], [ _ |R2]) :- a15(R1, R2). + +?- loesung(Wassertrinker, Zebrabesitzer). +\end{verbatim} + + Beispiel SUDOKU (BSP17.PRO): - Liste 9-elementliger Listen, die (von + links nach rechts) die Zeilen (von oben nach unten)repräsentieren - + Elemente einer jeden eine Zeile repräsentierenden Liste: - Ziffer, falls + dort im gegebenen Sudoku eine Ziffer steht - Anonyme Variable + andernfalls + + \paragraph{Tools für die formale + Logik}\label{tools-fuxfcr-die-formale-logik} + + \begin{quote} + Botschaft 7 Auch in der formalen Logik gibt es Deduktionsaufgaben, bei + der Variablenbelegungen gesucht sind, welche eine Aussage wahr machen: + 1. Meist geschieht das durch systematische Auswertung der Aussage, wozu + das Suchverfahren von Prolog genutzt werden kann. 2. Auch hier geht es + oft um gesuchte Werte für Variablen. Deshalb ist es oft auch mit dem + ``Deduktionstool'' Prolog lösbar, denn Prolog tut im Grunde nichts + anderes als ein ziel-gerichtetes ``Durchprobieren'' legitimer + Deduktionsschritte im ``Generate - and - Test'' - Verfahren. + \end{quote} + + Repräsentation von Aussagen als PROLOG-Term: - true, false: atom(true), + atom(false) - $A1\wedge A2$: und(A1,A2) - $A1\vee A2$: oder(A1,A2) - + $\lnot A$: nicht(A) - $A1\rightarrow A2$: wenndann(A1,A2) - + $A1\leftarrow A2$: dannwenn(A1,A2) - $A1\leftrightarrow A2$: gdw(A1,A2) + + Erfüllbarkeitstest: - + $?- erfuellbar(gdw(wenndann(nicht(oder(atom(false),atom(X))),atom(Y)), atom(Z))).$ + - X=true, Y=\_, Z=true ; steht für 2 Modelle (eines mit Y = true und + eines mit Y = false) - X=false, Y=true, Z=true + + Ketten von Konjunktionen und Disjunktionen als PROLOG-Listen: - + $A1\wedge A2\wedge ... \wedge An$: und verkettung({[}A1,A2, \ldots{}, + An{]}) - $A1\vee A2\vee ...\vee An$: oder verkettung({[}A1,A2, \ldots{}, + An{]}) + + Erfüllbarkeitstest: - $?- erfuellbar(undverkettung([true,X,Y,true]))$ - + X = true Y = true - $?- erfuellbar(oderverkettung([false,X,Y,false]))$ - + X = true Y = \emph{ - X = } Y = true + + Repräsentation von Termen als PROLOG-Term: - Wert: atom() - + $A1\wedge A2$: und(A1,A2) - $A1\vee A2$: oder(A1,A2) - $\lnot A$: + nicht(A) - $A1\rightarrow A2$: wenndann(A1,A2) - $A1\leftarrow A2$: + dannwenn(A1,A2) - $A1\leftrightarrow A2$: gdw(A1,A2) - + $A1\wedge A2\wedge ... \wedge An$: und verkettung({[}A1,A2, \ldots{}, + An{]}) - $A1\vee A2\vee ...\vee An$: oder verkettung({[}A1,A2, \ldots{}, + An{]}) + + Termauswertung: - + $?- hat_wert(und(atom(0.5),oder(atom(0.7),atom(0.3))),X).$ - X=0.5 + + Termauswertung unter Vorgabe des Wertebereiches: - + $?- hat_wert([0,0.3, 0.5, 0.7, 1], und(atom(X),oder(atom(0.5),atom(0.7))),Wert).$ + - X=0, Wert=0 - X=0.3, Wert=0.3 - X=0.5, Wert=0.5 - X=0.7, Wert=0.7 - + X=1, Wert=0.7 + +\end{multicols} +\end{document} \ No newline at end of file