1992 | OriginalPaper | Chapter
Logische Sprachen
Author : Volker Penner
Published in: Parallelität und Transputer
Publisher: Vieweg+Teubner Verlag
Included in: Professional Book Archive
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.