Definition
Term pattern matching comes in many variations. The basic problem is that of matching a term pattern (term with variables) against a ground subject term (without variables), producing a substition mapping the variables to the corresponding subterms in the subject term.
More often a subject term is matched against a set of patterns and the matching pattern or patterns has to be found.
Variations
The matching problem problem comes in many different guises. The basic problem considers matching a term at the root
Properties of the patterns
Implementation
Efficient implementations of pattern matching pre-process the pattern into an efficient automaton that walks the subject tree only once.
References
Here are some references to papers on the subject: