Institute of Computer Science

The Czech Academy of Sciences

The Czech Academy of Sciences

"Thinking is the hardest work there is, which is probably the reason why so few engage in it. - Henry Ford

The research in our department follows two directions. The first one concerns non-classical logics. We focus mainly on substructural, fuzzy and modal logics. In the second one we investigate computational complexity by means of specialised computational models like neural networks, branching programs and Boolean functions.

Logic is an essential tool for the formalization of mathematics and it is suitable also for formal description of many specialized structures, including those that arise from particular applications. Specialized types of logics are therefore used, e.g., for program or hardware verification.

Computational complexity looks into the problem of determining the least amount of computational resources that is necessary for algorithmic problem solving. Time and computer memory are typical resources of a computation, however, models with other complexity measures, such as the size and depth of a circuit, the number of memory accesses, energy, parallelism, probabilistic and analog computation, etc., are also investigated.

We focus on theoretical research in the following areas:

Our department organizes jointly with the Czech Society for Cybernetics and Informatics a seminar on applied mathematical logic (also called Hájek’s seminar according to its founder) which regularly takes place since the late 1960’s. The program can be found here.

- Algebraic Methods in Proof Theory
- Center of Excellence – Institute for Theoretical Computer Science
- Modelling vague quantifiers in mathematical fuzzy logic
- An Order-Based Approach to Non-Classical Propositional and Predicate Logics
- Totally ordered monoids

- Handbook of Mathematical Fuzzy Logic – Vol. 1
- Handbook of Mathematical Fuzzy Logic – Vol. 2
- A Henkin-Style Proof of Completeness for First-Order Algebraizable Logics.
*Journal of Symbolic Logic,*2015. - Undecidability of consequence relation in Full Non-associative Lambek Calculus.
*Journal of Symbolic Logic,*2015. - Full Lambek Calculus with Contraction is Undecidable.
*Journal of Symbolic Logic,*to appear. - Word Problem for Knotted Residuated Lattices.
*Journal of Pure and Applied Algebra,*2015.

- Bílková Marta, Mgr., Ph.D.
- Cintula Petr, doc.Ing., Ph.D.
- Dostál Matěj, Ing.
- Haniková Zuzana, RNDr., Ph.D.
- Harmancová Dagmar, prom.mat.
- Horčík Rostislav, Ing., Ph.D.
- Klimošová Tereza, Mgr., Ph.D.
- Lávička Tomáš, Mgr.
- Majer Ondrej, RNDr., CSc.
- Moraschini Tommaso
- Petrík Milan, Ing., Ph.D.
- Piguet Diana, Mgr., Ph.D.
- Přenosil Adam, Mgr.
- Sarkoci Peter, Ing., Ph.D.
- Savický Petr, RNDr., CSc.
- Sedlár Igor, Mgr., Ph.D.
- Šíma Jiří, doc. RNDr., DrSc.
- Tran Manh Tuan, M.Sc. Ph.D.
- Vidal Wandelmer Amanda, Ph.D.
- Žák Stanislav, RNDr., CSc.