ABSTRACT
This chapter discusses stable model semantics by the so-called fixpoint completion of programs. It enables the readers to draw almost effortlessly a number of corollaries on the stable model semantics, and provides some additional observations on stratification and the perfect model semantics. The fixpoint completion is a program transformation which is based on the notion of unfolding, meaning the replacement of a body atom by the body of a clause which also has head. In essence, the fixpoint completion of a given program is obtained by performing (recursively) a complete unfolding through all positive body atoms and disregarding all clauses which after this process still contain positive body atoms. The chapter describes an iterative method for obtaining the perfect model for locally stratified programs. Since locally stratified programs are a generalization of locally hierarchical programs, it is clear that each locally hierarchical program has a unique perfect model.
