The Complexity and Expressive Power of Second-Order Extended Logic

Abstract

We study the expressive powers of SO-HORN${}^{\ast }$, SO-HORN${}^r$ and SO-HORN${}^{\ast r}$ on all finite structures. We show that SO-HORN${}^r$, SO-HORN${}^{\ast r}$, FO(LFP) coincide with each other and SO-HORN${}^{\ast }$ is proper sublogic of SO-HORN${}^r$. To prove this result, we introduce the notions of DATALOG${}^{\ast }$ program, DATALOG${}^r$ program and their stratified versions, S-DATALOG${}^{\ast }$ program and S-DATALOG${}^r$ program. It is shown that, on all structures, DATALOG${}^r$ and S-DATALOG${}^r$ are equivalent and DATALOG${}^{\ast }$ is a proper sublogic of DATALOG${}^r$. SO-HORN${}^{\ast }$ and SO-HORN${}^r$ can be treated as the negations of DATALOG${}^{\ast }$ and DATALOG${}^r$, respectively. We also show that SO-EHORN${}^r$ logic which is an extended version of SO-HORN captures co-NP on all finite structures.

Cited by in corpus (1)

• Capturing the polynomial hierarchy by second-order revised Krom logic