Question

Consider propositional logic over the connectives $\land$, $\lor$, and $\lnot$. Notation: $| \alpha |$ is the length of formula $\alpha$.

We are given a formula $\phi$. Cancel all cancellable negations in $\phi$ by applying all possible valid biconditionals (EDIT: such as the examples below) to get $\phi'$; for clarity we note that $\phi \leftrightarrow \phi'$. We are also given that $\phi'$ is monotonic. Are there examples where $| \phi' |$ must grow exponentially, or is $| \phi' |$ bounded by a polynomial? If there's an example of exponential growth, please show it.

EDIT: The following biconditionals are examples of what I'm trying to get at, formulas which can be used to cancel negations while preserving equivalence. The procedure would presumably be to unify the left-hand side of the formula with $\phi$ via unification and substitute the right-hand side as appropriate per unification.

$$\alpha \land (\lnot \alpha \lor \beta) \leftrightarrow \alpha \land \beta$$ $$\lnot \lnot \alpha \leftrightarrow \alpha$$

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top