How to efficiently determine if two propositions are equivalent?
Solution 1:
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.
Solution 2:
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.