Blick ins Buch

Tableau, Tableauresolution und Tableaugraphresolution

Ein neuer Weg zur Automatischen Deduktion

Buch | Softcover

117 Seiten

1991
Peter Lang Gmbh, Internationaler Verlag Der Wissenschaften
978-3-631-44001-8 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)

Keine Verlagsinformationen verfügbar

Artikel merken

Die Klauselresolution ist derzeit das populärste Deduktionsverfahren. Ihre Anwendung ist jedoch auf die Klauselmenge eingeschränkt. Die vorliegende Arbeit stellt ein Verfahren vor, das mit Hilfe von Unifikation bzw. Resolution die gesamte Prädikatenlogik bearbeitet. Die in dieser Arbeit eingeführten Tableaus - Polybäume mit Literaleinfärbung - dienen zur strukturisierten Formeldarstellung. Daraus erhält man einen völlig neuen Kalkül, die Tableauresolution. Der Übergang von der Tableauresolution zur Tableaugraphresolution erfolgt wie von der Klauselresolution zur Klauselgraphresolution. Systematisch werden die Eigenschaften wie Korrektheit, Vollständigkeit und Konfluenz darüber ausgesprochen.

Der Autor: Wanlin Li wurde 1963 in Sichnan, China geboren. Er studierte Informatik an der Chongging-Universitä, China. Seit 1987 ist er an der Fakultät für Informatik der Universität Karlsruhe.

Aus dem Inhalt: Automatisches Beweisen - Prädikatenlogik erster Stufe - Tableaus - Tableauresolution - Tableaugraphresolution - Polybaum - Kodierung von Tableaus.

Erscheint lt. Verlag	1.10.1991
Reihe/Serie	Europäische Hochschulschriften / European University Studies / Publications Universitaires Européennes ; 6
Verlagsort	Frankfurt a.M.
Sprache	deutsch
Maße	148 x 210 mm
Gewicht	180 g
Themenwelt	Mathematik / Informatik ► Informatik ► Theorie / Studium
Themenwelt	Mathematik / Informatik ► Mathematik
Schlagworte	automatischen • Deduktion • Neuer • tableau • TABLEAUGRA • Tableaugraphresolution • Tableauresolution • Wanlin
ISBN-10	3-631-44001-4 / 3631440014
ISBN-13	978-3-631-44001-8 / 9783631440018
Zustand	Neuware