What techniques are there to search for first order sentence equivalence?

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?

• If you have access to an oracle, then this is doable in constant time. Unfortunately, we don't really have access to oracles in this physical reality. :-( – Asaf Karagila Jul 2 '14 at 2:41

Assuming your first order theory $T$, (where $T$ may possibly be the empty theory) does not have quantifier elimination, the following holds (furthermore, we can possibly argue that in most cases that do not have effective quantifier elimination, the following holds).
Now, your question above is actually "harder" than determining whether a sentence is valid or not (by harder, I mean that your question encodes the question above). Suppose we fix $\varphi$ and $\chi$ such that $\varphi \equiv \chi \equiv \tau$ (By $\equiv$, I mean logically equivalent), where $\tau$ is some logical validity. Then, finding $\psi$ is the exactly the same as finding the set of valid sentences. Again, while this set is recursively enumerable, it is not recursive, and so there is no way of actually finding all the sentences which satisfy this sentence.