First-order satisfiability in Gödel logics: an NP-complete fragment
type: Item
instance of: scholarly article
title: First-order satisfiability in Gödel logics: an NP-complete fragment
zbMATH Open document ID: 1244.03090
author: Matthias Baaz
author: Agata Ciabattoni
author: Norbert Preining
published in: Theoretical Computer Science
publication date: 2011-12-07T00:00:00Z
review text: The topic of the paper is a fragment of first-order Gödel logic with \(\Delta\) whose satisfiability problem is shown to be NP-complete. In particular, the considered fragment is the set \(\mathrm{FO}^1_{\mathrm{mon}}(V)\), a subset of both the monadic fragment and the one-variable fragment of first-order Gödel logic, of formulas in the language of Gödel logic plus \(\Delta\) having the form \[ \bigvee_{i=1}^n \left( \exists x A^i_1(x) \wedge \cdots \wedge \exists x A^i_{n_1}(x) \wedge \forall x B^i_1(x) \wedge \cdots \wedge \forall x B^i_{m_1}(x)\right), \] where each \(A_k^i\), \(B_k^i\) is a monadic and quantifier-free formula containing no function and constant symbol. \(V\) is the set of truth values (a subset of \([0,1]\)) in which the predicates are interpreted. Note that in general satisfiability in monadic Gödel logic with \(\Delta\) is undecidable if the set of truth values is infinite. The interest in this fragment also relies on the fact that formulas of \(\mathrm{FO}^1_{\mathrm{mon}}(V)\) are used to formalize the expert system CADIAG-2 for making differential diagnoses in internal medicine. If \(V\) has \(1\) as isolated point, it is not difficult to prove that the SAT problem of \(\mathrm{FO}^1_{\mathrm{mon}}(V)\) is decidable (this is for example the case when \(V\) is finite). If in \(V\) the point \(1\) is not isolated, then the proof of decidability needs a semantic investigation of the topological properties if \(V\). The complexity issues follow from a reduction to the satifiability problem of a suitable propositional finite-valued Gödel logic.
reviewed by: Brunella Gerla
Mathematics Subject Classification ID: 03B52
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 68T35
Mathematics Subject Classification ID: 92C50
zbMATH DE Number: 5986991
zbMATH Keywords: first-order Gödel logic
zbMATH Keywords: satisfiability
zbMATH Keywords: monadic logic
zbMATH Keywords: one-variable fragment
zbMATH Keywords: expert system CADIAG-2 for medical diagnosis
MaRDI profile type: Publication
full work available at URL: j.tcs.2011.07.015
OpenAlex ID: W2096504793
cites work: Q4893133
cites work: Monadic Fragments of Gödel Logics: Decidability and Undecidability Results
cites work: SAT in Monadic Gödel Logics: A Borderline between Decidability and Undecidability
cites work: Embedding logics into product logic
cites work: First-order Gödel logics
cites work: Continuous Fraïssé conjecture
cites work: Linear Kripke frames and Gödel logics
cites work: Algebraic Completeness Results for Dummett's LC and Its Extensions
cites work: Residuated fuzzy logics with an involutive negation
cites work: T-norm-based logics with an independent involutive negation
cites work: Q4450446
cites work: Metamathematics of fuzzy logic
cites work: On theories and models in fuzzy predicate logics
cites work: Q4323294
cites work: Strongly equivalent logic programs
cites work: Intuitionistic fuzzy logic and intuitionistic fuzzy set theory
cites work: On the completenes principle: A study of provability in heyting's arithmetic and extensions
DOI: 10.1016/J.TCS.2011.07.015
description: scientific article; zbMATH DE number 5986991