Login
- Original title:
- Normalization of Horn Clauses with Disequality Constraints
- Translated title:
- Normalisierung von Hornklauseln mit Ungleichheitsbedingungen
- Author:
- Reuß, Andreas
- Year:
- 2013
- Document type:
- Dissertation
- Faculty/School:
- 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.
- WWW:
- https://mediatum.ub.tum.de/?id=1116533
- Date of submission:
- 25.10.2012
- Oral examination:
- 05.06.2013
- File size:
- 867245 bytes
- Pages:
- 98
- Urn (citeable URL):
- https://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20130605-1116533-0-3
- Last change:
- 28.02.2014
BibTeX