How is predicate logic represented in Prolog?

Question

may be a strange and broad question and not a 100% programming question, but I hope this is ok. I recently had a discussion about, that a lot of programs in Prolog don´t follow strict predicate logic (of Frege) but often are "object oriented" which I am trying to grasp.

I know that Prolog is based on first order predicate logic especially Horn Clauses and that they are a special form of modus ponens. A fact and a rule if they occur solo are simply clauses, but as soon as I add more than one occurrence they become a predicate.

How are the quantors of first order predicate logic represented and related to fact , rule , predicate or the Prolog concept in general? What does the functor express and what the arguments in relation to predicate logic. How is predicate logic and first order predicate logic reflected in Prolog and where does prolog leave their concepts? e.g. how would I define a point, a line and a vertical line in predicate logic and first order predicate logic.

How do I formulate this in predicate logic and first order predicate logic what is the semantic and logic difference between

vertical(line).
line(vertical).

Or a line and point in this example. Are point and line not predicate logic? For me it is " point(X) the set of all points" and when I pick a concrete point "there exists one point(110, 12)."

point(X,Y).
line(point(W,X), point(Y,Z)).

vertical(line(point(X,Y), point(X,Z))).
horizontal(line(point(X,Y), point(Z,Y))).

Any info helps! Many thanks, H

Answer 1

A chapter of Programming in Prolog by W.Clocksin and C.Mellish is devoted to explain the relation of Prolog with logic. Citing from there

If we wish to discuss how Prolog is related to logic, we must first establish what we mean by logic. Logic was originally devised as a way of representing the form of arguments, so that it would be possible to check in a formal way whether or not they are valid. Thus we can use logic to express propositions, the relations between propositions and how one can validly infer some propositions from others. The particular form of logic that we will be talking about here is called the Predicate Calculus. We will only be able to say a few words about it here. There are scores of good basic introductions to logic you can turn to for background reading.

If we wish to express propositions about the world, we must be able to describe the objects that are involved in them. In Predicate Calculus, we represent objects by terms. A term is of one of the following forms:

• A constant symbol. This is a symbol that stands for a single individual or concept. We can think of this as a Prolog atom, and we will use the Prolog syntax. So greek, agatha, and peace are constant symbols.
• A variable symbol. This is a symbol that we may want to stand for different individuals at different times. Variables are really only introduced in conjunction with quantifiers, which are discussed below. We can think of them as Prolog variables and will use the Prolog syntax. Thus X, Man, and Greek are variable symbols.
• A compound term. A compound term consists of a function symbol, together with an ordered set of terms as its arguments. The idea is that the compound term represents some individual that depends on the individuals represented by the arguments. The function symbol represents how the first depends on the second. For instance, we could have a function symbol standing for the notion of "distance" and two arguments. In this case, the compound term stands for the distance between the objects represented by the arguments. We can think of a compound term as a Prolog structure with the function symbol as the functor. We will write Predicate Calculus compound terms using the Prolog syntax, so that, for instance, wife(henry) might mean Henry's wife, distance(point1, X) might mean the distance between some particular point and some other place to be specified, and classes(mary, dayafter(W)) might mean the classes that Mary teaches on the day after some day W to be specified.

Thus in Predicate Calculus the ways of representing objects are just like the ways available in Prolog.

Seems not appropriate to put the entire chapter here... there is also a program, very explanatory, in appendix B, that performs an automatic translation of WFFs into clauses.

The book is very readable, just a pity it's not among the titles in Free Prolog Programming Books section.

Answer 2

I know that Prolog is based on first order predicate logic especially Horn Clauses and that they are a special form of modus ponens.

In a sense, inverse "modus ponens":

a :- b

You want to show "a true", and to do so, you have to show "b true"

A fact and a rule if they occur solo are simply clauses, but as soon as I add more than one occurrence they become a predicate.

No, they are all predicates. The "predicate" is an object/agent/program/platonic-phenomenon which expresses that there (objectively) is some "relationship" between "things", and you can ask the Prolog Processor about that relationship. There is no direct meaning associated to all of that though, it's "strings related to strings via strings". We are working with syntactic machines after all (i.e. computers).

Enter this logic program:

p(x,y).   % Predicate p/2 states that there is a relationship p between x and y

And now, you can query the database about what the program is saying:

?- p(x,y).
true.        % a p relationship exists (fact, but could also be rule)

?- p(x,A).
A = y.       % the thing related to x via p is y

?- p(A,y). 
A = x.       % the thing related to x via p is y

?- p(A,B).
A = x,       % things related via p are x and y
B = y.

?- p(c,d).   
false.       % not REALLY "false" but "as far as I can tell, there
             % is no relationship p between c and d"

Note the interpretation of "false", which is not the "strong false" of classical logic. Even though it is traditionally state that Prolog works in classical logic, this is not really the case:

From "Logic Programming with Strong Negation" (David Pearce, Gerd Wagner, FU Berlin, 1991), appears in Springer LNAI 475: Extensions of Logic Programming, International Workshop Tübingen, FRG, December 8–10, 1989 Proceedings):

According to the standard view, a logic program is a set of definite Horn clauses. Thus, logic programs are regarded as syntactically restricted first-order theories within the framework of classical logic. Correspondingly, the proof theory of logic programs is considered as the specialized version of classical resolution, known as SLD-resolution. This view, however, neglects the fact that a program clause, a_0 <— a_1, a_2, • • •, a_n, is an expression of a fragment of positive logic (a subsystem of intuitionistic logic) rather than an implicational formula of classical logic. The classical interpretation of logic programs, therefore, seems to be a semantical overkill.

It should be clear that in order to explain the deduction mechanism of Prolog one does not have to refer to the indirect method of SLD-resolution which checks for the refutability of the contrary. It is certainly more natural to view Prolog's proof procedure as a kind of natural deduction, as, for example, in [Hallnäs & Schroeder-Heister 1987] and [Miller 1989]. This also is more in line with the intuitions of a Prolog programmer. Since Prolog is the paradigm, logic programming semantics should take it as a point of departure.

Now:

How are the quantors of first order predicate logic represented and related to fact, rule, predicate or the Prolog concept in general?

That is a long story. Note that Prolog is primarily about "programming using logic", and also about "modeling using logic". The two aspects certainly overlap well for problems that can be solved using explicit enumeration, but Prolog is not made for specifying general FOL constraints describing a sought-for solution. In fact, certain FOL constraints cannot be represented and other have to be transformed into nominally equivalent expression that are agreeable to the machine. Look up "skolemization". For example: https://www.cs.toronto.edu/~sheila/384/w11/Lectures/csc384w11-KR-tutorial.pdf

On the flip side, Prolog provides "meta-predicates" which generate solutions by calling other predicates, so it's making forays into second-order logic. As it must - nobody can survive in the FOL desert for long.

What does the functor express

Nothing. It just stands for itself. Pure syntax. Look up "Herbrand Universe".

How do I formulate this in predicate logic and first order predicate logic what is the semantic and logic difference between

vertical(line).
line(vertical).

It's you who imbues vertical and line with meaning. So, feelings. You want a "vertial line", so you would say, the "thing" is the "line" and "vertical" is an attribute of the "line". So vertical(line) sounds appropriate. Or maybe attribute(line,vertical). It depends.

Here:

point(X,Y).
line(point(W,X), point(Y,Z)).

You have to aspects:

Predicates express "relationships". "Function symbols" are used to construct "things with structure": you can form trees of stuff with function symbols on nodes and integers/strings/variables on leaves. These are called "term". But terms can appear as predicates or as things, depending on the context, it's quite fluid. So you can for example construct a Prolog program with another Prolog program.

point(X,Y)
line(point(W,X), point(Y,Z))

These are terms!

If you type this into a file program.pl:

point_on_line(point(X,Y),line(point(W,X), point(Y,Z))).

The terms appear as "things" related by predicate point_on_line/2. The whole line is itself a term.

If you type this into a file program.pl:

point(X,Y).
line(point(W,X), point(Y,Z)).

The terms appear as "predicates", and point appears both as predicate point/2 and as "thing" about which predicate line/2 is talking.

This is actually a vast subject and it takes some time getting used to it, much more than functional programming. I had some Prolog and Logic courses at uni but 20 years later I found out that I had badly misunderstood a lot of aspects.