Determining Implication of Fixed Matrix Prenex Normal Forms Can Be Decided in Linear Time

TL;DR

For two sentences $S_1$ and $S_2$ in Prenex Normal Form with a fixed matrix $P(\mathbf{x})$, the paper studies the decision problem of whether $S_1\implies S_2$. It introduces a finite, graph-based view of prefix equivalence classes under run-wise permutations and local moves, and presents a RAM algorithm that solves PNFPI in $O(n)$ time in the length of the prefix. The main contributions are a linear-time decision procedure and a matching linear-time lower bound, establishing optimality for this problem. The work clarifies the role of quantifier runs in prefix implication and notes the practical limits of applicability to a LeetCode-like setting.

Abstract

For a fixed arbitrary matrix depending on $n$ variables, one may ask whether a Prenex Normal Form (PNF) implies another. A RAM algorithm running in linear time is presented and shown to be asymptotically optimal.

Theorems & Definitions (6)

• Theorem 1
• proof
• Theorem 2
• proof
• Theorem 3
• proof