3
$\begingroup$

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

$\endgroup$
  • $\begingroup$ The Wikipedia articles tells us that Horn satisfiability is solvable in linear time.. $\endgroup$ – Pål GD Aug 6 '17 at 12:21
  • $\begingroup$ Ps, satisfiability (or simply SAT) is NP-complete, so that would be too general. $\endgroup$ – Pål GD Aug 6 '17 at 12:23
  • $\begingroup$ @PålGD, yes I know, but I don't see how satisfiability is relevant here. We are not trying to exhaustively search all boolean values for the predicates -- there is a knowledgebase to consult. The complexity of the resolution algorithm seems like a different issue. Already SLD resolution (for Horn clauses) can have exponential runtime, and may not even terminate. Would resolution for arbitrary disjunctions be worse? In what sense? $\endgroup$ – Roland Aug 6 '17 at 12:35
6
$\begingroup$

$\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.

$\endgroup$
  • $\begingroup$ I have to read up on these concepts a bit, but it sounds like you're saying that we don't allow things like $P \rightarrow Q_1 \land Q_2$ due to the closed world assumption: neither $Q_1$ or $Q_2$ can be proven, and propositions that can't be proven are considered false. Correct? $\endgroup$ – Roland Aug 7 '17 at 6:24
  • $\begingroup$ The issue doesn't have anything to do with the closed world assumption and nothing is considered false. Those concerns only arise when you're considering negation. The usual semantics of a (pure) logic programming language is goal-directed proof search. A logic program succeeds if it finds a proof; it fails if it doesn't. Failing to find a proof is not the same as finding a refutation which is why negation-as-failure is ill-behaved. $\endgroup$ – Derek Elkins Aug 7 '17 at 7:25
  • $\begingroup$ The proofs such an approach finds are uniform proofs, but not all proofs are uniform. Something can be provable but not uniformly provable so goal-directed proof search may simply fail to find the proof. An abstract logic programming language is a language where that doesn't happen. This is achieved by restricting the language of formulas and potentially also tweaking our notion of "provable". $\endgroup$ – Derek Elkins Aug 7 '17 at 7:25
  • $\begingroup$ Okay, I have now read the Miller et al paper. I don't understand all of it, but it seems to me like the notion of a uniform proof itself assumes a specific proof search algorithm (the "search instructions" on p.6) that excludes the example $P \rightarrow Q_1 \lor Q_2$ by requiring that we prove either $Q_1$ or $Q_2$ explicitly. But I don't see the motivation for why the algorithm must look like this. Why is the search algorithm I suggested that proves $Q_1 \lor Q_2$ directly not allowed? $\endgroup$ – Roland Aug 12 '17 at 10:01
  • $\begingroup$ Uniform proof is modeled on a specific kind of proof search. In no way is this the only approach to proof search. However, it is the approach that Prolog takes, and (to an unhealthy extent) Prolog is the archetype of what "logic programming" means. So the notion of abstract logic programming language is trying to capture this historical fact. On the other hand, this choice by Prolog wasn't arbitrary. $\endgroup$ – Derek Elkins Aug 12 '17 at 16:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.