The purpose of this paper is to draw attention to existential fixed-point logic. Among other things, we show that: (1) If a structure A satisfies an existential fixed-point formula , then A has a finite subset F such that every structure B with A|F = B|F satisfies . (2) Using existential fixed-point logic instead of first-order logic removes the expressivity hypothesis in Cook's completeness theorem for Hoare logic. (3) In the presence of a successor relation, existential fixed-point logic captures polynomial time.
CITATION STYLE
Blass, A., & Gurevich, Y. (1987). Existential fixed-point logic (pp. 20–36). https://doi.org/10.1007/3-540-18170-9_151
Mendeley helps you to discover research relevant for your work.