Suppose we have a first order sentences $\phi$, $\psi$, and $\chi$ such that:
$\phi$ $\longleftrightarrow$ ($\psi$ $\land$ $\chi$)
And $\phi$ and $\chi$ are known or fixed. How can we search for a formula $\psi$ such that the statement is valid?
I understand the proof calculus to search for consequences of first order sentences, using deduction and rules of inference, or to test if a particular statement is valid. With the resolution rule it becomes simple and straightforward to turn everything into clauses, assume the negation, and search for the empty clause (contradiction.)
It's not obvious to me how we can search for a sentence $\psi$ without doing brute force enumeration of well formed formulas and using resolution to test for validity of the equivalence statement. Are there any more efficient techniques?