Definability of Horn Revision from Horn Contraction

Abstract

In the AGM framework [Alchourron and Makinson, 1985], a revision function can be defined directly through constructions like systems of spheres, epistemic entrenchment, etc., or indirectly through a contraction operation via the Levi identity. A recent trend is to construct AGM style contraction and revision functions that operate under Horn logic. A direct construction of Horn revision is given in [Delgrande and Peppas, 2011]. However, it is unknown whether Horn revision can be defined indirectly from Horn contraction. In this paper, we address this problem by obtaining a model-based Horn revision through the model-based Horn contraction studied in [Zhuang and Pagnucco, 2012]. Our result shows that, under proper restrictions, Horn revision is definable through Horn contraction via the Levi identity.