Revision specifications by means of programs

We propose a formahsm for specifying revisions in knowledge bases and belief sets. This formalism extends logic programming with stable model semantics. Main objects of our system are revision programs consisting of revision rules. A revision rule expresses a specification of change or a constraint on a knowledge base. There are two types of revision rules. In-rules require that an element be in a knowledge base whenever some other elements are in the knowledge base and yet other elements are absent from it. Similar conditions in an out-rule force the absence of an element from the knowledge base. For a revision program P we introduce the notion of a P-justified revision, which we use to specify the meaning of the program. Main motivation for our formalism and for the semantics of P-justified revisions comes from default logic and logic programming with stable model semantics. In the paper, we show that if a knowledge base B is a model of a program P then B is the unique P-justified revision of B. We show that P-justified revisions are models of P. We also show that P-justified revisions of a given knowledge base satisfy some minimality criterion. We outline the proof theory for revision programs gad show its adequacy for the proposed semantics. We generalize the notion of a revision program to the case of disjunctive revision programs. A simple example of an application is also discussed.