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)