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?
 A: 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.
A: Suppose that two propositional formulas $\alpha$ and $\beta$ are equal.  Then it follows that ($\alpha$$\rightarrow$$\beta$) is logically equivalent to ($\beta$$\rightarrow$$\alpha$).  So, ($\alpha$$\rightarrow$$\beta$) and ($\beta$$\rightarrow$$\alpha$) are both tautologies.  Thus, if $\alpha$ and $\beta$ are not equal, then either ($\alpha$$\rightarrow$$\beta$) is false or ($\beta$$\rightarrow$$\alpha$) is false.  So, without using truth tables, we can suppose ($\alpha$$\rightarrow$$\beta$) false, which implies $\alpha$ is true, and $\beta$ is false.  If that doesn't work out, then ($\alpha$$\rightarrow$$\beta$) is true.  Likewise for ($\beta$$\rightarrow$$\alpha$).  Either both ($\alpha$$\rightarrow$$\beta$) and ($\beta$$\rightarrow$$\alpha$) are true, both ($\alpha$$\rightarrow$$\beta$) and ($\beta$$\rightarrow$$\alpha$) are false in which case $\alpha$=$\beta$, or only one of them is false and the other is true, in which case $\alpha$ doesn't equal $\beta$.
As an example of using that method, we'll look at your formulas:
Suppose $\lnot$[(¬C∨¬A)$\rightarrow$¬(A∧(B∨¬B)∧C)].  Thus, ¬(A∧(B∨¬B)∧C) is false.  So, (A∧(B∨¬B)∧C) is true.  Thus, A, and C are both true, and thus (¬C∨¬A) is false, which is contrary to the hypothesis.  So, [(¬C∨¬A)$\rightarrow$¬(A∧(B∨¬B)∧C)] is always true.
Suppose  $\lnot$(¬(A∧(B∨¬B)∧C)$\rightarrow$(¬C∨¬A)].  Then, (¬C∨¬A) is false.  So, ¬C is false, and so is ¬A.  Thus, A and C are both true.  ¬(A∧(B∨¬B)∧C) is true, and thus (A∧(B∨¬B)∧C) is false.  But, since A, C, and (B∨¬B) are all true, we have a contradiction.  Thus, (¬(A∧(B∨¬B)∧C)$\rightarrow$(¬C∨¬A)] is always true.
Since both implications are always true, it follows that the two propositional formulas are equal.  
