The current project is focused on propositional logic as a foundation for computer science. We will study classical logic, as well as multivalued logic, looking at the foundation of multivalued logic based on t-norms, and the proof theory of both logics. Moreover, we will apply this knowledge to automated deduction, hardware verification and implementation of heuristics for computationally hard problems. The topics will be:

1. logic and algebraic foundation of multivalued logic;
2. applications to this logics to the study of approximate reasoning for further creation of intelligent systems;
3. study of classical deduction systems from the point of view of computational complexity;
4. extension to multivalued logic of the results obtained in classical proof theory;
5. theoretical foundation of automated deduction;
6. algorithms and implementations of classical SAT and signed SAT (multivalued), as well as implementations of proof systems.