Testing wffs for equivalency

This question popped out in a conversation I had and I couldn't figure
anything useful out of it. Any thoughts?

If we have two different wffs a and b in FO could one test if they are
equivalent? Is it possible to write, say, an algorithm which takes two
wffs, tests if they are equal and returns true if they are and if they
differ provides a model in which one is true and the another is false?

If such algorithm exists would it be of "reasonable complexity" for
real life usage?

I think I have faced this question earlier but can't recall when and
couldn't find anything concerning it from my books.
.

Relevant Pages
Quantcast