Page 113 - DCAP310_INTRODUCTION_TO_ARTIFICIAL_INTELLIGENCE_AND_EXPERT_SYSTEMS
P. 113
Unit 6: Formalized Symbolic Logics
Generation of a resolvent from two clauses, called resolution, is the sole rule of inference of the Notes
resolution principle. The resolution principle is complete, so a set (conjunction) of clauses is
unclassifiable if the empty clause can be derived from it by resolution. Proof of the completeness
of the resolution principle is based on Herbrand’s theorem. Since unsatisfiability is dual to
validity, the resolution principle is exercised on theorem negations. Multiple strategies have
been developed to make the resolution principle more efficient. These strategies help select
clause pairs for application of the resolution rule. For instance, linear resolution is the following
deduction strategy. Let be the initial set of clauses. If , C ∈ S, a linear deduction of C from S with
o n
top clause C is a deduction in which each C is a resolvent of C and B (0 ≤ i ≤ n – 1), and each B
o i+1 1 1 i
is either in or a resolvent C (with j < i).
j
Linear resolution is complete, so if C is a clause in an unsatisfiable set S of clauses and S – C is
satisfiable, then the empty clause can be obtained by linear resolution with as the top clause. If
the additional restriction that B be in S imposed, then this restricted strategy is incomplete.
i
However, it is complete for sets of Horn clauses containing exactly one goal, and the goal is
selected as the top clause. All other clauses in such sets are definite Horn clauses. Implementations
of programming language Prolog conduct search within the framework of this strategy.
!
Caution Resolution principle can be applied in all situations.
Task Apply inference rule to declare today is hot or not.
Self Assessment
State whether the following statements are true or false:
11. A literal is a propositional variable or the negation of a propositional variable.
12. Unification is a key technique in proofs by resolution.
6.7 Deductive Inference Methods
Inference is the act or process of deriving logical conclusions from premises known or assumed
to be true. The conclusion drawn is also called an idiomatic. The laws of valid inference are
studied in the field of logic. Or inference can be defined in another way. Inference is the
non-logical, but rational, means, through observation of patterns of facts, to indirectly see new
meanings and contexts for understanding. Of particular use to this application of inference are
anomalies and symbols. Inference, in this sense, does not draw conclusions but opens new paths
for inquiry. In this definition of inference, there are two types of inference: inductive inference
and deductive inference. Unlike the definition of inference in the first paragraph above, meaning
of word meanings are not tested but meaningful relationships are articulated. Human inference
(i.e. how humans draw conclusions) is traditionally studied within the field of cognitive
psychology; artificial intelligence researchers develop automated inference systems to emulate
human inference. Statistical inference allows for inference from quantitative data.
6.7.1 Law of Detachment
In propositional logic is a valid, simple argument form and rule of inference. It can be summarized
as “P implies Q; P is asserted to be true, so therefore Q must be true.” The history of modus
LOVELY PROFESSIONAL UNIVERSITY 107