We investigate a formula-based approach for updating ABoxes in DL-Lite(ℋℱ) horn , a description logic that enjoys a low computational complexity of reasoning. Specifically, we extend the existing coherence update semantics from DL-Lite(ℋℱ) core to deal with conjunctions on the left-hand side of TBox axioms, which introduce ambiguity in the update result. We address this problem by proposing the new prioritized coherence update semantics that employs rankings over conjuncts to select among competing updates while preserving the central properties of minimal change, syntax independence, and uniqueness. We further show that updated ABoxes can be computed via a stratified Datalog¬ program based on a novel consequence-based calculus. The approach runs in polynomial
time, matching the complexity of standard reasoning in DL-Lite(ℋℱ )horn .