I don't know how to translate this problem to mathematical logic language. How am I supposed to came up with a Horn formula from this? I should easily be able to test it's satisfiability after that, but I'm stuck at the beginning.
Suppose we have the apparatuses available to perform the following chemical reactions.
$$ MgO + H_2 \rightarrow Mg + H_2O\\ C + O_2 \rightarrow CO_2\\ H_2O + CO_2 \rightarrow H_2CO_3 $$
Further, our lab has the following basic materials available: $MgO$, $H_2$, $O_2$ and $C$. Prove (by an appropriate application of the Horn formula algorithm) that under these circumstances it is possible to produce $H_2CO_3$.
Hint
You have already the "basic ingredients"; you have only to formalize them as Horn-clause :
Clauses
1) $\lnot MgO \lor \lnot H_2 \lor Mg $
2) $\lnot MgO \lor \lnot H_2 \lor H_2O$
3) $\lnot C \lor \lnot O_2 \lor CO_2$
4) $\lnot H_2O \lor \lnot CO_2 \lor H_2CO_3$
Facts
5) $MgO, H_2, O_2, C$.
Goal
Now you can easily check themfor satisfiability.