ADDCT 2014 PROCEEDINGS: EDITOR'S PREFACE

This volume contains the papers presented at the workshop  ADDCT 2014: Automated Deduction: Decidability, Complexity, Tractability, held in Vienna on July 18, 2014 (affiliated with IJCAR 2014 and RTA 2014).

ADDCT 2014 is the fourth of the ADDCT workshops: The previous workshops were ADDCT 2007 (held in Bremen, together with CADE 21), ADDCT 2009 (held in Montreal together with CADE 22) and ADDCT 2013 (held in Lake Placid together with CADE 24).

The goal of ADDCT is to bring together researchers interested in

• Decidability, in particular decision procedures based on logical calculi such as: resolution, rewriting, tableaux, sequent calculi, or natural deduction,  but also decidability in combinations of logical theories; 
• Complexity, especially complexity analysis for fragments of first- (or higher) order logic and complexity analysis for combinations of logical theories (including parameterized complexity results); 
• Tractability (in logic, automated reasoning, algebra, ...); 
• Application domains for which complexity issues are essential (verification, security, databases, ontologies, ...).

With the development of computer science these problems are becoming extremely important. 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 programme of ADDCT 2014 includes one invited talk, by Nicolas Peltier, entitled "A Superposition-Based Approach to Abductive Reasoning in Equational Clausal Logic'' and 5 contributed papers.  We allowed the possibility of submitting to ADDCT not only original papers, but also presentation-only papers, describing work presented in papers which are already published.  We thank the programme committee and the additional reviewers for their careful referee reports.   The workshop organizers greatly benefited from using the EasyChair system.