Automata-based reasoning for decidable logics with data values

Abstract

Decidable logics play a major role in knowledge representation, automated verification, and database management. A common ground relating many of these logics is the two-variable fragment of First Order logic (FO2), which is well-suited for handling graph-structured data. Real-world applications nearly always require us to model so-called concrete values such as measurements, strings, and time. As a result, efforts have been made to incorporate data values into DLs, and to extend FO2 with means for modeling data while maintaining decidability.The overarching goal of this thesis is to develop techniques based on automata for reasoning in rich decidable logics that allow to model data values. We concentrate on two different expressive logics with data values, and employ automata for solving the following open problems.First, we consider a DL called ALCP(Zc) that supports constraints given as comparisons of integer numbers. Decidability of this logic has been proven but no upper complexity bounds has been established for the problem. We obtain a tight ExpTime upper bound for deciding concept satisfiability w.r.t. general TBoxes which is, to our knowledge, the first complexity upper bound for reasoning with general TBoxes and discrete concrete domains.Second, we consider the logic FO2 with a linear order, a total preorder, and its induced successor, whose finite satisfiability problem is known to be ExpSpace -complete. We introduce a novel automata model called Pebble-Intervals automata (PIA), study its power in contrast to other automata models, and investigate its emptiness problem and its closure properties. We also obtain an automata-theoretic proof of the upper bound for the finite satisfiability problem of the logic by reducing it to a PIA emptiness test.