Program completion in propositional logic
Christopher John Hogger · 1990
Abstract The completion of a program P is a particular set of sentences which we denote by Comp(P). In some texts you will find it called instead the completed database of P and denoted there by CDB(P). Like the construction CW A(P), the completion provides a consequenceoriented meaning for default inference under the closed-world assumption. Unlike CW A(P), however, it can be written down more-or-less directly and is consistent for all well-structured programs. In general it is also a more economical construction in that it implies, but does not necessarily declare, various negative propositions which CW A(P) would have to declare explicitly. In the case of propositional logic the construction is particularly simple: