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:
logic and algebraic foundation of multivalued logic;
applications to this logics to the study of approximate reasoning for further creation of intelligent systems;
study of classical deduction systems from the point of view of computational complexity;
extension to multivalued logic of the results obtained in classical proof theory;
theoretical foundation of automated deduction;
algorithms and implementations of classical SAT and signed SAT (multivalued), as well as implementations of proof systems.