Why do we call disjunction literals, none of which is a target position?
There are three types of Horn clause
A definite sentence: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t ∨ u
fact: u Purpose: ¬ p ∨ ¬ q ∨ ⋯ ∨ ¬ t
which are related to Prolog.
Example Prolog from Adventure in Prolog
A specific clause is the Prolog rule :
where_food(X,Y) :-
location(X,Y),
edible(X).
Fact is Prolog fact :
room(kitchen).
A goal proposal is a request:
location(X, kitchen), edible(X).
Another way to look at the three common uses Prolog uses head
, body
and :-
.
Rule head :- body.
Fact head.
Requestbody.
The body consists of calls to predicates (head), so the body might look like A,B,C
.
When you use query, it really is
goal :- body.
or
goal <- A,B,C
or
location(X, kitchen), edible(X) ⊃ goal
Prolog example
Facts
location(apple, kitchen). location(crackers, kitchen). location(flashlight, desk). edible(apple). edible(crackers).
Goal proposal
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 it ancestor(X,Y)
is known as the head and parent(X, Z) , ancestor(Z,Y)
is known as the body.
Conversion in Prolog implication :-
- ⊃
,
- ∧
and the implication is canceled.
(parent(X,Z) ∧ ancestor(Z,Y)) ⊃ ancestor(X,Y)
converting the conjunction (∧) of literals to the 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 body of Prolog or in your question about target.
In other words, goal clauses are statements that must be fulfilled in order to achieve the goal, which is the chapter of the Prologue 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 two that are used to define an ancestor with a missing Prolog ruleancestor(A, B) :- parent(A, B).
Links
University of Edinburgh Course: Prolog Programming for Students with Automated Investigation - Lecture 10 - Logic Programming
defining a target from Wikipedia -
a Horn clause without a positive literal is sometimes called a goal clause
or ¬p ∨ ¬q ∨ ... ∨ ¬t
SWI-Prolog Glossary of Terms
Try Prolog online
Using swish (Prolog rules are already entered using this link)
In the bottom right corner ?-
where it says your query goes here ...
enter ancestor(X, john).
Then in the bottom right corner click Run!
Above what you should see the ancestor john X=david
Under this click Next
and you will see another ancestor john X=jim
keep clicking Next
. to see other ancestors, and then finally you should see
false
means that there are no more reliable answers.
Excerpt
From Logic Programming by Frank Pfenning
To move from inference rules to logic programming, we need to enforce a certain strategy. Two fundamental ideas suggest themselves: we could either search backward from the hypothesis, a growing (potential) proof tree upward, or we could work forward from the axioms applying the rules until we arrive at the hypothesis. We invoke the first focused and second forward-thinking.
How to search
OP's comment
Could you please tell me how you do this kind of searches, because when I come across some tricky problems I usually don't know how to look for the resources I need
Usually I would like the OP (original poster) to ask this as a different question, but since this is more of a subjective than objective question, it will get knocked down on SO (StackOverflow) with an empty and close voice, and I can use the examples linked from the original question, so I'll answer it here.
When looking for a path to success, you should find out the current terminology used by experts in the field and what keywords in that terminology are relevant to what you are looking for. Sometimes I know keywords head-on, since with this question s disjunction of literals
and goal
I knew they are key terms in logic, reasoning, theorem proving and logical languages. In other cases, I am guessing or in the dark, as with this question.
One way that is sometimes successful when trying to learn current terminology is to search for article reviews , which usually have survey
a title and are therefore a survey
good keyword. for example using the Semantic Scientist with an overview of the horn sentence finds on the first page Programming Logic Constraint: an overview
As an example of searching for the canonical form of mathematical expressions with math canonical form
, little value was found, but standard from
better results were found after finding more frequent use .
Sometimes, it's not words that help you find the answer, and search engines that rely on words won't help you. For example, the type of search that I see every few weeks or so includes searching for a pattern / formula / etc. which generates a sequence of numbers and you only know part of the sequence and usually the beginning of the sequence. This is a search using the OEIS (Online Encyclopedia of Whole Sequences). Another type of math-related search engine is WolframAlpha . Therefore, be aware that there are other types of search engines.
Once you have the keywords, whereas @WillNess notes that you are querying for them multiple times as single words goal clause
, but multiple times as exact quoted words "goal clause"
. Better results were obtained for this question using the exact word.
The next thing to understand is that the source of the information often matches the quality of the information.
- Sources from university courses, online digital science libraries, and books high on my list
- PDF (Postscript Document Format). The reason for PDF is that it is customary to write professional technical documents with LaTeX , which are then output as PDF. The old format was PS (PostScript), but I rarely see this with new documents. Thus, it
pdf
is a good search term to add. - Then sites from creators like Ubuntu , SWI-Prolog
- Sites that are obviously good like w3schools
- Expert blog entries; most blogs are not experts.
Other search engines I use related to computer science:
and of course you can always ask for other academic search engines
If you only have one or two documents that appeal to you, but still do not have sufficient detail, then start working on the links indicated in these documents. This can be challenging since many of the articles were published only in professional journals many years ago and are not available. However, as a rule, these articles are freely available if one of the authors is a professor and you can find the document listed in 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 the top responder and remember that the accepted answer may not be the best answer, but that any answer may be the wrong answer to your question.
Then there are several articles to read to find out what information is relevant and if there is consistency. Some areas are moving rapidly and changing rapidly, even over the span of time spanning the last 20 years of the Internet.
Feel free to spend over an hour looking, and then a few more for a full day just reading. Here is the question I have spent over four hours searching and reading and still have not been able to find an answer. After finally running out to try it, I posted the question only to find it impossible to do and not documented. The answer was from someone I know as an expert in F #.
Finally, don't be afraid to leave bread crumbs, for example. your personal notes as I do with comments Of interest:
or in this question. You will often use the same search terms over and over, and if you have enough published on the Internet, it will start working in your own post. After a while, you will realize that if you left only bread crumbs, it would make your life easier.
The rest is years of experience and dedication.
Also sometimes asking an SO question asking for help on which keywords to use sometimes gets answers and sometimes gets confused.
source to share
This is my personal understanding, but I will do my best to convey it.
What is the intuition behind the "goal clause"? Why do you call it that?
Let's first confirm some definitions:
-
A clause is defined as a disjunction of literals. Moreover, since the disjunction operator is associative, i.e. The following property applies:
Further, the sentence can be considered as a disjunction of sentences "under", that is, a sentence of the type <Sub>
Sub> can be divided into two parts, representing the "sub-item" <Sub> 
Sub> and <Sub> 
Sub> -
A Horn clause is defined as a sentence containing at most one positive literal; as such, it can take three recognizable forms:
- "full" form: <Sub>
Sub>, which is known as a specific sentence - a form devoid of any negative literals: <Sub>
Sub>, which is known as an actual sentence (or just a fact). - a form with no positive literal: <Sub>
Sub>, which is known as a target clause
- "full" form: <Sub>
Sub> can be divided into two parts, representing the "sub-item" <Sub> 
Sub> and <Sub> 
Sub>
Sub>, which is known as a specific sentence
Sub>, which is known as an actual sentence (or just a fact).
Sub>, which is known as a target clauseIf you compare Forms 1 and 3, you will see that you can split Form 1 into two parts (or subclasses): one sentence that is basically a "goal sentence" and the other a stand-alone positive literal, which we will call a voice ...
In addition, this Horn sentence can be rearranged into an implication form as follows:
The form of implication can also be referred to as "relationship" because if we are given this particular horn sentence as a premise, we are essentially told that "it applies, if the first part is true then the second must necessarily be true."
Now the title purpose proposal should start to make more sense. From the rules of natural deduction, we know that, given <Sub> 
Sub>, if we also succeed in proving <Sub> 
Sub>, then we can deduce <Sub> 
Sub>. Therefore, given the position of the horn in the form of implication, which essentially says: "The goal implies the head", if we show that the "Goal" is true, we can logically conclude that the head must also be true. Therefore, the "Objective" part in Horn's sentence is the part for which we need to find out whether it is feasible or not, in order to conclude whether the result is true.
Note that what I now call "Target" in this context is no longer in "clause" form, as "Target" is now a concatenation of (positive) literals, as opposed to literal disjunction. In fact, the logical operator that I am now calling "Purpose", which I am trying to prove, is actually equivalent to negating what we talked about earlier as "Purpose Statement" (ie, a Statement formed by the disjunction of negative literals). Thus, we might think of a "goal proposition" as a corresponding statement in a clause-form, that is, to correspond to a denial of the goal we are trying to prove; it is the part of a sentence in a Horn sentence (when written in the "sentence" form) that becomes negative,which leads to a target component in the form of an implication.
But what is the point of talking about proposals of purpose and purpose. Have you ever got offline Goals / Goal Suggestions in the database?
Sure. Note that the stand-alone "Target Suggestion" statement is equivalent to "Target implies False" (or more, assuming "Target" is true, does not prove / provide any further information). Thus, the autonomous "goal position" is essentially equivalent to a headless goal, that is, a goal that, when satisfied, proves nothing.
If we have a goal without a head, then we are essentially asked to assess whether the goal can be satisfied, but without linking it to the head to be inferred. The notion of evaluating a goal just for fun may sound strange, but it starts to make sense in Prolog terms when you realize that some predicates cause side effects on the system. So, for example, in Prolog, statements like this:
:- dynamic pred1, pred2.
:- writeln("I have just reached the end of the database file").
will be evaluated in-place at the read point in the database (ie your "script" prologue) and have side effects in the system, but does not result in the fact or relations entering the knowledge database, In Prolog, such "headless" statements, that are intended to be evaluated in place and cause runtime side effects are often referred to as directives.
What is the relationship between Goal's proposal and Query? They are the same?
Oh no. They are connected. Specifically, the query is executed (under the hood) trying to prove that the goal cannot be fulfilled, that is, we start with the assumption that it is false (or, equivalently, that the Goal clause is true). The prolog then walks through the database and tries to match literals or checks for substitutions, just as if it was trying to satisfy a purpose in order to deduce the chapter of a particular sentence. If we come across a substitution that satisfies this goal, then in the context of the query it will lead to a contradiction. Therefore, the query specifies the conditions for which the negation of the target under these substitutions leads to a contradiction. In other words, these substitutions are the ones for which the goal is fulfilled.
EDIT: (addressing comments).
From wikipedia :
The execution of a Prolog program is initiated by a user posting a single target called a query. Logically, the Prolog engine tries to find a resolution rejection of the denied request. The resolution method used by Prolog is called SLD resolution . If a negative query can be refuted, it follows that the query with the appropriate variable bindings is a logical consequence of the program. In this case, all the generated variable bindings are reported to the user and the request is said to succeed
Here's an example of how a request might be implemented under the hood. Let's 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 run operator b :- a
essentially matches a boolean expression a -> b
, which is equivalent to a boolean expression ¬a v b
. Therefore, we are assigned ¬a v b
and a
how the premises.
Now let's say you make the following query:
?- b.
This is equivalent to saying, "Hello Prolog, is this a b is true
true or false statement ?"
It would be very inefficient to just start evaluating statements at random to see if they lead to a result b is true
. So instead of proving (in a mathematical sense) that b is true
, Prolog thinks like this: “Instead, I will start with the assumption of what is b
in fact false and start plugging it in the appropriate premises. assumptions that I believe to be true, then this proves that this assumption is actually not fulfilled, and therefore it is proved that b is true. "
It might look like this programmatically:
- Step 1: suppose ¬b
- Step 2: Find all rooms containing the literal
b
and test them - Step 3: b takes part in the room
¬a v b
. This must be judged to be true because it is a prerequisite. Since b is considered false, for this premise to evaluate to true, ita
must be false. - Step 4: a is true (premise 1). This is contrary to step 3.
Therefore, the assumption ¬b
leads to a contradiction and, therefore, is incorrect. This proves the statement b is true
.
In this example, only literals were involved. When variable predicates are involved, there may be some variable substitutions for which "¬b" results in a contradiction in a similar manner. Therefore, we conclude that "b is proven to be true for the following substitutions," and Prolog will then report the corresponding substitutions for which b is proven to be true.
source to share