Decomposable Theories

TL;DR

This paper introduces a general algorithm for solving first-order formulas in decomposable theories, characterized by special quantifiers, and demonstrates its correctness and applicability to the theory of trees, including practical benchmarks.

Contribution

It presents a formal characterization of decomposable theories and a universal algorithm for solving formulas within these theories, including implementation and benchmarks.

Findings

Algorithm transforms formulas into solvable conjunctions

Proves the completeness of decomposable theories

Successfully applied to theories of finite and infinite trees

Abstract

We 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 "P", which can possibly contain free variables, into a conjunction "Q" of solved formulas easily transformable into a Boolean combination of existentially quantified conjunctions of atomic formulas. In particular, if "P" has no free variables then "Q" is either the formula "true" or "false". The correctness of our algorithm proves the completeness of the decomposable theories. Finally, we show that the theory "Tr" 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 "Tr" with more than 160 nested alternated quantifiers.