An order-sorted query system for sort, predicate, and meta-predicate hierarchies

This paper presents a decidable order-sorted query system for reasoning between ontologies and rules. We describe order-sorted logic programming with sort, predicate, and meta-predicate hierarchies (OSL_3h), which derives predicate and meta-predicate assertions. Meta-level predicates (predicates of predicates) are useful for representing relationships between predicate formulas, and further, they conceptually yield a hierarchy similar to the hierarchies of sorts and predicates. By extending the order-sorted Horn-clause calculus, we develop a query-answering system in OSL_3h that can answer queries such as atoms and meta-atoms generalized by containing predicate variables. We show that the expressive query-answering system computes every generalized query in single exponential time, that is, the complexity of our query system is equal to that of DATALOG.