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
   108   109   110   111   112   113   114   115   116   117   118