The three most common representations of states in iterated belief revision are compared: explicit, by levels and by history. The first is a connected preorder between models, the second is a list of formulae representing equivalence classes, the third is the sequence of the previous revisions. The latter depends on the revision semantics and on history rewriting, and the latter depends on the allowed rewritings. All mechanisms represent all possible states. A rewritten history of lexicographic revision is more efficient than the other considered representations in terms of size with arbitrary history rewritings. Establishing the redundancy of such a history is a mild rewriting. It is coNP-complete in the general case, and is hard even on histories of two revisions or revisions of arbitrary length of Horn formulae, and is polynomial on histories of two Horn formulae. A minor technical result is a polynomial-time algorithm for establishing whether a Horn formula is equivalent to the negation of another Horn formula.
翻译:本文比较了迭代信念修正中三种最常见的状态表示方法:显式表示、分层表示和历史表示。第一种是模型之间的连通预序,第二种是表示等价类的公式列表,第三种是先前修正操作的序列。历史表示依赖于修正语义和历史重写,而历史重写又依赖于允许的重写规则。所有机制都能表示所有可能的状态。在具有任意历史重写的条件下,词汇修正的重写历史在规模上比其它考虑的表示方法更高效。判断此类历史的冗余性属于轻度重写问题。在一般情况下,该问题为coNP-完全问题,即使在仅包含两次修正操作的历史或任意长度的Horn公式修正历史上也是困难的,但在仅涉及两个Horn公式的历史上则为多项式时间可解问题。一个次要技术成果是提出了一种多项式时间算法,用于判断一个Horn公式是否等价于另一个Horn公式的否定形式。