AGM postulates are for belief revision （revision by a single belief）, and DP postulates are for iterated revision （revision by a finite sequence of beliefs）. R-calculus is given for R-configurations △｜Г, where ...AGM postulates are for belief revision （revision by a single belief）, and DP postulates are for iterated revision （revision by a finite sequence of beliefs）. R-calculus is given for R-configurations △｜Г, where △ is a set of atomic formulas or the negations of atomic formulas, and Г is a finite set of formulas. We shall give two R-calculi C and M （sets of de- duction rules） such that for any finite consistent sets Г, △of formulas in the propositional logic, there is a consistent set ⊙ Г C of formulas such that △IГ → △, ⊙ is provable and⊙ is a contraction of F by A or a minimal change of F by A; and prove that C and M are sound and complete with respect to the contraction and the minimal change, respectively.展开更多
This paper proposes a decomposition based algo- rithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satis- fiability of formulas. The satisfiability of...This paper proposes a decomposition based algo- rithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satis- fiability 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.展开更多
文摘AGM postulates are for belief revision （revision by a single belief）, and DP postulates are for iterated revision （revision by a finite sequence of beliefs）. R-calculus is given for R-configurations △｜Г, where △ is a set of atomic formulas or the negations of atomic formulas, and Г is a finite set of formulas. We shall give two R-calculi C and M （sets of de- duction rules） such that for any finite consistent sets Г, △of formulas in the propositional logic, there is a consistent set ⊙ Г C of formulas such that △IГ → △, ⊙ is provable and⊙ is a contraction of F by A or a minimal change of F by A; and prove that C and M are sound and complete with respect to the contraction and the minimal change, respectively.
基金This work was supported by the State Key Laboratory of Software Develop Environment Supported Project （SKLSDE- 2012ZX-18）, the National Natural Science Foundation of China （Grant No. 912183001） and the National High-Tech Research and Development Program （863） of China （2013AA01A212）.
文摘This paper proposes a decomposition based algo- rithm for revision problems in classical propositional logic. A set of decomposing rules are presented to analyze the satis- fiability 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.
