A Proof Calculus for Automated Deduction in Propositional Product Logic

Propositional product logic belongs to the basic fuzzy logics with continuous t-norms using the product t-norm (defined as the ordinary product of real numbers) on the unit interval [0,1]. This paper introduces a proof calculus for the product logic which is suitable for automated deduction. The calculus provides one of possible generalisations of the family of modifications of the procedure (algorithm) of Davis, Putnam, Logemann, and Loveland (DPLL) in the context of fuzzy logics. We show that the calculus is refutation sound and finitely complete as well. The deduction, satisfiability, and validity problems are solved in the finite case. The achieved results contribute to the theoretical (logic and computational) description of multi-step fuzzy inference.