Graded many-valued resolution with aggregation. (Q1428680)

The aim of the paper is to define a resolution truth function \(f_\lor(x,y)\), \(x,y\in[0,1]\), for using it in a many-valued resolution procedure. This function \(f_\lor(x,y)\) provides a truth value \(z\) of a resolvent \([(C\lor B), z]\) of a pair of signed many-valued clauses \([(C\lor A), x]\) and \([(B\lor\neg A), y]\), i.e. clauses which are true with respect to some truth values \(x\) and \(y\) from the unit interval \([0,1]\). The goal of the paper is achieved by algebraic analysis of such many-valued operators as t-(semi)conorms. The authors introduce a notion of aggregation deficit which is based on the construction of conjunction from residuated implication proposed by \textit{D. Dubois} and \textit{H. Prade} [Stochastica 8, 267--279 (1984; Zbl 0581.03016)]. There exist highly related papers that are not cited here: (*) ``Automated deduction for many-valued logics'', by \textit{M. Baaz}, \textit{F. Fermüller} and \textit{G. Salzer} [in: A. Robinson et al. (eds.), Handbook of automated reasoning. In 2 vols. Amsterdam: North-Holland/Elsevier. 1355--1402 (2001; Zbl 0992.03015)]; (**) ``\(\alpha\)-resolution principle based on first-order lattice-valued logic \(\text{LF}(X)\)'', by \textit{Y. Xu, D. Ruan, E. Kerre} and \textit{J. Liu} [Inf. Sci. 132, 221--239 (2001; Zbl 0997.03006)]. For instance, in (**) the authors develop a resolution calculus for first-order logic having a lattice-ordered set of truth values. It would be very interesting to establish wether this earlier paper by Xu et al. contains a more general result than the present paper. The authors obtain a sufficient result which could be applied in many-valued theorem proving. However, they use algebraic notation which is not common among logicians, see e.g. (*). Of course it is not a defect of the paper, but it shows that the authors work in a very particular branch of many-valued logic without knowing important results concerning many-valued logic. Also it testifies the lack of commonly adopted symbolic notation and terminology among many-valued logic researchers in general. That constitutes the main methodological problem at the present stage of development of many-valued logic.