Stratified least fixpoint logic (Q1331926)

A close connection between logic programming and program verification is studied. The author proves the non-trivial fact that a logic which characterizes the expressibility of stratified logic programs (stratified least fixpoint logic -- SLFP) is equivalent to the formally continuous \(\mu\)-calculus. A complete sequent calculus (Gentzen-style deductive system) for SLFP is presented. Stratified logic programming enables us to use a limited form of negation (incl. negation of intensional symbols). This is due to the fact that within each rule, the only symbols that may be negated are those defined in lower strata. Existential least fixpoint logic (ELFP) which expresses the queries of unstratified logic programs is also described. SLFP and ELFP are compared; ELFP allows only existential quantification, and negation can be applied only to atomic formulas containing no relation variables (intensional symbols in logic programming). Both partial correctness and total correctness are logical notions with respect to SLFP. This demonstrates the superiority of SLFP over first-order logic as an assertion language. Partial correctness is a logical notion with respect to first-order logic but total correctness is not.