  In this paper, we show how the notion of tree dimension can be used in the
verification of constrained Horn clauses (CHCs). The dimension of a tree is a
numerical measure of its branching complexity and the concept here applies to
Horn clause derivation trees. Derivation trees of dimension zero correspond to
derivations using linear CHCs, while trees of higher dimension arise from
derivations using non-linear CHCs. We show how to instrument CHCs predicates
with an extra argument for the dimension, allowing a CHC verifier to reason
about bounds on the dimension of derivations. Given a set of CHCs $P$, we
define a transformation of $P$ yielding a dimension bounded set of CHCs
$P^{\leq{k}}$. The set of derivations for $P^{\leq{k}}$ consists of the
derivations for $P$ that have dimension at most $k$. We also show how to
construct a set of clauses denoted $P^{>{k}}$ whose derivations have dimension
exceeding $k$. We then present algorithms using these constructions to
decompose a CHC verification problem. One variation of this decomposition
considers derivations of successively increasing dimension. The paper includes
descriptions of implementations and experimental results. Under consideration
for publication in Theory and Practice of Logic Programming (TPLP).
