Sets of rules as conjunctions and/or disjunctions

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

To me, this is essentially the same question as whether to read Prolog programs as knowledge encoded in clausal form or as (inductive) definitions. The classic reference for the conjunction / clausal knowledge view is Bob Kowalski’s timeless Logic for Problem Solving, while the inductive definition / disjunction view is developed in depth in the finite model theory literature on Datalog.

Got some Prolog code to demonstrate this? Sounds wrong, probably due to predicate vs clause confusion.

E.g. 2 predicates with the same ground/1 head are independent of each other. They could exist if there are different ways for the predicates to succeed (aka hold, be satisfied).

Here is a trivial example:

relative_family(james, father, susan, smith).
relative_family(james, son, john, smith).

is_smith(james) :-
    relative_family(james, father, susan, smith).
is_smith(james) :-
    relative_family(james, son, john, smith).
?- is_smith(james).
true ;
true.

The point is: commenting out exactly one of those relative_family/4 facts will still result in one of the is_smith/1 predicates succeeding.

The classical conjunction view would abstract these (written propositionally) as

(a \leftarrow b) \land (a \leftarrow c) \land b \land c

and then conclude that from that conjunction, one can indeed prove a (in fact, using either of the first two conjuncts).

The definitory view would say that this program defines a as b \lor c and that then b and c are defined as true (as facts can be read as empty bodies). Hence, again, one can say that the definition is satisfied (in two different ways using either of the two disjuncts).

I haven’t read Kowalski’s book (I know, right?) but that gels with my understanding of his background in formal logic. I’m always a bit suspicious of the database view on the other hand. It feels like raising an implementation detail to a semantics. But I guess the two views can live side-by-side if they don’t bother each other.

There’s certainly confusion about the meaning of “predicate” in Prolog. To be clear, my sources for logic programming are G. W. Lloyd (Introduction to Logic Programming) and Nienhuys-Cheng and de Wolf (Introduction to Inductive Logic Programming; the first half is a robust introduction to logic and logic programming so it works for both deductive and inductive LP). Neither of them defines “predicate”. There’s no such thing as a “predicate” in FOL: there’s such a thing as a predicate symbol. But in Prolog we call that a “functor” whereas we call a “predicate” either a functor/arity term (as in current_predicate/1) or the head of a clause (as in predicate_property/2). But we also sometimes call a “predicate” what Lloyd calls a “predicate definition” i.e. a set of definite clauses with the same functor/arity. I’ve even heard a single clause out of a set called a “predicate”. Worse, Prolog “functors” are no different to “atoms” which are what FOL calls constants. And there is no distinction between predicate and function symbols as there is in FOL (where the two are disjoint sets). It is very confusing. Anyway when I say “predicate” I mean it in the FOL sense, because that’s the only sane sense. I love Prolog but sometimes the terminological fudge is deep enough to drown in. However this is not about predicates or clauses etc.

That’s similar to the example in the link to the Learn Prolog Now page I link to above. It’s a special case, because it’s a set of propositional clauses. They’re fully ground, right? Still, that doesn’t change the semantics.

Consider this. The Least Herbrand Model (LHM) of is_smith/2 is { is_smith(james), relative_family(james,father,susan,smith), relative_family(james,son,john,smith) }. That is the smallest set of facts that make every clause in the program true.

If we took the two clauses of is_smith/1 as a disjunction, then there would be a smaller model of is_smith/1 than the LHM, either {is_smith(james), relative_family(james, father, susan, smith)} or {is_smith(james), relative_family(james, son, john, smith)}. Then the LHM would not be least. But that’s a contradiction, so the LHM of the set of clauses must be the conjunction of the Herbrand Models of each clause. Yes?

Another way to think of it is that the LHM of is_smith/1 is the intersection of the Herbrand models of its clauses. A set intersection corresponds to a logical conjunction, not a logical disjunction (which corresponds to a set union).

Here’s a different line of argument, maybe a bit more esoteric since we don’t teach that stuff in Prolog courses. A set of definite clauses is a set of first-order formulae in Skolem Standard Form (SSF). To put a formula in SSF one begins by putting the formula in Prenex Normal Form. To put a formula in Prenex Normal Form one begins by putting the formula in Conjunctive Normal Form (CNF) and moving all the quantifiers to the prenex of the formula (i.e. at the front). Now, a set of formulae in CNF is a conjunction of disjunctions. The disjunctions are the clauses, the conjunction is the logic program. So a logic program is a conjunction of clauses.

But, like I say above and felix.weitkaemper points out, that a set of definite clauses is formally a conjunction is not the whole story: this is just the declarative semantics. There is also a procedural semantics, which describes the flow of control through a Prolog program. And in that setting, clauses are selected one-by-one for execution by the Prolog runtime, depending on unification, so they don’t always all “fire”. The upshot of this is that when you enter a query at the top-level you only get some subset of the logical consequences of the definite clauses in the logic program.

So just to be clear, my argument is that there are two readings of a set of definite clauses, the declarative one, which is the formal one that jives with FOL; and the procedural one that makes more sense with respect to the experience of programming in Prolog, and running Prolog programs. I prefer the formal semantics because it connects to other areas of predicate logic but I can’t completely dismiss the procedural semantics. You need both to understand Prolog, as usual.

I apologise in advance if there are mistakes above. It’s getting late. Hopefully I won’t read tomorrow what I wrote today and pull my hair out in shame. I usually manage to insert some stupid mistake somewhere. It’s because I’m half were-coyote.

Good night!

Yeah, this is the argument put forward by the bot, about the distributivity of implication over disjunction and conjunction. I don’t have the energy to engage with it right now without making a complete mess of it but I think it’s useful to think that way; although the entire idea of distributivity was news to me I have to confess. I guess it never comes up in logic programming (and I rarely read anything in logic that isn’t logic programming; my bad).

I don’t see a contradiction in Prolog, which is e.g. happy to succeed more than once.

Do you have an example Prolog program in which an intended OR turns into an AND, or vice versa? :grinning_face:

I agree - e.g. all programs have a concept of acceptable execution time.

The contradiction I point out is in that the Least Herbrand Model of a set of definite clauses is, by definition, their least Herbrand model. If there’s a smaller one, then the LHM is not least. Which contradicts the definition.

When you backtrack you are getting more of the logical consequences of a set of clauses, the ones that match your query. If you make a query with all the arguments unbound, you eventually get all the logical consequences of the set of clauses. That’s a conjunction. If it was a disjunction, you’d only get some of them.

I don’t understand what that means. What is an “intended OR”?

All I’m saying is that, formally speaking, in predicate logic, a set of definite clauses is a conjunction but in Prolog it can look like a disjunction, which is not quite right.

Maybe I should give a simple example in code? Consider this:

fruit(apple).
fruit(banana). 
fruit(durian).

Now, when we query fruit(X) at the top level we’ll get answers like:

% Made up by hand
?- fruit(X).
X = apple ;
X = banana ;
X = durian.

What does that mean? Are the X’s alternatives? Does our program say that “An apple is a fruit OR a banana is a fruit OR a durian is a fruit”?

Or does it say “An apple is a fruit AND a banana is a fruit AND a durian is a fruit”?

I’d say clearly the latter. They’re all fruit. That’s because X is implicitly universally quantified, so all the Xs in fruit(X) are fruit and not just some of them. For all X, fruit(X) is true whenever X is a fruit. That’s a conjunction, not a disjunction.

The OR relation also holds - but that’s a special case again. If A AND B is true then A OR B is true, too, but the conjunction is a stronger constraint on the meaning of the sentence.

The output is showing semicolons separating the alternatives: ;/2 which is specified as disjunction i.e. OR.

We can say “this is a solution, AND that is also a solution”, but I think that’s just because English is a flexible and inexact language :grinning_face: E.g. people say “sick” to mean good, and say “literally” purely for emphasis.

AND seems inapplicable, because a fruit cannot simultaneously be an apple and a banana.

My non-logician take:

Or does it say X is a fruit if X is an apple OR X is a fruit if X is a banana OR X is a fruit if X is a durian ? X is universally quantified but it is just one “thing”, not all fruits.

If multiple clauses with the same functor/arity is not a disjunction in Prolog, how would I express a disjunction in Prolog? (And I don’t think it has anything to do with declarative or procedural semantics.)

I also think words matter so we need to clearly define what is meant by rule, clause, predicate, axiom(?), etc. The actual meaning seems to vary with context (to a non-logician).

That’s more confusion still but what the “;” means at the top-level is “redo” not "or’. It’s the same symbol as ;/2 but it’s not ;/2. You can see that if you press “h” at the top-level after the first result before pressing “;”. You get this help text that says that “;” means “redo”:

  Possible actions:
  ; (n,r,space,TAB): redo              | t:           trace&redo
  *:                 show choicepoint  | . (c,a,RET): stop
  w:                 write             | p:           print
  +:                 max_depth*5       | -:           max_depth//5
  b:                 break             | h (?):       help

And you can also redo by pressing n,r space or tab, which unlike “;” don’t have synonymous built-ins.

A single fruit is not simultaneously different fruit, yes, but the set of all fruit includes apple, banana and durian (in my example). The thing to keep in mind is that in fruit(X), the “X” is a universally quantified variable so fruit(X) it’s true for all values of X. Universal quantification clearly shows a conjunction.

For example, if someone says that X is universally quantified over the set {a,b,c} you can replace every occurrence of the variable X with the sentence a AND b AND c and that will not change the meaning of the original sentence. But you can’t change it with a OR b OR c because that will change the meaning.

That’s right, a FOL sentence can take many different meanings when translated to natural language. But when we say that a set of clauses is a conjunction, that’s unambiguous. Equally so when we say it’s a disjunction. But it can’t be both.

That’s right, each value that X can take is one fruit; but the set of all values of X is a conjunction because fruit(X) is true for all the X. If the set was a disjunction, fruit(X) could be true for only some values of X. Then X would be existentially quantified.

But like I say above a set of definite clauses is a set of logic formulae in Skolem Standard Form which means that all the quantifiers are explicitly replaced by the universal quantifier. Although of course, just to make matters even more confusing, when a query like fruit(X) succeeds at the top-level that’s a proof that there exists an X such that fruit(X) is true. I know.

Well I was just reading The Craft of Prolog by O’Keefe because I was curious to see whether he discusses this at all. It turns out the only place I could find the word “disjunction” was with respect to the if-then-else structure with ->/2 and ;/2, for example:

% This is an if-then-else: (if a then b; else c)
(   a
->  b
 ;  c
)

Or, more simply:

% This is a disjunction
a
; 
b

So the question now is, if a set of clauses is already a disjunction, then why do we need an explicit disjunction operator (as in ;/2)?

It really, really shouldn’t. That’s the one thing that causes so much pain when trying to learn or teach Prolog.

To give you an example, when I started learning Prolog I was very confused about what is a “predicate”. I looked at a Prolog programs and saw facts and rules and I was taught that those are “predicates”. OK. Then I looked at the top-level and saw queries that looked exactly the same as those other “predicates”. But those can’t be predicates, right? They’re queries. Then, if a set of rules with the same functor/arity are predicates, what are the individual rules? Are they predicates, too? And what are the “clauses”? Are they the same as “rules”? Or the same as “facts”? Facts can’t be “clauses”, can they? I was tying myself up in knots like that until I found online the free copy of “Prolog for Natural Language Analysis” by Pereira and Shieber (http://www.mtome.com/Publications/PNLA/prolog-digital.pdf) and that has a good and clear explanation of what definite clauses are (because it speaks about DCGs) which helped me a lot to understand what’s what.

All this is totally the fault of the Prolog community, the textbooks and the tutors. I think everyone is constantly worrying that Prolog is too hard and that students won’t get it if we introduce it in all its complexity, so everyone is constantly trying to fudge things up - like the bit about sets of clauses being “alternatives”. This works up to the point where a student wants to go a bit deeper and tries to connect what they know about Prolog with what they know about logic… and get horribly, terribly confused because nothing quite makes sense anymore. See my comment above about the difference between the way we treat predicate and function symbols in FOL and in Prolog.

This is further complicated by the fact that Prolog has borrowed terminology from different communities. For example “rule” and “fact” comes AFAICT from Charles Sanders Pierce, who set the foundation of FOL along with Gotlob Frege in the 1920’s. “Query” is obviously a database term. “Clause” and is probably from predicate logic but later than Pierce and Frege. I have no idea where “predicate” comes from. “Axiom” is obviously from mathematics. It’s Greek so it probably goes all the way back to Aristotle. We don’t use “axiom” very often in Prolog though. That the rules and facts in a logic program are the axioms of a theory is something to say when explaining Prolog in terms of more general logic terms.

A clause in Prolog is a definite clause, either a definite program clause or a Horn goal (others call that a definite goal). A definite program clause is also called a “rule” if it has one or more body literals, or a “fact” otherwise. A Horn goal is also called a “query”. “Predicate” should really be reserved for functor symbols but that horse has bolted. See my earlier comment.

A redo is an OR :joy:

I suppose this is as plain as possible:

?- (X = apple , X = banana).
false.
?- (X = apple ; X = banana).
X = apple ;
X = banana.

i.e.:

  • X has the value apple
  • OR X has the value banana

Not simultaneously.

Just seen this interesting tidbit:

The kind of logic used by Prolog is a subset of First Order Logic called quantifier-free Horn Clause Logic. As the name suggests, there are no existential or universal quantifiers. Instead, any variable is implicitly assumed to be universally quantified.

Regarding the issue of whether clauses are in a conjunction or a disjunction, I agree with stassa.p and felix.weitkaemper that it is a conjunction. Prolog syntax was derived from conjunctive normal form (CNF), where one reduces an FOL formula to a conjunction of disjunctions (using skolemization etc.). I.e., to:

( ~m(X) v n(Y) v ~s(X) v ... ) ^ ( ... v ... ) ^ ( ... v ... ) 

Each element of this conjunction is called a clause. In principle in (C)LP one considers only Horn clauses, which are clauses with just zero or one non-negated literals. E.g.:

( p([H|T]) v ~q(H,Y) v ~r(Y) v ~p(T) ) ^ ( p([]) ) ^ ... 

Clauses with just one non-negated literal are facts. The original Prolog from Marseiiles used something very similar (positive and negative literals) but I believe it was Kowalski that suggested, in order to avoid all those negations, to use instead an implication (b v ~a ==> b ← a):

( p([H|T]) <- q(H,Y) ^ r(Y) ^ p(T) ) ^ ( p([]) ) ^ ...

Prolog syntax then simplifies a bit for the keyboard by using commas for the inner conjunctions, :- for the implication, and periods, in place of the outer conjunctions, to separate the clauses, i.e.:

p([H|T]) :- q(H,Y), r(Y), p(T). 
p([]).
...

I also agree with stassa.p that the reason we view clauses of the same predicates as alternatives comes from resolution (a.k.a., the procedural semantics). But I think it is all still totally within logic. Resolution proves by contradiction, i.e., it is trying to find a contradiction in (actually, counter examples to) the negation of what we want to prove, and this flips the perception of the conjunction into a ‘disjunction’: to prove that a conjunction is false we can prove either one of the conjuncts to be false, i.e., the clauses are ‘alternatives’, and we tend to read the programs that way.

Btw, in addition to the very good books already mentioned, I would like to mention the excellent classic by Gallier (Jean Gallier's Home Page for logic book). Let me also mention the different materials on logic, resolution, and Prolog in our course-related web pages: Computational Logic / Prolog Course Material and Tools The more theoretical parts are a bit rusty (teaching leans much more to the practical side nowadays, so we start with Prolog right away :slight_smile:) but should still cover some bases.

Agreed.

I don’t remember seeing the Gallier book before. Thanks for the links. Btw is the University of Madrid still teaching Prolog or did it give up like many others?

I’m not sure I agree. A redo is when the interpreter backtracks to the last choice point to explore another branch. If a new answer is found in that branch we can see it as a conjunct or a disjunct. But this is what we’re trying to decide, right?

I think this means that the program logic could be expressed in more than one way, having different arrangements of conjunctions and disjunctions. That’s fair enough.

Is it correct to call this a contradiction? (I assume not, but have no idea.)

I hesitate to pursue this further to avoid confusing myself but we don’t need to use an operator to get disjunction, just the “predicate”:

;(Goal1,_) :- Goal1.
;(_,Goal2) :- Goal2.

Perhaps this works because two clause instances with the same functor/arity is a disjunction? Defining the operator is just syntactic sugar, rather than the more clumsy (IMO) ;(Goal1,Goal2). But I think this is seldom used due to the disjunction semantics “built-in” to multiple clauses with the same functor/arity ( predicate?).

Also note the SWI-Prolog doc for ;/2 does define it as disjunction, as does the ISO standard (Sect 7.8.6), so it does seem to be pretty well entrenched in Prolog. You might deem that incorrect based on some meta-interpretation of a Prolog program, but I think you’re swimming upstream.

And I may be wrong but isn’t interpreting X as a set of values some version of a second order logic?