This field deals with deduction problems expressed in some kind of Logic. Currently, we work actively with classical, multivalued and higher order Logics. The goal is to chain adequately the inferences to solve automatically the deduction problems at hand. As the deduction problems we treat are difficult to solve, the analysis and optimization of the needed resources, mainly the time, is mandatory.

  • Tractability in Non Clausal forms
  • Satisfiability problem
  • Automated Deduction in Many-valued Logics
  • Higher-Order Logics (Unification problem)

RAzonamiento, Satisfacción y Optimización

Initial/final date: 
De 01 Enero 2016 hasta 31 Diciembre 2019
Main researcher: 
Project type: 
Plan Nacional
Funding Entity: 
MINECO/FEDER TIN2015-71799-C2-1-P
Description: 

This project aims at advancing the state-of-the-art in several aspects of fuzzy logic, argumentation with uncertainty and preferences, new techniques for SAT/MaxSAT and distributed solving, and in their application to solve two real problems: the analysis of discussions in social networks to determine which are the most relevant opinions, and the control of energy resources in energy grids with decision strategies optimizing the selection and use of the most appropriate available energy resource at every time, trying to balance the economical and environmental impacts. These two problems, although different, are examples of complex problems that our society has to face today that require advanced techniques of reasoning, preference modelling, and optimization tasks to be successfully solved. To this end, in this project we aim at addressing the following objectives.

First, to develop an uniform, fuzzy logic-based logical framework integrating reasoning, argumentation and decision making models able to cope with vague and uncertain knowledge, as well as mechanisms to handle inconsistent information. To this end, we will study extensions of t-norm based logics with multiple modalities, each one accounting for an intensional notion like uncertainty, preference, trust or approximation. Argumentation

mechanisms accommodating uncertain and trust information will be also studied, in particular a probabilistic extension of the DeLP framework will be investigated.

Second, to extend current SAT, MaxSAT or SMT-based techniques for solving different reasoning and optimization tasks over that framework, and needed for our application problems. In particular, in the classical setting, we will pay attention to improving techniques to solve SAT/MaxSAT problems in a distributed way. Indeed, we want to study how graph layout algorithms could be used to model the intrinsic structure or topology of industrial (or real problem) SAT instances, and then to explicitly exploit it, specially the modularity property, in specialized SAT solvers. As for MaxSAT and MinSAT, our objective is to investigate and implement inference-based solvers and empirically compare them with state- of-the-art solvers. In the finitely-valued setting, the goal is to extend successful MaxSAT and MinSAT solving techniques to the framework of signed CNF formulas, whereas in the infinitely-valued setting we plan to make use of SMT solvers.

Third, to use the above real problems as testbeds to check the applicability of our models and solving tools, and to study their strengths and weaknesses. For the analysis of discussions in social networks, we want to develop argumentation models, on top of our fuzzy logic-based framework, such that opinions and relations between them can be modelled with a rich set of features and then analized with our reasoning algorithms. For dynamic and big size discussions, we want to check the suitability of distributed versions of our algorithms. For solving problems about control of energy resources, we want to develop models that use the characteristics of our logic framework that allow to model uncertainty, for the behaviour of energy resources, and user preferences, for considering the integration of multiple competing objectives. We plan to integrate this novel modelling approach within the general framework of reinforcement learning algorithms.

Referencia: 

MINECO/FEDER TIN2015-71799-C2-1-P

Project Status: 
Ongoing
Research line: 
Automated Reasoning
Acronym: 
RASO
External researchers: 
Tommaso Flaminio
ChuMin Li
Jimmy Lee
In collaboration with: 
Universitat de Lleida
Geographical scope: 
National
Grant type: 
Competitive
Transferència: 

Plataforma para la mejora de la experiencia de compra de alimentos en superficies comerciales basada en semántica y razonamiento automático

Initial/final date: 
De 01 Octubre 2012 hasta 31 Marzo 2015
Project researchers: 
Main researcher: 
Project type: 
Plan Nacional
Funding Entity: 
Ministerio de Economía y Competitividad - INNPACTO 2012 (IPT-2012-0688-060000)
Description: 
The main goal of the project SmartExFood is the development of an experimental platform for (i) the intelligent distribution of information associated to a product, (ii) the generation of shopping recommendations and (iii) the facilitation of personalized and contextualized assessment using mobile devices, in order to improve the experience of grocery shopping in supermarkets.
Funding Amount (€): 
91.08
Research line: 
Automated Reasoning
Acronym: 
SmartExFood
In collaboration with: 
Alimerka, Ainia, Innovati Networks S.L., Intermark

Lógica Multivaluada: fundamentos y aplicaciones al tratamiento de la vaguedad y la imprecisión

Initial/final date: 
De 13 Diciembre 2004 hasta 13 Diciembre 2007
Main researcher: 
Project type: 
-
Funding Entity: 
TIN2004-07933-C03-01
Description: 
The project, planned as a continuation of project LOGFAC (TIC2001-1577-C03-01), has three basic objectives. The first one is to continue the logic and algebraic study of t-norm based many-valued logics in the frame of both residuated and substructural logics. The second one is the formalization, within the framework of the above logics, of several deductive soft computing mechanisms, based on fuzzy logic, to deal with fuzziness and imprecision. The last one is to continue theoretical and experimental research on algorithms for the satisfiability problem in many-valued logics and their application to computational problems, in particular to constraint satisfaction problems with hard and soft constraints problems.
Funding Amount (€): 
0.00
Phd Students: 
Carles Noguera
Research line: 
Automated Reasoning
Acronym: 
MULOG