Disjunctive logic program = Horn program + Control program

Abstract

This paper presents an alternative view on propositional disjunctive logic program: Disjunctive program = Control program + Horn program. For this we introduce a program transformation which transforms a disjunctive logic program into a Horn program and a so called control program. The control program consists of only disjunctions of new propositional atoms and controls the “execution” of the Horn program. The relationship between original and transformed programs is established by using circumscription. Based on this relationship a new minimal model reasoning approach is developed. Due to the transformation it is straightforward to incorporate SLD-resolution into the proof procedure.