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

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

Identifiers

  • 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⟩

Share

Metrics

Record views

113

Files downloads

129