Generalization of Horn clauses in logic programming?

Question

As far as I understand, Prolog and related languages are restricted to inference rules of the form $$ p_1 \land \dots \land p_n \rightarrow q$$ which is equivalent to the Horn clause $$ \neg p_1 \lor \dots \lor \neg p_n \lor q$$ I'm wondering if there are languages that relax this constraint to allow arbitrary disjuctions as clauses in the knowledgebase, and if so what the downsides of this would be. For example, the rule $$ p \rightarrow q_1 \lor q_2 \equiv \neg p \lor q_1 \lor q_2$$ is not a Horn clause and is not allowed in Prolog, but it seems to me that it would be possible to run a resolution algorithm for such clauses as well. For example, if $p = \top$, then we can prove $q_1 \lor q_2$ by contradiction: we assume the converse $\neg(q_1 \lor q_2) = \neg q_1 \land \neg q_2$ and resolve $$ (\neg p \lor q_1 \lor q_2) \land (\neg q_1 \land \neg q_2) = \neg p$$ which then yields a contradiction $p \land \neg p$.

Why should such arbitraty disjuctions not be permitted? Is it somehow related to the satisfiability problem (HORNSAT) ? Or is it due to the closed world assumption (where the statement $q_1 \lor q_2 = \top$ is paradoxical) ?

p.s. I am a hobbyist in logic programming, so simple informal explanations are appreciated :)