Algorithms and application in decision-making for the finest splitting of a set of formulae

Belief revision, as one central problem in artificial intelligence, is of interest in decision-making and game theory. To deal with local belief change that is a desirable property for belief revision, a novel notion – the finest splitting was proposed by Parikh, Kourousias and Makinson, respectively. But it was not clear how to construct the finest splitting of a propositional theory (a closed set of propositional formulae). In this paper, we propose a constructive method, that is intractable generally, to compute the finest splitting of a propositional theory. We also propose a polynomial time algorithm to compute the finest splitting of a propositional theory consisting of clauses. As an application in the diagnosis theory, we show that, given a diagnosis system (SD,COMP,OBS)(SD,COMP,OBS), it is quite easy to compute all of its diagnosis if the splitting of SD∪OBSSD∪OBS is pre-computed. Additionally, in terms of this approach, we can have more specific reason to interpret observation than the original one.