A Proof Calculus for Automated Deduction in Propositional Product Logic

Dušan Guller ()
Additional contact information
Dušan Guller: Department of Applied Informatics, Comenius University, Mlynská dolina, 842 48 Bratislava, Slovakia

Mathematics, 2024, vol. 12, issue 23, 1-48

Abstract: 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.

Keywords: product logic; procedure of Davis, Putnam, Logemann, and Loveland; automated deduction; fuzzy inference; proof calculi (search for similar items in EconPapers)
JEL-codes: C (search for similar items in EconPapers)
Date: 2024
References: View complete reference list from CitEc
Citations:

Downloads: (external link)
https://www.mdpi.com/2227-7390/12/23/3805/pdf (application/pdf)
https://www.mdpi.com/2227-7390/12/23/3805/ (text/html)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:gam:jmathe:v:12:y:2024:i:23:p:3805-:d:1534397

Access Statistics for this article

Mathematics is currently edited by Ms. Emma He

More articles in Mathematics from MDPI
Bibliographic data for series maintained by MDPI Indexing Manager ().