Item
Ministerio de EconomÃa y Competitividad (Espanya)  
AlmendrosJimenez, JesÃ¹s M.
Bofill Arasa, Miquel LunaTedesqui, Alejandro Moreno, GinÃ¨s VÃ zquez, Carlos Villaret i AusellÃ©, Mateu 

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. Instead of focusing on satisfiability (i.e., proving the existence of at least one model) as usually done in a SAT/SMT setting, our interest moves to the problem of finding the whole set of models (with a finite domain) for a given fuzzy formula. We reuse a previous method based on fuzzy logic programming where the formula is conceived as a goal whose derivation tree, provided by our FLOPER tool, contains on its leaves all the models of the original formula, together with other interpretations. Next, we use the ability of the FuzzyXPath tool (developed in our research group with FLOPER) for exploring these derivation trees once exported in XML format, in order to discover whether the formula is a tautology, satisfiable, or a contradiction, thus reinforcing the bilateral synergies between FuzzyXPath and FLOPER This work has been partially supported by the EU (FEDER), and the Spanish MINECO Ministry (Ministerio de EconomÃa y Competitividad) under grants TIN201344742C44R, TIN201233042 and TIN201345732C42P 

http://hdl.handle.net/2072/299150  
eng  
Springer Verlag  
Tots els drets reservats  
ProgramaciÃ³ lÃ²gica
Logic programming Teoremes  DemostraciÃ³ automÃ tica Automatic theorem proving LÃ²gica difusa Fuzzy logic Sistemes borrosos Fuzzy systems 

Fuzzy XPath for the automatic search of fuzzy formulae models  
info:eurepo/semantics/article  
Recercat 