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?
Edit:
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).
As you probably know, given a sentence in FOL, there is no algorithm which will tell you where or not a sentence is a validity. However, both the set of valid sentences and the set of contradictions are computably (recursively) enumerable. This can be done by taking two Turing machines, and as you say, 'brute forcing' the matter.
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.