The propositional product logic is one of the basic fuzzy logics with continuous t-norms, exploiting the multiplication t-norm on the unit interval [0,1]. Our aim is to combine well-established automated deduction (theorem proving) with fuzzy inference. As a first step, we devise a modification of the procedure of Davis, Putnam, Logemann, and Loveland (DPLL) with dichotomous branching inferring in the product logic. We prove that the procedure is refutation sound and finitely complete. As a consequence, solutions to the deduction, satisfiability, and validity problems will be proposed for the finite case. The presented results are applicable to a design of intelligent systems, exploiting some kind of multi-step fuzzy inference.
翻译:命题乘积逻辑是基于连续t-范数的基础模糊逻辑之一,采用单位区间[0,1]上的乘法t-范数。我们的目标是将成熟的自动演绎(定理证明)与模糊推理相结合。作为第一步,我们针对乘积逻辑中的推理过程,设计了一种采用二分分支的Davis、Putnam、Logemann和Loveland(DPLL)过程的改进方案。我们证明了该过程具有反驳可靠性和有限完备性。由此,针对有限情形,将提出演绎、可满足性和有效性问题的求解方案。所呈现的结果可应用于利用某种多步模糊推理的智能系统设计。