A <i>DPLL</i> Procedure with Dichotomous Branching for Propositional Product Logic

The propositional product logic is one of the basic fuzzy logics with continuous t-norms, employing the product t-norm on the unit interval [Formula: see text]. 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 for inference 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.