In case a logic formula is mechanically constructed, obtained as the specification of an expression in an imperative programming language for example, the functional constraints could be implicit in the sub-formulas or may not be functional at all.
To form an analogy. We usually apply the resolution to a clause, such as the following: $$ \frac {C_1 \lor p(x, f(z)), \quad C_2 \lor \neg p(g(z), y)} {(C_1 \lor C_2) \sigma}, \sigma = [g(z)/x, f(z)/y] $$
But if we encounter the following case (with relational constraints $f$ and $g$ instead of functional), it has to be treated slightly differently:
$$ \frac {C_1 \lor p(x, z_f) \lor \neg \color{blue}{f(z, z_f)}, \quad C_2 \lor \neg p(z_g, y) \lor \neg \color{blue}{g(z, z_g)}} {(C_1 \lor C_2) \lor \neg \sigma},\\ \sigma \equiv \color{blue}{g(z, x)} \land \color{blue}{f(z, y)} \land f(z, z_f) \land g(z, z_g) $$
The trivia aside, I suppose there are algorithmic issues here. We need to find the predicates that merely enforce constraints and are not in danger of conflicting with other predicates (thus being essential for the outcome of the resolution.) We need to track them when manipulating the formulas, if necessary. The substitution has different format also.
Are there any articles, or books, or sub-fields that have addressed the algorithmic issue from this perspective?