Benutzer: Gast  Login
Originaltitel:
Normalization of Horn Clauses with Disequality Constraints 
Übersetzter Titel:
Normalisierung von Hornklauseln mit Ungleichheitsbedingungen 
Jahr:
2013 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Seidl, Helmut (Prof. Dr.) 
Gutachter:
Seidl, Helmut (Prof. Dr.); Esparza Estaun, Francisco Javier (Prof. Dr. Dr. h.c.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Schlagworte (SWD):
Horn-Klausel; Entscheidbarkeit 
TU-Systematik:
DAT 706d; DAT 542d 
Kurzfassung:
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. 
Übersetzte Kurzfassung:
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. 
Mündliche Prüfung:
05.06.2013 
Dateigröße:
867245 bytes 
Seiten:
98 
Letzte Änderung:
28.02.2014