  Developing an efficient non-linear Horn clause solver is a challenging task
since the solver has to reason about the tree structures rather than the linear
ones as in a linear solver. In this paper we propose an incremental approach to
solving a set of non-linear Horn clauses using a linear Horn clause solver. We
achieve this by interleaving a program transformation and a linear solver. The
program transformation is based on the notion of tree dimension, which we apply
to trees corresponding to Horn clause derivations. The dimension of a tree is a
measure of its non-linearity -- for example a linear tree (whose nodes have at
most one child) has dimension zero while a complete binary tree has dimension
equal to its height.
  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$). We start by generating $P^k$ with $k=0$, which is
linear by definition, then pass it to a linear solver. If $P^k$ has a solution
$M$, and is a solution to $P$ then $P$ has a solution $M$. If $M$ is not a
solution of $P$, we plugged $M$ to $P^{(k+1)}$ which again becomes linear and
pass it to the solver and continue successively for increasing value of $k$
until we find a solution to $P$ or resources are exhausted. Experiment on some
Horn clause verification benchmarks indicates that this is a promising approach
for solving a set of non-linear Horn clauses using a linear solver. It
indicates that many times a solution obtained for some under-approximation
$P^k$ of $P$ becomes a solution for $P$ for a fairly small value of $k$.

Logic in Computer Science