How to efficiently determine if two propositions are equivalent?

Question

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?

Answer 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.

Answer 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.