STRATIFIED LEAST FIXPOINT LOGIC

Stratified least fixpoint logic, or SLFP, characterizes the expressibi lity of stratified logic programs and, in a different formulation, has been used as a logic of imperative programs. These two formulations o f SLFP are proved to be equivalent. A complete sequent calculus with o ne infinitary rule is given for SLFP. It is argued that SLFP is the mo st appropriate assertion language for program verification. In particu lar, it is shown that traditional approaches using first-order logic a s an assertion language only restrict to interpretations where first-o rder logic has the same expressibility as SLFP.