Why do we call a disjunction of literals of which none is positive a goal clause?

Question

I think I know the meaning of goal clauses and horn clauses, but I'm quite confused about why people name a disjunction of literals of which none is positive a goal clause?

What's the goal here?

Answer 1

There are three types of Horn clauses

definite clause: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u
fact: u
goal clause: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t

which relate to Prolog.
Example Prolog from Adventures in Prolog

A definite clause is a Prolog rule:

where_food(X,Y) :-  
  location(X,Y),
  edible(X).

A fact is a Prolog fact:

room(kitchen).

A goal clause is a Prolog query:

location(X, kitchen), edible(X).

Another way of looking at three common with Prolog uses head, body and :-.

A rule is head :- body.
A fact is head.
A query is body.

A body is made up of calls to predicates (head), so a body can look like this A,B,C.

When you use a query it is really

goal :- body. 

or

goal <- A,B,C

or

location(X, kitchen), edible(X) ⊃ goal

A Prolog example

Facts

location(apple, kitchen).
location(crackers, kitchen).
location(flashlight, desk).

edible(apple).
edible(crackers).

Goal clause

location(X, kitchen), edible(X).

Answer

X = apple
X = crackers

Earlier answer

Starting with a predicate in Prolog

ancestor(X,Y) :- parent(X, Z) , ancestor(Z,Y).

where ancestor(X,Y) is know as the head clause and parent(X, Z) , ancestor(Z,Y) is known as the body.

Converting the Prolog to an implication
:- is ⊃
, is ∧
and the implication is reversed.

(parent(X,Z) ∧ ancestor(Z,Y)) ⊃ ancestor(X,Y) 

converting the conjunction (∧) of literals into a disjunction (∨) of literals

not parent(X,Z) ∨ not ancestor(Z,Y) ∨ ancestor(X,Y) 

results in not parent(X,Z) ∨ not ancestor(Z,Y) which is the Prolog body or in your question the goal clause.

In other words the goal clause are the statements that need to be satisfied in order to achieve the goal which is the Prolog head ancestor(X,Y).

To see an example of using the Prolog ancestor see Prolog/Recursive Rules. Note that the rule given in this example is only one of the two that are used to define ancestor with the missing Prolog rule being ancestor(A, B) :- parent(A, B).

References

The University of Edinburgh Course: Prolog Programming for Automated Reasoning students - Lecture 10 - Logic Programming

Goal clause definition from Wikipedia -

a Horn clause without a positive literal is sometimes called a goal clause
or ¬p ∨ ¬q ∨ ... ∨ ¬t

SWI-Prolog Glossary of Terms

Prolog/Recursive Rules

Foundations of Logic (WorldCat)

Try the Prolog online

Using swish (Prolog rules are already entered with this link)
In the lower right by ?- where it says your query goes here ... enter ancestor(X, john).
Then in the lower right click Run!
Above that you should see an ancestor of john
X=david
Under that click Next and you should see another ancestor of john
X=jim
keep clicking Next to see other ancestors and then finally you should see false meaning there are no more valid answers.

An excerpt

From Logic Programming by Frank Pfenning

To make the transition from inference rules to logic programming we need to impose a particular strategy. Two fundamental ideas suggest themselves: we could either search backward from the conjecture, growing a (potential) proof tree upwards, or we could work forwards from the axioms applying rules until we arrive at the conjecture. We call the first one goal-directed and the second one forward-reasoning.

How to search

OP comment

Could you tell me how you do such searches, 'cause when I run into some complex problems I usually don't know how to search necessary resources

Normally I would have the OP (original poster) ask that as another question, but since it is more of a subjective than objective question it will get shot down at SO (StackOverflow) with down and close votes and I can use examples related to the original question so I will answer it here.

When searching the path to success is to figure out the current terminology used by the experts in the area and which key words in that terminology are relevant to what you seek. Sometimes I know the key words off the top of my head, as with this question with disjunction of literals and goal I knew they were key terms in logic, reasoning, theorem proving and logic languages. Other times I am guessing or in the dark as with this question.

One way that sometimes yields success when trying to learn the current terminology is to search for review articles which typically have survey in the title and thus survey is a good keyword. e.g. using Semantic Scholar with horn clause survey finds on first page Constraint Logic Programming: A Survey

As an example of searching for the canonical form of math expressions with math canonical form little of relevance was found but after finding that standard from was more commonly used, better results were obtained.

Sometimes it is not words that help you find the answer and search engines that rely on words will fail you. For example a type of search I see every few weeks or so involves finding the pattern/formula/etc. that generates a sequence of numbers and you only know part of the sequence, and typically the start of the sequence. This is were a search using OEIS (The On-Line Encyclopedia of Integer Sequences®) comes in handy. Another type of search engine related to math is WolframAlpha. So be attentive to the fact that there are other kinds of search engines

Once you have the key words then as @WillNess notes you some times query for them as single words goal clause, but some times as exact words in quotes "goal clause". For this question using an exact word returned better results.

The next thing to realize is the source of the information often corresponds with quality of information.

• Sources from university courses, online digital scientific libraries and books are high on my list
• PDF (Postscript Document Format). The reason for PDF is that it is common to write technical professional papers with LaTeX which are then output as PDF. The old format was PS (PostScript) but I rarely see that with newer papers. Thus pdf is a good search term to add.
• Then sites from the creators such as Ubuntu, SWI-Prolog
• Sites that are obviously good such as w3schools
• Blog entries by the experts; most blogs are not by the experts.

Other search engines I use related to computer science technical papers are:

• CiteSeerX
• arxiv.org
• Google Scholar
• Microsoft Academic
• WorldCat
• Semantic Scholar
• dblp

and of course you can always query for other academic search engines

If you have only one or two documents that appeal to you but still don't have enough detail then start working down the references noted in those documents. This can be challenging as years ago many of the articles were only published in professional journals and are not freely available. However it is common to find those articles freely available if one of the authors is a professor and you can find the document listed under their public pages where they teach. CiteSeerX is really good for finding referenced documents.

If you are using an existing SO answer then check the tag to see if they are a top answerer and remember that the accepted answer may not be the best answer and that any answer may not be a correct answer to your question.

Then it is a matter of reading several of the articles to see what information is current and if there is consistency.

Some fields are moving fast and changing rapidly even in the time span of the last 20 years of the Internet. Here is an example where one paper made a significant change. If you are not aware of this paper in the area it relates you will probably be confused by research that happened before the paper and research based on the paper. To find such papers note the significant number of citations, at present 18658.

Don't be hesitant to spend upwards of an hour just searching and then a few more to a full day just reading. Here is a question I spent over four hours searching and reading and still could not find an answer. After finally running out of things to try I posted the question only to find it can not be done and is not documented. The answer was by someone I know to be an expert in F#.

Lastly don't be afraid to leave bread crumbs, e.g. your own personal notes as I do with Of interest: comments or in this question. You will often use the same search terms over and over again and if you have enough posted on the Internet will start to run into your own post. After a while you will realize that if you only left bread crumbs there it would have made your life easier.

The rest is just years of experience and diligence.

Also sometimes asking an SO question requesting help with which keywords to use sometimes gets answers and sometimes get shot down.

Answer 2

This is my personal understanding, but I'll do my best to relay it.

---

What's the intuition behind a 'goal clause'? Why call it that at all?

First let's confirm some definitions:

• A clause is defined as a disjunction of literals. Furthermore, since the disjunction operator is associative, that is, the following property applies:

  

  a clause can further be thought of as a disjunction of 'sub' clauses, that is, a clause like , could be 'split' into two parts representing "sub" clauses and

• a Horn clause is defined as a clause with at most one positive literal; as such, it can take three recognisable forms:

  1. the 'full' form: , which is known as a definite clause
  2. the form lacking any negative literals: , which is known as a factual clause (or simply a fact).
  3. the form lacking a positive literal: , which is known as a goal clause

If you compare forms 1 and 3, you will see that you could split form 1 into two parts (or sub-clauses): one clause which is essentially in the form of a 'goal clause', and one which is a standalone positive literal, which we will call the head.

Furthermore, this Horn clause can be rearranged into implication form as follows:

The implication form might also be referred to as a 'relationship', since, if we are given this particular horn clause as a premise, we are essentially being told that "it applies that if the first part is true, then the second must also necessarily be true".

The name goal clause should now start to make more sense. From the rules of natural deduction we know that, given , if we also manage to prove , then we can deduce . Therefore given a horn clause in implication form, which essentially reads "Goal implies Head", if we show that the "Goal" is true, we can logically conclude that the Head part must also necessarily be true. Therefore the "Goal" part of a Horn clause is the part for which we need to discover whether it is satisfiable or not, in order to conclude whether the Head is then true as a result.

Note that what I'm now referring to as "Goal" in this context is no longer in "clause" form, since the "Goal" is now in the form of a conjunction of (positive) literals, as opposed to a disjunction of literals. In effect, the logical statement that I'm now referring to as the "Goal" I'm trying to prove, is in fact equivalent to the negation of what we referred to earlier as the "Goal clause" (i.e. the statement formed by the disjunction of the negative literals). So we could think of the "Goal clause" as the relevant statement in clause-form, i.e. corresponding to the negation of the Goal we're trying to prove; it is the clause part of the Horn clause (when written in "clause" form) that gets negated, giving rise to the Goal component in the implication form.

---

But what's the point of even talking about Goals and Goal clauses. Do you ever get standalone "Goals" / "Goal clauses" in a database?

Sure. Note that a standalone "Goal clause" statement is equivalent to the statement "Goal implies False" (or more to the point, assuming the "Goal" is true proves nothing further / does not yield any more information). So a standalone "Goal clause" is essentially equivalent to a Goal without a Head, i.e. a Goal that when satisfied proves nothing else.

If we have a Goal without a Head, then we are essentially being asked to evaluate whether the Goal can be satisfied, but without relating this to a Head that needs to be deduced. The notion of having to evaluate a goal just for the fun of it might sound odd, but it starts making sense in Prolog terms, when you realise that some predicates cause side-effects to the system. So for instance, in Prolog, statements like these:

:- dynamic pred1, pred2.
:- writeln("I have just reached the end of the database file").

will be evaluated on the spot at the point of reading in the database (i.e. your prolog "script"), and have side-effects on the system, but without resulting in a fact or relationship entering the knowledge-database. In Prolog, such "headless" statements which are intended to be evaluated on-the-spot and cause side-effects to the runtime environment, are often called directives.

---

What's the relationship between a Goal clause and a Query? Are they the same?

Well, no. They're related. Specifically, a query is performed (under the hood) by attempting to prove that the Goal cannot be satisfied, i.e. we start by assuming it is false (or equivalently, that the Goal clause is true). Prolog then goes through the database, and tries to match the literals, or tries out substitutions, just like it would if it was trying to satisfy a Goal with the intent of deducing the Head of a definite clause. If we come across a substitution that satisfies this goal, then, in the context of the query, this leads to a contradiction. A query therefore reports the terms for which the negation of the goal under those substitutions leads to a contradiction. In other words, these substitutions are the ones for which the goal is satisfied.

EDIT: (addressing comments).

From wikipedia:

Execution of a Prolog program is initiated by the user's posting of a single goal, called the query. Logically, the Prolog engine tries to find a resolution refutation of the negated query. The resolution method used by Prolog is called SLD resolution. If the negated query can be refuted, it follows that the query, with the appropriate variable bindings in place, is a logical consequence of the program. In that case, all generated variable bindings are reported to the user, and the query is said to have succeeded

Here is an example of how a query might be implemented under the hood. Say you have the following knowledge-base:

a.        % premise 1
b :- a.   % premise 2
% ... plus many other facts and relationships not involving a or b

The prolog statement b :- a essentially corresponds to the logical statement a -> b, which is equivalent to the logical statement ¬a v b. So we are given ¬a v b and a as premises.

Now let's say you ask the following query:

?- b.

This is equivalent to saying "Hey, Prolog, is the statement b is true, true or false?"

It would be very inefficient to just start evaluating statements randomly to see if they happen to yield b is true as a result. So instead, in order to prove (in the mathematical sense) that b is true, Prolog reasons as follows: "I will instead start by assuming that b is in fact false, and start plugging it in, in the relevant premises. If this assumption forces a falsification in any of my premises which I hold to be true, then this proves that this assumption does not in fact hold, and therefore b is proven to be true."

Programmatically this might go like this:

• Step 1: Assume ¬b
• Step 2: Find all premises involving the literal b and test them
• Step 3: b takes part in premise ¬a v b. This needs to evaluate to true because it's a premise. Since b is assumed to be false, for this premise to evaluate to true, a needs to be false.
• Step 4: a is true (premise 1). This contradicts Step 3.

Therefore the assumption ¬b leads to a contradiction, and is therefore false. This proves the statement b is true.

This example only involved literals. When predicates with variables are involved, there may be some variable substitutions for which "¬b" leads to a contradiction in a similar way. Therefore we conclude that "b is proven to be true for the following substitutions", and Prolog will then report the relevant substitutions for which b is proven to be true.