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?

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.  
