Page 105 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS

Unit 6: Formalized Symbolic Logics

Horn clauses are clauses that have one or zero positive literals. Sets of Horn clauses are also Notes
called Horn.

Example 2:
~taller(Y,x(Y)) | wise(Y) | ~wise(x(Y))
~wise(geoff) | ~taller(Person,brother_of(jim))
are Horn clauses. Written in Kowalski form, these Horn clauses are:
taller(Y,x(Y)) & wise(x(Y)) => wise(Y)
wise(geoff) & taller(Person,brother_of(jim)) => FALSE
Non-Horn clauses are clauses that have two or more positive literals. Sets of clauses that contain
one or more non-Horn clauses are also called non-Horn.

Example 3:
~taller(Y,x(Y)) | ~wise(Y) | wise(x(Y)) | taller(x(Y),x(x(Y)))
wise(X) | wise(brother_of(X))
are non-Horn clauses. Written in Kowalski form, these non-Horn clauses are:
taller(Y,x(Y)) & wise(Y) => wise(x(Y)) | taller(x(Y),x(x(Y)))
TRUE => wise(X) | wise(brother_of(X))

Self Assessment

State whether the following statements are true or false:
7. Clause Normal Form (CNF) is a sub-language of 1st order logic.

8. Clauses are denoted by lowercase letters with a superscript.

6.5 Inference Rules

In terms of ATP, the disjunction of positive literals in non-Horn clauses corresponds to a choice
point in any goal directed search. This is a source of search. Thus, in general, Horn problems are
easier than non-Horn problems. In logic, a rule of inference, inference rule, or transformation
rule is the act of drawing a conclusion based on the form of premises interpreted as a function
which takes premises, analyzes their syntax, and returns a conclusion (or conclusions).

Example: The rule of inference modus ponens takes two premises, one in the form of “If
p then q” and another in the form of “p” and returns the conclusion “q”.
The rule is valid with respect to the semantics of classical logic (as well as the semantics of many
other non-classical logics), in the sense that if the premises are true (under an interpretation)
then so is the conclusion. Typically, a rule of inference preserves truth, a semantic property. In
many-valued logic, it preserves a general designation. But a rule of inference’s action is purely
syntactic, and does not need to preserve any semantic property: any function from sets of
formulae to formulae counts as a rule of inference. Usually only rules that are recursive are
important; i.e. rules such that there is an effective procedure for determining whether any given
formula is the conclusion of a given set of formulae according to the rule. An example of a rule
that is not effective in this sense is the infinitary ω-rule.

LOVELY PROFESSIONAL UNIVERSITY 99