gif gif up gif contents index
Nächste Seite: 2.11.9 Probabilistisches Wissen Vorige Seite: 2.11.7 Modallogik

2.11.8 Markierte Deduktionsformalismen

Im vorangegangenen Unterabschnitt haben wir Erweiterungen der Prädikatenlogik betrachtet. Im folgenden Kapitel werden wir andere Erweiterungen der Prädikatenlogik besprechen. Damit ist die Vielfalt möglicher Logiken noch bei weitem nicht erschöpft. Wenn man das Ziel eines allgemeinen intelligenten Systems ernsthaft weiterverfolgen möchte, so ergibt sich durch diese Vielfalt das Problem der Integration verschiedener Logiken innerhalb eines einzigen Systems.

Eine mögliche Lösung dieses Integrationsproblems ergibt sich, wenn es gelingt, einen allgemeinen Deduktionsformalismus anzugeben, von dem all die genannten Logikvarianten Instanzen sind. Ein solch allgemeiner Formalismus ist der von Dov Gabbay in [Gaben] entwickelter markierter Deduktionsformalismus (engl. labelled deductive systems, kurz LDS). Er ist so allgemein, daß wohl alle in diesem Buch genannten Logikformalismen als Instanz eines LDS angesehen werden können. In einem LDS wird eine Ableitbarkeitsrelation nicht wie üblich zwischen (Mengen von) Formeln, sondern zwischen markierten Formeln definiert. Die verschiedenen Ausprägungen solcher Markierungen ergeben dann die verschiedenen Logikvarianten.

Die Idee eines markierten Deduktionssystems wurde wohl zum ersten Mal in der Konnektionsmethode [Bib87a] realisiert, wo als Markierung eine Struktur auf der Formel gegeben ist und wo sich die Formel selbst bei jedem Ableitungsschritt überhaupt nicht ändert.



Christoph Quix, Thomas List, René Soiron
30. September 1996