Term-rewriting software recommendation
PLT Redex has support for term rewriting. You'll find that most of the examples are focused on small-step operational semantics for programming languages, but in general the system allows for arbitrary rewriting, including non-determinism. It also has a bunch of nice features, like randomized testing of properties, alpha-equivalence, steppers for visualising/debugging, and excellent graphical output.
If you want higher-order syntax, you might be interested in something like ELPI.
For a super-lightweight prolog-style programming, you might be interested in miniKanren.