Function symbols are used, together with constants and variables, to form terms.
The satisfiability problem for free theories is solved by syntactic unification; algorithms for the latter are used by interpreters for various computer languages, such as Prolog.
Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see Unification (computer science).
As an example of uninterpreted functions for SMT-LIB, if this input is given to an SMT solver: the SMT solver would return "This input is satisfiable".
[3] Free theories can be solved by searching for common subexpressions to form the congruence closure.