Logische Sprachen

Die Erfahrungen im Bereich des Automatischen Beweisens, wo Beweissysteme auf der Grundlage der Resolution [Rob 65], der Induktion oder von Hilbert-Typ-Kalkülen entwickelt werden, zeigen den hohen Aufwand, der bei der Implementation der vollen Prädikatenlogik zu treiben ist. Den meisten logischen Programmiersprachen und insbesondere Prolog [Col 79] (programming in logic) liegt daher eine Teilmenge der Prädikatenlogik - die Horn-Klausel-Logik — zugrunde. Sie ermöglicht die Verwendung der SLD-Resolution (lineare Resolution mit Selektorfunktion für definite Klauseln), die im Unterschied zu allgemeinen Resolutionsprozeduren effiziente Implementationen zuläßt. Logische Programme sind endliche Mengen von Horn-Klauseln, die prädikatenlogische Formeln in Klauselform repräsentieren und die je nach Semantik unterschiedlich interpretiert werden. Aufbauend auf der operationalen Interpretation wird in den folgenden Abschnitten das für parallele logische Sprachen wichtige Prozeßmodell entwickelt. Grundlegend sind dabei syntaktische Begriffe (Term, Formel, Klausel, Substitution, Unifikation) zur Beschreibung und Manipulation von Daten resp. zur Charakterisierung von Eigenschaften und Zusammenhängen und beweistheoretische Begriffe (Resolution), mit deren Hilfe sich ein Ableitungs- und Auswertungsbegriff für Anfragen definieren läßt.