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.