# Equivalence of Horn fomulas tractable?

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?