Satisfiability in Łukasiewicz logic and its unbounded relative
This provides the first complexity characterization for unbounded Łukasiewicz logic, linking it to the well-studied Łukasiewicz logic.
The authors prove that the existential theory of the additive ℓ-group on the reals with a distinguished element -1 is NP-complete, establishing a complexity upper bound for the theoremhood and finite consequence relation of unbounded Łukasiewicz logic. This is achieved by a reduction to the existential theory of the standard MV-algebra.
Unbounded Łukasiewicz logic is a substructural logic that combines features of infinite-valued Łukasiewicz logic with those of abelian logic. The logic is finitely strongly complete w.r.t.~the additive $\ell$-group on the reals expanded with a distinguished element $-1$. We show that the existential theory of this structure is NP-complete. This provides a complexity upper bound for the set of theorems and the finite consequence relation of unbounded Łukasiewicz logic. The result is obtained by reducing the problem to the existential theory of the MV-algebra on the reals, the standard semantics of Łukasiewicz logic. This provides a new connection between both logics. The result entails a translation of the existential theory of the standard MV-algebra into itself.