A decomposition based algorithm for maximal contractions

Abstract

This paper proposes a decomposition based algorithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satisfiability of formulas. The satisfiability of a formula is equivalent to the satisfiability of a set of literal sets. A decomposing function is constructed to calculate all satisfiable literal sets of a given formula. When expressing the satisfiability of a formula, these literal sets are equivalent to all satisfied models of such formula. A revision algorithm based on this decomposing function is proposed, which can calculate maximal contractions of a given problem. In order to reduce the memory requirement, a filter function is introduced. The improved algorithm has a good performance in both time and space perspectives.

Keywords

belief change / maximal contraction / decomposing rules / revision algorithm

References

[1] Li W. A logical framework for evolution of specifications. In: Proceedings of the 5th European Symposium on Programming. 1994, 4: 394-408

[2] Li W. Logical verification of scientific discovery. Science China Information Sciences, 2010, 53(4): 677-884

[3] Jiang D, Lou Y, Jin Y, Luo J, Li W. A representative model based algorithm for maximal contractions. Science China Information Sciences, 2013, 56(1): 1-13

[4] Alchourrón C, Gärdenfors P, Makinson D. On the logic of theory change: partial meet contraction and revision functions. Journal of Symbolic Logic, 1985, 50(2): 510-530

[5] Katsuno H, Mendelzon A O. A unified view of propositional knowledge base updates. In: Proceedings of the 11th International Joint Conference on Artificial Intelligence. 1989, 1413-1419

[6] Darwiche A, Pearl J. On the logic of iterated belief revision[j]. Artificial Intelligence, 1997, 89: 1-29

[7] Dalal M. Investigations into a theory of knowledge base revision: preliminary report[c]. In: Proceedings of the 7th National Conference on Artificial Intelligence. 1988, 8: 475-479

[8] Nebel B. Belief revision and default reasoning: Syntax-based approaches. In: Proceedings of the 2nd International Conference on Principles of Knowledge Representation and Reasoning. 1991, 4: 417-428

[9] Delgrande J P, Schaub T. A consistency-based approach for belief change. Artificial Intelligence, 2003, 151(1): 1-41

[10] Li W. A development calculus for specifications. Science in China Series F: Information Sciences, 2003, 46(5): 390-400

[11] Li W. R-calculus: An inference system for belief revision. The Computer Journal, 2007, 50(4): 378-390

[12] Luo J, Li W. An algorithm to compute maximal contractions for horn clauses. Science China Information Sciences, 2011, 54(2): 244-257

[13] Luo J. A general framework for computing maximal contractions. Frontiers of Computer Science, 2013, 7(1): 83-94

[14] Luo J, Li W. R-calculus without the cut rule. Science China Information Sciences, 2011, 54(12): 1-14

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg