The notion of logical difference plays an important role in characterizing substantial difference among logic-based knowledge bases that suffer from dynamic changes continuously.This notion is also closely related to forgetting,which has been extensively explored in various logics.This paper presents three notions of difference over a relevant signature for propositional theories—logical difference,clausal difference and prime difference,to capture the difference of logical consequence,clause consequence and prime clause consequence respectively.Besides,their properties and computational complexities are also investigated.It is shown that various deciding problems involving logical difference are one level higher in the polynomial hierarchy than their corresponding satisfiability problem,except for 2-CNF theories for which these deciding problems are tractable.Extensive experimental results on random 3-CNF,2-CNF and Horn theories reveal some interesting phenomena on clausal difference and prime difference.In particular,the number of clauses in both clausal and prime difference exhibits a similar phase transition with their satisfiability for both random 3-CNF theories and 2-CNF theories.However,for random Horn theories,while the number of clauses in clausal difference exhibits a similar coarse phase transition with its satisfiability,the number of clauses in prime difference behaves quite differently from that of clausal difference.It reveals a new character of satisfiability phase transition for random 3-CNF and 2-CNF theories,that their evolutions will introduce more different knowledge nearby their phase transition thresholds.
维普
万方数据