Skip to Main content Skip to Navigation
New interface
Reports (Research report)

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 (Research report)
Complete list of metadata
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 4:46:01 PM
Last modification on : Wednesday, October 26, 2022 - 8:16:26 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 7:53:03 PM


  • HAL Id : inria-00074881, version 1



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



Record views


Files downloads