A deductive system for existential least fixpoint logic

Kevin J. Compton 1
1 ALGO - Algorithms
Inria Paris-Rocquencourt
Abstract : Existential least fixpoint logic (ELFP) is a logic with a least fixpoint operator but only existential quantification. It arises in many areas of computer science including logic programming, database theory, program verification, complexity theory, and recursion theory on abstract structures. A sequent calculus (Gentzen-style deductive system) for this logic is presented and proved to be complete. Basic model theoretic facts about ELFP are derived from the completeness theorem and the construction used in its proof. The relationship of these model theoretic facts to logic programming and database queries is explored.
Type de document :
Rapport
[Research Report] RR-1675, INRIA. 1992
Liste complète des métadonnées

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

Fichiers

Identifiants

  • HAL Id : inria-00074881, version 1

Collections

Citation

Kevin J. Compton. A deductive system for existential least fixpoint logic. [Research Report] RR-1675, INRIA. 1992. 〈inria-00074881〉

Partager

Métriques

Consultations de la notice

90

Téléchargements de fichiers

69