decomposable theories

International audienceWe present in this paper a general algorithm for solving first-order formulas in particular theories called decomposable theories. First of all, using special quantifiers, we give a formal characterization of decomposable theories and show some of their properties. Then, we present a general algorithm for solving first-order formulas in any decomposable theory T. The algorithm is given in the form of five rewriting rules. It transforms a first-order formula ', which can possibly contain free variables, into a conjunction C of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if ' has no free variables then C is either the formula true or ¬true. The correctness of our algorithm proves the completeness of the decomposable theories. Finally, we show that the theory T of finite or infinite trees is a decomposable theory and give some benchmarks realized by an implementation of our algorithm, solving formulas on two-partner games in T with more than 160 nested alternated quantifiers