Objectives: The calculi used in automated deduction, such as (ordered) resolution, paramodulation, superposition and chaining, can be used to design decision procedures for many important fragments of first-order logics: the guarded fragment, the two-variable fragment, the monadic fragment, their combinations and extensions. Such decision procedures can be, in particular, used for reasoning in expressive description logics through the standard semantical embedding, where they have certain advantages over conventional tableaux-based procedures, such as optimal worst-case complexity, direct usage of semantics for DL-constructors, and independence from finite/tree model properties of a fragment.
Objectives: In conceptual modelling, e.g. using ontologies, one has to devise automated procedures for maintenance of knowledge bases, e.g. computation of subsumption hierarchies. It has been recognised that understanding the sources of complexities in correspondent reasoning problems is indispensable for development of practical (i.e. resources/time efficient) algorithms performing these tasks. Using automata theory, graph theory and translational methods one can analyse computational complexity for different terminological languages and reasoning tasks, and develop efficient reasoning procedures.