Updating knowledge bases II

We consider the problem of updating a knowledge base, where a knowledge base is realised as a (logic) program. In a previous paper, we presented procedures for deleting an atom from a normal program and inserting an atom into a normal program, concentrating particularly on the case when negative literals appear in the bodies of program clauses. We also proved various properties of the procedures including their correctness. Here we present mutually recursive versions of the update procedures and prove their correctness and other properties. We then generalise the procedures so that we can update an (arbitrary) program with an (arbitrary) formula. The correctness of the update procedures for programs is also proved.