Mauricio Osorio, Juan Carlos Nieves, and Chris Giannella
We define a reduction system CS3 which preserves the stable semantics. This system includes two types of transformation rules. One type (which we call CS2) preserves the stable semantics regardless of the EDB (extensional database). So, it can be used at compilation time. The other (which we call CS1) does not preserve the stable semantics across changes to the EDB. Thus, it should be used at run time. Nonetheless CS1 can reduce the program size considerably and is quadratic time computable. Sometimes CS2 can transform a cyclic program into an acyclic one. At these times, a satisfi- ability solver can be used to obtain the stable models.