A logic model for maintaining consistency of bureaucratic policies

A logic model based on Horn clause logic and deontic logic is presented. It attempts to formalize policies suitable for automated reasoning. Consistency of the policies is defined based on a set of meta-level logical statements called integrity constraints that must be satisfied in all evolutionary phases of the policies. Inconsistencies can be detected if any of the integrity constraints is proven false, and an explanation can be provided based on the proof tree. A more general inference mechanism is presented based on the theory of abduction for checking potential inconsistency of policies