A Revision System Based on Delegate Model for Propositional Logic

Problem of belief revision and specification evolution has been studied for years. Researchers have proposed ACM theory and R-calculus to solve the problem. This paper concerns with the revision of proposition logic and proposes a revision algorithm which can automatically find out a revision of given sets. The correctness of the algorithm is proved and concepts such as basic proposition, assignment equivalence relation and delegate model are introduced. Tactics are used to improve the efficiency of the revision algorithm. A revision system is realized based on the improved algorithm. And an example is run to illustrate the syntax and the property of the system.