ABSTRACT
The chapter presents various tools and techniques for representation of knowledge by propositions and predicates and demonstrates the scope of reasoning under the proposed framework of knowledge representation. It begins with the syntax and semantics of the logic of propositions, and then extends them for reasoning with the logic of predicates. Both the logic of propositions and predicates require the formulation of a problem in the form of a logical theorem and aim at proving it by the syntactic and the semantic tools, available in their framework. The ‘resolution principle’ is the most common tool that is employed for reasoning with these logics. To prove a goal, complex sentences are first represented in ‘clause forms’ and the principle of resolution is employed to resolve the members of a given set, comprising of the axiomatic rules (clauses) and the negated goal. One main drawback of the predicate logic lies in its semi-decidablity that fails to disprove a statement that does not really follow from the given statements. The chapter discusses all these in detail along with the formal proofs of ‘soundness’ and ‘completeness’ of the resolution principle.
