Special Issue on Automated Deduction: Decidability, Complexity, Tractability

Decidability and complexity issues are extremely important in automated deduction. Although general logical formalisms (predicate logic, set theory, number theory) are undecidable or not even recursively enumerable, it is often the case that in applications only special fragments need to be considered, which are decidable and sometimes even have low complexity. In the field of automated deduction, considerable effort was dedicated to the task of identifying decidable problems and studying their complexity, and in giving uniform decision procedures obtained with general-purpose methods such as resolution, tableau calculi or sequent calculi, and to study situations in which these methods can be tuned to provide algorithms with optimal complexity. In recent years, automated reasoning techniques found a large number of practical applications ranging from knowledge representation (reasoning in large databases and ontologies, reasoning in non-classical logics) to program verification and verification of reactive, real time or hybrid systems. The need of efficient decision procedures for application areas in which the complexity and size of formulae is really large – e.g. reasoning in large ontologies and problems arising from verification – was an important stimulus for the investigation of decidable (and even tractable) logical theories and their complexity. In most applications logical theories do not appear alone: the problems to be solved are of a heterogeneous nature, and need to be modeled using combinations of theories.[…]