Login
- Originaltitel:
- Normalization of Horn Clauses with Disequality Constraints
- Übersetzter Titel:
- Normalisierung von Hornklauseln mit Ungleichheitsbedingungen
- Autor:
- Reuß, Andreas
- Jahr:
- 2013
- Dokumenttyp:
- Dissertation
- Fakultät/School:
- 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.
- WWW:
- https://mediatum.ub.tum.de/?id=1116533
- Eingereicht am:
- 25.10.2012
- Mündliche Prüfung:
- 05.06.2013
- Dateigröße:
- 867245 bytes
- Seiten:
- 98
- Urn (Zitierfähige URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130605-1116533-0-3
- Letzte Änderung:
- 28.02.2014
BibTeX