Horn Clause - Artificial intelligence Tutorial
Clause:-
a clause is an expression formed from a finite collection of literals . That is, it is a finite disjunction or conjunction of literals, depending on the context.Definition:
horn clause is a disjunction of literal in which at most one positive literal.Example:-
~X1 V ~X2 V……..V~Xn V Y
Example :-
{~lawyer(x),rich(x)}
Every Horn clause can be written as an implication whose
premise(base) is a conjunction of positive literals and whose conclusion is a
single positive literal. E.g. lawyer(x) Þ
rich(x)
Related Other Post
Any Horn clause therefore belongs to one of four categories:
- Horn clause with exactly one positive literal(1 positive literal, at least 1 negative literal) called definite clause.an implication often called A “rule”. whose antecedent(left side) consists of a conjunction of positive literals and whose consequent(right side) consists of a single positive literal. Example:- "~P1 V ~P2 V ... V ~Pk V Q". This is logically equivalent to "[P1^P2^ ... ^Pk] => Q"; Examples: "~parent(X,Y) V ~ancestor(Y,Z) V ancestor(X,Z)" (If X is a parent of Y and Y is an ancestor of Z then X is an ancestor of Z.)
- A definite clause with no negative literals simply asserts a given proposition called fact .in another words 1 positive literal, 0 negative literals called fact. Example: "ancestor(X,X)" (Everyone is an ancestor of themselves .
- A clause with zero positive literals called negated
goal . in another words 0 positive literals, at least 1 negative literal.
In virtually all implementations of Horn clause logic, the negated goal is the
negation of the statement to be proved; the knowledge base consists entirely of
facts and goals. The statement to be proven, therefore, called the goal, is
therefore a single unit or the conjuction of units;
an existentially quantified variable in the goal turns into
a free variable in the negated goal. E.g. If the goal to be proven is
"exists (X) male(X) ^ ancestor(elizabeth,X)" (show that there exists
a male descendent of Elizabeth) the negated goal will be "~male(X) V
~ancestor(elizabeth,X)".
- The null clause: 0 positive and 0 negative literals. Appears only as the end of a resolution proof.
0 Comments
if u have any doubts please let me know,