Skip to Main content Skip to Navigation

Stratified least fixpoint logic

Kevin J. Compton 1
1 ALGO - Algorithms
Inria Paris-Rocquencourt
Abstract : Stratified least fixpoint logic or SLFP characterizes the expressibility of stratified logic programs and in a different formulation has been used as a logic of imperative programs. These two formulations of SLFP are proved to be equivalent and a complete sequent calculus for SLFP is presented. It is argued that SLFP is the most appropriate assertion language for program verification. In particular, it is shown that traditional approaches using first-order logic as an assertion language only restrict to interpretations where first-order logic has the same expressibility as SLFP.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 4:46:41 PM
Last modification on : Thursday, February 3, 2022 - 11:16:45 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 7:53:59 PM


  • HAL Id : inria-00074882, version 1



Kevin J. Compton. Stratified least fixpoint logic. [Research Report] RR-1674, INRIA. 1992. ⟨inria-00074882⟩



Record views


Files downloads