Automated Deduction: Decidability, Complexity, Tractability
Overview
Decidability, and especially complexity and tractability of logical theories is extremely important for a large number of applications. Although general logical formalisms (such as predicate logic or number theory) are undecidable, decidable theories or decidable fragments thereof (sometimes even with low complexity) often occur in mathematics, in program verification, in the verification of reactive, real time or hybrid systems, as well as in databases and ontologies. It is therefore important to identify such decidable fragments and design efficient decision procedures for them. It is equally important to have uniform methods (such as resolution, rewriting, tableaux, sequent calculi, ...) which can be tuned to provide algorithms with optimal complexity.
The goal of ADDCT is to bring together researchers interested in
- identifying (fragments of) logical theories which are decidable,identifying fragments thereof which have low complexity, and analyzing possibilities of obtaining optimal complexity results with uniform tools;
- analyzing decidability in combinations of theories and possibilities of combining decision procedures;
- efficient implementations for decidable fragments;
- application domains where decidability resp. tractability are crucial.
Detailed information on ADDCT 2014 can be found on the ADDCT 2014 website.