A DPLL Procedure with Dichotomous Branching for Propositional Product Logic

TL;DR

This paper introduces a modified DPLL procedure tailored for propositional product logic, enabling automated deduction and fuzzy inference, with proven soundness and completeness for finite cases, supporting intelligent system design.

Contribution

It presents a novel DPLL-based method adapted for fuzzy logic with continuous t-norms, bridging theorem proving and fuzzy inference.

Findings

Procedure is refutation sound and finitely complete.

Solutions for deduction, satisfiability, and validity are proposed.

Applicable to multi-step fuzzy inference in intelligent systems.

Abstract

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.