문제

I'm looking for an algorithm to decide if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are existentials).

Is it known if such an algorithm exists or does not exist? At least when no functions symbols are admitted? And if it actually exists, which is its complexity?

I know that, given a formula, we can build an equivalent one in prenex form. However, here is an example which illustrates that a formula, equivalent to an existential one, admits also an equivalent prenex formula which is not existential:

Consider the vocabulary $L=\{E\}$, where $E$ is a binary relation symbol. Then the formula $$\exists x\,E(x,x)$$ which states that a directed graph admits a loop, is an existential formula and is equivalent to $$\exists x\forall y\,\,\,\,x=y\rightarrow E(x,y)$$ which is in prenex form, but not existential. So applying the algorithm to build a prenex form to the second formula would not produce an existential one.

올바른 솔루션이 없습니다

라이센스 : CC-BY-SA ~와 함께 속성
제휴하지 않습니다 cs.stackexchange
scroll top