User: Guest  Login
Original title:
Normalization of Horn Clauses with Disequality Constraints 
Translated title:
Normalisierung von Hornklauseln mit Ungleichheitsbedingungen 
Year:
2013 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Seidl, Helmut (Prof. Dr.) 
Referee:
Seidl, Helmut (Prof. Dr.); Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Controlled terms:
Horn-Klausel; Entscheidbarkeit 
TUM classification:
DAT 706d; DAT 542d 
Abstract:
We prove the class H1 of Horn clauses decidable when extended with disequality tests of arbitrary (sub)terms. Decidability even is preserved if the terms are transformed by a given tree homomorphism prior to the test for disequality. Furthermore, a novel class of tree automata with equality and disequality tests is introduced, for which we prove Boolean closure and decidability. 
Translated abstract:
Wir zeigen, dass die Klasse H1 von Hornklauseln entscheidbar bleibt, wenn sie mit Ungleichheitstests zwischen beliebigen (Sub-)Termen erweitert wird. Die Entscheidbarkeit bleibt auch erhalten, wenn die Terme vor dem Test auf Ungleichheit durch einen Baumhomomorphismus transformiert werden. Des Weiteren wird eine neue Klasse von Baumautomaten mit Gleichheits- und Ungleichheitsbedingungen eingeführt, für die wir Booleschen Abschluss und Entscheidbarkeit beweisen. 
Oral examination:
05.06.2013 
File size:
867245 bytes 
Pages:
98 
Last change:
28.02.2014