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.
Type de document :
Rapport
[Research Report] RR-1674, INRIA. 1992
Liste complète des métadonnées

https://hal.inria.fr/inria-00074882
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 16:46:41
Dernière modification le : vendredi 25 mai 2018 - 12:02:02
Document(s) archivé(s) le : mardi 12 avril 2011 - 19:53:59

Fichiers

Identifiants

  • HAL Id : inria-00074882, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

147

Téléchargements de fichiers

48