  We address the problem of checking the satisfiability of Constrained Horn
Clauses (CHCs) defined on Algebraic Data Types (ADTs), such as lists and trees.
We propose a new technique for transforming CHCs defined on ADTs into CHCs
where the arguments of the predicates have only basic types, such as integers
and booleans. Thus, our technique avoids, during satisfiability checking, the
explicit use of proof rules based on induction over the ADTs. The main
extension over previous techniques for ADT removal is a new transformation
rule, called differential replacement, which allows us to introduce auxiliary
predicates, whose definitions correspond to lemmas that are used when making
inductive proofs. We present an algorithm that performs the automatic removal
of ADTs by applying the new rule, together with the traditional
folding/unfolding rules. We prove that, under suitable hypotheses, the set of
the transformed clauses is satisfiable if and only if so is the set of the
original clauses. By an experimental evaluation, we show that the use of the
new rule significantly improves the effectiveness of ADT removal. We also show
that our approach is competitive with respect to tools that extend CHC solvers
with the use of inductive rules.
