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 :)

Answer 1

$\lambda$Prolog is a logic programming language based on a much richer logic than Prolog. In particular, the formulas that constitute its language are (higher-order) hereditary Harrop formulas. Horn clauses are a pallid fragment of that. The enabling concept for $\lambda$Prolog is the notion of a uniform proof, and additionally switching to an intuitionistic perspective on the logic. That last paper introduces the notion of an abstract logic programming language based on the notion of uniform proof and shows that classical first-order and higher-order Horn clauses form an abstract logic programming language.

Basically, a uniform proof is one where the rules used can be given an operational interpretation based on goal-directed search. This isn't the actual definition of a uniform proof, but the motivation behind the actual definition. An abstract logic programming language is one where uniform proofs suffice to prove any formula in the language with respect to a given notion notion of provability that is contained by the usual classical one.

Even the class of higher-order hereditary Harrop formulas doesn't allow $P \to Q_1\lor Q_2$ as a program clause. (It is allowable as a goal.) Why not? Obviously, $P, P\to Q_1\lor Q_2 \vdash Q_1\lor Q_2$, that is, if we know $P$ holds, and we know $P \to Q_1 \lor Q_2$ holds, then we can prove $Q_1 \lor Q_2$. However, this proof succeeds without ever specifying which of $Q_1$ or $Q_2$ holds. Indeed, neither $P, P\to Q_1\lor Q_2 \vdash Q_1$ nor $P, P\to Q_1\lor Q_2 \vdash Q_2$ is true. Formally, the proof of $Q_1\lor Q_2$ from $P$ and $P\to Q_1\lor Q_2$ is not a uniform proof. Informally, the operational interpretation we'd like to give to proving $Q_1 \lor Q_2$, is that we search for a proof of $Q_1$ and a proof of $Q_2$, and if either search succeeds we've established $Q_1 \lor Q_2$. Obviously this search approach will fail in the above example since neither $Q_1$ nor $Q_2$ can be individually established.

Finally, why do we need to "retreat" to intuitionistic logic in the hereditary Harrop formula case (we don't for Horn clauses)? This is because $P\lor(P\to Q)$ is a goal in the class of hereditary Harrop formulas, and it's classically true. However, if we again apply our operational interpretation, the search would proceed as follows: First try to prove $P$, this fails. Next, try to prove $P\to Q$ which reduces to proving $Q$ given $P$ which fails. $P\lor(P\to Q)$ isn't true intuitionistically since when $Q$ is false, this is just the law of the excluded middle. Of course, it requires a more involved proof (which is in the paper) to show that there isn't a similar failure with respect to intuitionistic logic for the class of higher-order hereditary Harrop formulas.

Since 1991, the notion of an abstract logic programming language has been extended. The most notable extension is the generalization of uniform proofs to focusing proofs, and the idea has been applied primarily in the context of linear logics. In many ways disjunction and negation are more tractable in linear logic. However, the idea has also been applied to Disjunctive Logic Programming. The idea was (first?) applied in Uniform Proofs and Disjunctive Logic Programming, but it didn't provide any guidance on how to handle quantifier elimination. That is, the idealized interpreter of an abstract logic programming language assumes you can "magically" guess the term to use in existential quantifier elimination. Normally this is accomplished with unification, but unification interacts with proof search. For example, higher order unification generates extra backtracking and the universal quantifiers in hereditary Harrop formulas lead to eigenvariables. Unification interacts with disjunction as well. The later paper A New Abstract Logic Programming Language and its Quantifier Elimination Method for Disjunctive Logic Programming gives a story not just for the abstract logic programming part of Disjunctive Logic Programming, but also how unification needs to be modified in this context.

To my knowledge, DLV seems to be the only serious implementation of any form of disjunctive logic programming.