  In this paper we investigate the use of the concept of tree dimension in Horn
clause analysis and verification. The dimension of a tree is a measure of its
non-linearity - for example a list of any length has dimension zero while a
complete binary tree has dimension equal to its height. We apply this concept
to trees corresponding to Horn clause derivations. A given set of Horn clauses
P can be transformed into a new set of clauses P=<k, whose derivation trees are
the subset of P's derivation trees with dimension at most k. Similarly, a set
of clauses P>k can be obtained from P whose derivation trees have dimension at
least k + 1. In order to prove some property of all derivations of P, we
systematically apply these transformations, for various values of k, to
decompose the proof into separate proofs for P=<k and P>k (which could be
executed in parallel). We show some preliminary results indicating that
decomposition by tree dimension is a potentially useful proof technique. We
also investigate the use of existing automatic proof tools to prove some
interesting properties about dimension(s) of feasible derivation trees of a
given program.
