First-order satisfiability in Gödel logics: an NP-complete fragment (Q650893)

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.