Standard and Non-Standard Inferences in the Description Logic FL0 Using Tree Automata

Aus International Center for Computational Logic
Wechseln zu:Navigation, Suche

Standard and Non-Standard Inferences in the Description Logic FL0 Using Tree Automata

Vortrag von Oliver Fernández Gil
Although being quite inexpressive, the description logic (DL) FL0, which provides only conjunction, value restriction and the top concept as concept constructors, has an intractable subsumption problem in the presence of terminologies (TBoxes): subsumption reasoning w.r.t. acyclic FL0 TBoxes is coNP-complete, and becomes even ExpTime-complete in case general TBoxes are used. In this talk, I will describe an approach that uses automata working on infinite trees to solve both standard and non-standard inferences in FL0 w.r.t. general TBoxes. I will start by sketching an alternative proof of the ExpTime upper bound for subsumption in FL0 w.r.t. general TBoxes based on the use of looping tree automata. Afterwards, I will explain how to employ parity tree automata to tackle non-standard inference problems such as computing the least common subsumer w.r.t. general TBoxes.