Skip to main content
Top

2013 | Book

Logikkalküle in der Informatik

Wie wird Logik vom Rechner genutzt?

insite
SEARCH

About this book

Im Mittelpunkt steht das Spannungsverhältnis zwischen einerseits dem herkömmlichen Logikansatz mit Begriffen wie Signatur, Struktur, Wahrheitswert und andererseits dem eher dynamisch ausgerichteten Begriff des Kalküls, also zwischen Semantik und Syntax. Wie dieser Graben überwunden wird, wird für verschiedene auch nicht-klassische Logiken vorgeführt: Prädikatenlogik, modale, temporale, nichtmonotone, epistemische Logik und andere.

Dadurch wird insbesondere auch eine einführende Übersicht über Logiken gegeben, die an manchen Stellen der Informatik benötigt werden, zu deren Verständnis man sich aber kein ganzes spezielles Buch anschaffen möchte. Das Buch enthält einen einheitlichen Ansatz für verschiedene Logiken.

Table of Contents

Frontmatter
1. Einführung
Zusammenfassung
Was bedeutet Wissenschaft? Ganz wesentlich das Zusammenspiel von Theorie und Experiment. Im Rahmen einer Theorie werden die Fakten der alltäglichen Welt abstrakt modelliert, zumeist in der Sprache der Mathematik. Dort werden aus der Abstraktion bekannter Tatsachen mit mathematischer Präzision Schlüsse gezogen. Diese müssen wiederum an der Wirklichkeit überprüft werden, also durch ein Experiment. Es geht also um Dinge wie:
  • Erklärbarkeit von beobachteten Phänomenen der realen Welt durch Schlüsse der Mathematik,
  • Vorhersagbarkeit von Phänomenen der realen Welt durch logische Schlüsse der Mathematik.
Auch die Sprache ist ein gewichtiger Teilbereich der realen Welt. Auch auf die Sprache lässt sich daher das eben Gesagte anwenden. Als die entsprechende mathematische Abstraktion von Teilen der Sprache kann die Logik betrachtet werden. Wie bei jeder Sprache müssen auch bei der abstrakten Sprache der Logik sowohl ihre Syntax, also ihre formale Struktur, ihr „Satzbau“, als auch ihre Semantik, also die Bedeutung der einzelnen möglichen Sprachfragmente, untersucht werden. Unterschiedliche untersuchte Sprachfragmente führen zu unterschiedlichen Logiken.
In diesem Buch werden deshalb sehr unterschiedliche Logiken betrachtet, unter anderem:
  • Aussagenlogik,
  • Prädikatenlogik,
  • Modale Logik,
  • Temporale Logik,
  • Epistemische Logik.
Michael Schenke
2. Aussagenlogik
Zusammenfassung
Die Aussagenlogik ist die einfachste Form der Logik. Sie beschreibt einfachste Verknüpfungen zwischen als atomar („unteilbar“) angesehenen Elementaraussagen. Die praktische Bedeutung der AL in der Informatik kann gar nicht überschätzt werden. In jeder Programmiersprache kommen Boolesche Ausdrücke vor und auch beim Schaltkreisentwurf sind sie unentbehrlich. In der AL lassen sich künstliche, abstrahierte Situationen mit mathemathematischer Präzision analysieren. Der syntaktischen Frage, ob eine Formel wohlgeformt ist, steht die semantische Frage nach der Gültigkeit einer Formel gegenüber.
Soll die Gültigkeit einer Formel F geklärt werden, kann eine Wahrheitstafel benutzt werden. Das ist ein rein semantischer Ansatz. Bei einem alternativen und für gewöhnlich schnelleren Ansatz könnte man so vorgehen: Man forme F so lange syntaktisch durch vorher festgelegte Schlüsse um, bis man den gewünschten Schluss erhalten hat. Bei den Umformungen wird dabei nur auf die Form der Formeln geachtet. Es wird dabei eine endliche Menge von solchen Umformungsregeln, quasi ein „Werkzeugkasten“, benutzt. Ein solcher „Werkzeugkasten“ wird Kalkül genannt. Im Allgemeinen werden einige Anforderungen an einen Kalkül gestellt. Korrektheit bedeutet, dass alles, was im Kalkül abgeleitet werden kann, wahr ist. Vollständigkeit bedeutet, dass jede wahre Formel im Kalkül abgeleitet werden kann. Das allgemeine Ziel eines Kalküls ist es daher, vollständig und korrekt zu sein. Verschiedene Kalküle für die Aussagenlogik werden vorgestellt.
Michael Schenke
3. Prädikatenlogik
Zusammenfassung
Der offensichtlichste syntaktische Unterschied zwischen der AL und der PL, den beiden wichtigsten logischen Formalismen in der Informatik (und darüber hinaus), ist die Existenz zweier zusätzlicher Symbole, des Allquantors (" ) und des Existenzquantors ($ ), die sich auf zusätzliche Sprachfragmente beziehen. Eng damit verbunden ist der Unterschied, dass in der AL nichts über die Aussagen festgelegt wird. Diese werden dort durch Variablen repräsentiert, aber das Einzige, was man über Aussagen ausdrücken möchte, ist, ob sie wahr oder falsch sind.
Bei der PL wird dagegen eine detailliertere Analyse der Aussagen durchgeführt. Insbesondere wird dargestellt, über wen was ausgesagt wird. Ein ganz auffälliger Unterschied ist daher, dass es in der PL sowohl Formeln gibt, das heißt Aussagen, die wahr oder falsch sein können, als auch Terme; das sind Ausdrücke, die auf Individuen rekurrieren.
Es werden einige Themen mit Bezug zu Kalkülen in der PL angesprochen:
  • Der Prädikatenkalkül von Kurt Gödel.
  • Syllogismen werden als ein (unvollständiger) Kalkül der PL vorgestellt. Ihre Behandlung wird durch das „Spiel der Logik“ von Lewis Carroll verdeutlicht.
  • Es gibt eine Hinführung zum SLD-Kalkül.
Michael Schenke
4. Der SLD-Kalkül (Logik-Programmierung)
Zusammenfassung
Die bekannteste Programmiersprache, die Logik operationell benutzt, um gegebene Fragen direkt durch logische Schlüsse zu beantworten, ist Prolog. Dabei kann Prolog grob in zwei Teile unterteilt werden: in die logischen und die nichtlogischen Bestandteile. Die rein logischen Teile von „Prolog“, die „Logik-Programmierung“, betrachtet spezielle prädikatenlogische Formeln, die sogenannten „Horn-Klauseln“. Diese können durch einen Kalkül mit einer einzigen Regel, der SLD-Regel, recht intuitiv behandelt werden. Die Bedeutung von Logik-Programmen ist durch zwei Semantiken gegeben: die operationelle und die denotationelle.
Diese beiden Semantiken sind äquivalent, was letztlich bedeutet, dass der SLD-Kalkül vollständig und korrekt ist.
Michael Schenke
5. Hoaresche Logik
Zusammenfassung
Eine der wichtigsten Aufgaben der Informationsverarbeitung mit einem Rechner ist es, korrekte Programme zu erstellen. Der Begriff des „korrekten Programmes“ alleine ist dabei noch zu unscharf. Was soll es heißen, dass ein Programm „korrekt“ ist? Ein korrektes Programm muss eine Anforderung oder Spezifikation erfüllen. Um überhaupt über korrekte Programme reden zu können, braucht man also drei Dinge:
  • eine Programmiersprache, deren Elemente die korrekt geformten Programme sind,
  • eine Spezifikationssprache, deren Elemente die korrekt geformten Spezifikationen sind,
  • einen Korrektheitsbegriff, der entscheidet, ob ein gegebenes Programm eine gegebene Spezifikation erfüllt.
In dieser Allgemeinheit ist das Problem leider unentscheidbar. Das ist eine Folge des Satzes von Rice über Turing-Maschinen. In der HL wird die kalkülmäßige Verifikation von Programmen durch Hoaresche Tripel betrieben. Das sind Tripel {F} S {G}, für die gilt:
  • S ist ein einfaches Programm,
  • F, G sind Formeln der PL, die die Ein- und die daraus resultierende Ausgabe beschreiben.
Kalküle für Hoaresche Tripel mit kleinem Programmumfang werden vorgestellt.
Michael Schenke
6. Modale Logik
Zusammenfassung
Das vordergründige Ziel der modalen Logik ist die Erfassung und formale Behandlung von Sprachfragmenten wie „notwendigerweise“, „möglicherweise“, „zufälligerweise“. Solche werden im Rahmen der ML Modalitäten genannt. Durch diese Fragmente kann die modale Logik viele alltägliche Dinge oft sehr elegant, mathematisch präzise und nahe der normalen Umgangssprache ausdrücken. Die ML kann zur mathematischen Untermauerung auch anderer in den folgenden Kapiteln vorgestellter Logiken dienen.
Auf syntaktischer Ebene werden einige klassische Kalküle und dann die zugehörigen semantischen Formalismen, die Kripke – Semantiken, vorgestellt.
Ein herausragendes Ergebnis ist das Äquivalenztheorem, das besagt, dass die in der Praxis am weitesten verbreiteten Kalküle durch ganz fundamentale relationale Eigenschaften auch semantisch charakterisiert werden können.
Als eine spezielle mit Hilfe der ML gut erklärbare Logik erweist sich die Intuitionistische Logik. Das ist eine Form der Logik, in deren Hintergrund ein konstruktiver Ansatz steht. Eine Aussage gilt nur dann als gesichert, wenn diese nicht etwa nur durch einen indirekten Beweis gesichert sondern tatsächlich durch einen expliziten Beweis gegeben ist. Beispielsweise gilt der Satz vom ausgeschlossenen Dritten in der IL nicht.
Michael Schenke
7. Temporale Logik
Zusammenfassung
Die TL ist unentbehrlich für die formale Verifikation von Realzeitsystemen. Der modale Begriff der Notwendigkeit kann temporal als „immer“ interpretiert werden. Es geht dabei um logische Bezüge zwischen Aktionen, die zumeist auf eine spezielle Form der temporalen Quantifizierung hinauslaufen. Die TL ist dabei flexibler als eine reine Darstellung von Tatsachen durch die PL.
In diesem Kapitel werden mehrere Kalküle vorgestellt, von der klassischen einfachen Minimal Tense Logic bis hin zum modernen, sehr eleganten und aussagekräftigen Duration Calculus.
Auf der Ebene der Kripke-Semantiken für eine modale temporale Logik lassen sich die Zeitdomänen sehr gut an die praktischen Bedürfnisse anpassen:
  • als Äquivalenzrelation oder mit schwächeren relationalen Eigenschaften,
  • als totale Ordnung oder als verzweigende Zeit, wie in parallelen Systemen angemessen,
  • mit diskreter oder kontinuierlicher Zeit,
  • mit metrisierbarer Zeit, also mit genau messbaren Zeitangaben.
Michael Schenke
8. Epistemische Logik
Zusammenfassung
Bei der EL werden die Begriffe „Wissen“ und „Glauben“ von Aussagen mit Hilfe dafür geeigneter Modalitäten formalisiert.Die dann entstehenden Kalküle sind den klassischen Kalkülen der ML sehr ähnlich. Auch die semantische Behandlung durch Kripke-Strukturen lässt sich sehr gut von der ML auf die EL übertragen, wobei die Notwendigkeits-Modalität durch einen Operator ersetzt wird, der Wissen ausdrückt; und wie in der ML lassen sich dann das Äquivalenztheorem und weitere mächtige Äquivalenzsätze beweisen.
Die EL kann in der Informatik zum Beispiel zur formalen Beschreibung von Multi-Agentensystemen eingesetzt werden. Dann gibt es nicht nur einen Modaloperator wie in der ML sondern für jeden Agenten einen. Dadurch können die Konzepte von gemeinsamem und von verteiltem Wissen präzise mathematisiert werden. Bei der Behandlung kann man sich sehr weit gehend auf die Methoden der ML stützen.
Michael Schenke
9. Deontische Logik
Zusammenfassung
Die DL widmet sich der Erforschung sittlicher Normen, und zwar nicht nur in der Form einzelner Regeln, sondern als gesamtes System. Es geht also um Ausdrücke der Form „etwas ist obligatorisch“, „etwas ist erlaubt“ oder „etwas ist verboten“. Die Notwendigkeit sittlicher Beschränkungen in der Informatik und der Wissenschaft überhaupt ist evident.
Deren formale Behandlung im Rahmen einer rein kalkülmäßig betriebenen DL stößt aber auf große Schwierigkeiten. In den bisherigen formalen Systemen, etwa dem „Old System (OS)“ genannten System, wo erstmals formal modale Logik zur Grundlage der DL gemacht wurde, und dem späteren „Standardsystem der deontischen Logik (SDL)“, wurden gravierende Mängel und absurde Konsequenzen gefunden, die zeigen, wie schwierig eine konsistente formale Behandlung von Normen ist .
Ein möglicher aber sehr abstrakter Ausweg ist es, deontische Sätze nicht allgemeingültig zu formulieren sondern nur bezüglich einer nichtleeren Menge von Normen zu formulieren. Solche Mengen von Normen werden „Kodex“ genannt.
Michael Schenke
10. Nichtmonotone Logik
Zusammenfassung
Es geht bei der bei der nichtmonotonen Logik (NML) um ein in der künstlichen Intelligenz häufig auftretendes Phänomen: Es sei schon eine Menge von Fakten gesichert. Jetzt kommt neues Wissen hinzu. Die Menge des bekannten Wissens wächst dadurch aber nicht, sondern einige der scheinbar altbekannten Fakten werden ungültig. Ein Musterbeispiel dafür ist „Tweety, der KI-Vogel“: Ist über Tweety nur bekannt, dass er ein Vogel ist, lässt sich aus der Tatsache, dass Vögel im Allgemeinen fliegen können, schließen, dass Tweety fliegen kann. Wird Tweety dagegen näher untersucht und als Pinguin identifiziert, der dann nicht fliegen kann, so muss der Schluss auf die Flugfähigkeit von Tweety revidiert werden. Dieses Phänomen möchte man formal exakt behandeln können.
Bei den vorgestellten Truth Maintenance-Systemen wird zwischen sicherem und unsicherem Wissen unterschieden. Ein zulässiges Modell für eine Menge (zum Teil unsicherer) Begründungen darf nur durch Schlüsse fundiertes Wissen enthalten und muss alle Konsequenzen gültiger Begründungen umfassen. Solche Modelle müssen nicht unbedingt existieren, und sie sind für gewöhnlich auch nicht eindeutig.
Der hier vorgestellte JTMS-Algorithmus zeigt, wie aus einem zulässigen Modell bei Gewinnung neuer Fakten ein auch für die neue Situation zulässiges Modell konstruiert werden kann, falls ein solches existiert.
Michael Schenke
11. Default-Logiken
Zusammenfassung
Während bei Truth Maintenance-Systemen die nichtmonotone Ableitung im Vordergrund steht und nichtmonotone Regeln dort eher als Mittel zum Zweck eingesetzt werden, stellen die unsicheren Regeln, Default-Regeln oder einfach Defaults genannt, in der Default-Logik das Rückgrat des Geschehens dar. Sie zeichnen sich dabei dadurch aus, dass sie Ausnahmen zulassen und daher nicht ganz allgemein sondern nur typischerweise gelten. Sie gelten, solange nicht das Gegenteil explizit bewiesen worden ist.
Es geht um ein (unter Umständen unendliches) Verfahren zur Ansammlung von Konsequenzen, immer abwechselnd vermöge klassischer Deduktion und vermöge Defaults. Die Suche wird auf ein Fixpunktproblem reduziert, und man kann vieles benutzen, was aus verschiedenen Fixpunkttheorien bekannt ist. Ein unter Umständen endliches Verfahren zur Bestimmung der Konsequenzen kann die Erstellung von Prozessbäumen liefern.
Michael Schenke
12. Mathematische Grundlagen
Zusammenfassung
In diesem Kapitel werden einige mathematische Werkzeuge zusammengestellt, die zum Verständnis der vorangehenden Kapitel hilfreich sind. Auch hier wird auf aufwendige Begriffsanhäufungen verzichtet und der Stoff nur so weit geboten, wie er tatsächlich gebraucht wird.
Michael Schenke
Backmatter
Metadata
Title
Logikkalküle in der Informatik
Author
Michael Schenke
Copyright Year
2013
Electronic ISBN
978-3-8348-2295-6
Print ISBN
978-3-8348-1887-4
DOI
https://doi.org/10.1007/978-3-8348-2295-6

Premium Partner