How to efficiently determine if two propositions are equivalent? Given any two arbitrary propositional formulas only using $\land, \lor, \lnot$, e.g., $\lnot(A \land (B \lor \lnot B) \land C)$ and $\lnot C \lor \lnot A$, how can I (or a computer) efficiently determine if they are equivalent?
The formulas may contain many propositions, so the corresponding truth tables may be exponentially large. Is there a fast algorithm to convert formulas to some normal form so that any two equivalent formulas will reduce to the same normal form?

Efficient : NO.
See Boolean satisfiability problem, abbreviated as SATISFIABILITY or SAT :

There is no known algorithm that efficiently solves SAT, and it is generally believed that no such algorithm exists.

To ask for two propositional formulae $\mathcal A, \mathcal B$ are equivalent can be reduced to asking if :

$\mathcal A \vDash \mathcal B$ and $\mathcal B \vDash \mathcal A$.

But $\mathcal A \vDash \mathcal B$ iff $\vDash \mathcal A \rightarrow \mathcal B$, i.e. $\mathcal A \rightarrow \mathcal B$ is a tautology and this in turn is equivalent to $\mathcal A \land \lnot \mathcal B$ being unsatisfiable.
In other words, if one of $\mathcal A \land \lnot \mathcal B$ and $\mathcal B \land \lnot \mathcal A$ is satisfiable, then $\mathcal A, \mathcal B$ are not equivalent.
