Assume I have two Horn formulas $ \phi_1, \phi_2$ . Horn formulas are CNF formulas so that each clause has at most one unnegated literal, for example

$ x_1 \vee (\neg x_1 \vee \neg x_2 \vee x_3 )\vee (x_3 \vee \neg x_4)$

I want to decide whether $ \phi_1,\phi_2$ are logically equivalent, i.e., $ \phi_1 \leftrightarrow \phi_2$ . Equivalently, I want to test whether $ F=(\phi_1 \vee \neg\phi_2)\wedge (\neg \phi_1 \vee \phi_2)$ is true for all assignments of $ x_1,\dots,x_n$ .

Is this problem tractable?