Over at the ILP Discord server there was a discussion about whether a set of Prolog rules should be seen as a disjunction or a conjunction.
The, let’s say “traditional” interpretation that one can find in many Prolog sources is that rules with the same functor/arity are a disjunction, e.g. :
Though note that the LPN link makes a more specific claim that declaring rules with the same fully ground head are a way to express disjunction.
The other interpretation, that was offered by a person with major pedantry issues (yeah, that’s me) is that a set of definite clauses with the same symbol and arity, are, formally, a conjunction.
The debate is complicated by the fact that there are always two interpretations of a Prolog program: a declarative one and a procedural one. In my understanding, in the declarative interpretation, a set of definite clauses is a conjunction. But in the procedural interpretation it’s common to see them as alternatives, i.e. a disjunction, because execution “falls through” from one clause to the next depending on unification. Indeed, this is what I was taught many years ago when first I learned the Art of Prolog. Or its Craft. Can’t remember which. Probably both.
I couldn’t find a specific reference to support my claim except a relatively recent ILP paper that defines a clausal theory as a conjunction of definite clauses. On the other hand, that a set of rules is a conjunction follows from the understanding that rules are axioms of a theory encoded as a logic program, and every axiom of a theory must be true. Of course in Prolog we often say that rules are “conditionally true”, because they are implications. When I thrashed with the same question a while ago, Stephen Muggleton pointed out to me that definite clauses aren’t true or false: they are satisfiable. But that’s not a concept we often encounter in Prolog. We tend to fudge it with “true”.
So I did like kids do today and I went to check with google’s AI. Here’s a link to my conversation:
Just to be clear, I’m not treating the bot as an Oracle. More as an pleasant but unreliable interface to the world wide web.
So the bot started by saying that “A set of axioms is always taken as a conjunction” which agrees with me, but when I asked for an authoritative reference to that it said there aren’t any.
It instead pointed to a couple of references about the definition of a model of a set of formulae. Indeed, if M is a model of Σ then M is a model of every formula φ in Σ. But I’m afraid that is too far from common Prolog parlance to make any sense.
So I come back to the SWI-Prolog community with a question:
In your opinion, fellow Prolog practitioner, is a set of Prolog rules to be read as a disjunction, or a conjunction? Or both, depending on the interpretation (declarative or procedural)?