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 :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00074882
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 4:46:41 PM
Last modification on : Friday, May 25, 2018 - 12:02:02 PM
Long-term archiving on : Tuesday, April 12, 2011 - 7:53:59 PM

Identifiers

  • HAL Id : inria-00074882, version 1

Collections

Citation

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

Share

Metrics

Record views

170

Files downloads

102