文章基本信息

标题：Automatic Proving of Fuzzy Formulae with Fuzzy Logic Programming and SMT
本地全文：下载
作者：Miquel Bofill ; Gines Moreno ; Carlos Vazquez 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2014
卷号：64
语种：English
出版社：European Association of Software Science and Technology (EASST)
摘要：In this paper we deal with propositional fuzzy formulae containing several propositional symbols linked with connectives defined in a lattice of truth degrees more complex than Bool. We firstly recall an SMT (Satisfiability Modulo Theories) based method for automatically proving theorems in relevant infinitely valued (including Łukasiewicz and G¨odel) logics. Next, instead of focusing on satisfiability (i.e., proving the existence of at least one model) or unsatisfiability, our interest moves to the problem of finding the whole set of models (with a finite domain) for a given fuzzy formula. We propose an alternative method based on fuzzy logic programming where the formula is conceived as a goal whose derivation tree contains on its leaves all the models of the original formula, by exhaustively interpreting each propositional symbol in all the possible forms according the whole set of values collected on the underlying lattice of truth-degrees.