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.