Satisfiability in Łukasiewicz logic and its unbounded relative

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Haniková, Zuzana, Jankovec, Filip
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914608142352384
author Haniková, Zuzana
Jankovec, Filip
author_facet Haniková, Zuzana
Jankovec, Filip
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2601_00817
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Satisfiability in Łukasiewicz logic and its unbounded relative
Haniková, Zuzana
Jankovec, Filip
Logic
Logic in Computer Science
F.4.1
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.
title Satisfiability in Łukasiewicz logic and its unbounded relative
topic Logic
Logic in Computer Science
F.4.1
url https://arxiv.org/abs/2601.00817