Automated Reasoning
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)
- Lógica Multivaluada: fundamentos y aplicaciones al tratamiento de la vaguedad y la imprecisión13/12/2004 - 13/12/2007
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.
