Model-based Algorithm for Belief Revisions between Normal Conjunctive Forms

Abstract

Belief revision is a central area in knowledge representation and processing of automated reasoning. We will consider a knowledge base (KB) K and a new information φ, both expressed in conjunctive form(CF). We present here, a novel, deterministic and correct algorithm for belief revision of φ in K. We denote our revision operator as: K 0 = K ◦ φ. We introduce a new logical binary operator Ind between two conjunctive forms, such that Ind(φ,K) generates also a conjunctive form. The operator Ind(φ,K) works building independent clauses with the clauses of K, and whose falsifying assignments of the resulting formula cover exactly the space of assignments Fals(φ) − Fals(K), this is essential for performing the process of belief revision K 0 = K ◦ φ, where K 0 |= φ. Furthermore, our proposal satisfies the KM postulates. We also present the correctness proof of our belief revision method, and the analysis of its time complexity.