Canonical Logic Programs are Succinctly Incomparable with Propositional Formulas
Yuping Shen, Xishun Zhao · arXiv (Cornell University) · 2014
\\emph{Canonical (logic) programs} (CP) refer to normal logic programs augmented with connective $not\\ not$. In this paper we address the question of whether CP are \\emph{succinctly incomparable} with \\emph{propositional formulas} (PF). Our main result shows that the PARITY problem, which can be polynomially represented in PF but \\emph{only} has exponential representations in CP. In other words, PARITY \\emph{separates} PF from CP. Simply speaking, this means that exponential size blowup is generally inevitable when translating a set of formulas in PF into an equivalent program in CP (without introducing new variables). Furthermore, since it has been shown by Lifschitz and Razborov that there is also a problem that separates CP from PF (assuming $\\mathsf{P}\ subseteq \\mathsf{NC^1/poly}$), it follows that CP and PF are indeed succinctly incomparable. From the view of the theory of computation, the above result may also be considered as the separation of two \\emph{models of computation}, i.e., we identify a language in $\\mathsf{NC^1/poly}$ which is not in the set of languages computable by polynomial size CP programs.