  The theory of finite term algebras provides a natural framework to describe
the semantics of functional languages. The ability to efficiently reason about
term algebras is essential to automate program analysis and verification for
functional or imperative programs over algebraic data types such as lists and
trees. However, as the theory of finite term algebras is not finitely
axiomatizable, reasoning about quantified properties over term algebras is
challenging.
  In this paper we address full first-order reasoning about properties of
programs manipulating term algebras, and describe two approaches for doing so
by using first-order theorem proving. Our first method is a conservative
extension of the theory of term algebras using a finite number of statements,
while our second method relies on extending the superposition calculus of
first-order theorem provers with additional inference rules.
  We implemented our work in the first-order theorem prover Vampire and
evaluated it on a large number of algebraic data type benchmarks, as well as
game theory constraints. Our experimental results show that our methods are
able to find proofs for many hard problems previously unsolved by
state-of-the-art methods. We also show that Vampire implementing our methods
outperforms existing SMT solvers able to deal with algebraic data types.
