Logika w informatyce

Opis

Teoria typów w odniesieniu do programowania funkcyjnego, przepisywanie termów, automatyczne wspomaganie dowodzenia. Logiczne podstawy weryfikacji: logika temporalna, logika programów, logika monadyczna i jej związek z automatami i grami. Tematy badawcze dotyczą między innymi siły wyrazu rozmaitych rachunków logicznych, rozstrzygalności, oraz efektywności weryfikacji modelowej.

Seminaria

• Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji
• Seminarium badawcze „Systemy Inteligentne”
• Seminarium „Logika i teoria typów”
• Research Seminar of the Logic Group: Approximate reasoning in data mining

Pracownicy i doktoranci

• dr Marcin Benke

  Rachunek lambda, teoria typów

• prof. dr hab. Mikołaj Bojańczyk

  Logiki dla weryfikacji, teoria automatów

• dr Jacek Chrząszcz

  Rachunek lambda, przepisywanie termów, systemy wspomagania dowodzenia

• dr hab. Lorenzo Clemente
• dr hab. Wojciech Czerwiński, prof. UW
• dr Tomasz Gogacz
• dr Piotr Hofman
• dr hab. Eryk Kopczyński
• prof. dr hab. Sławomir Lasota

  Weryfikacja, sprawdzanie równoważności, teoria automatów

• dr hab. Filip Murlak, prof. UW
• dr hab. Anh Linh Nguyen, prof. UW

  Logiki modalne, logiki dla baz danych

• prof. dr hab. Damian Niwiński

  Logiki dla weryfikacji, teoria automatów, gry nieskończone, złożoność obliczeniowa

• dr hab. Paweł Parys, prof. UW
• dr Marcin Przybyłko
• dr hab. Aleksy Schubert, prof. UW

  Rachunek lambda, teoria typów, złożoność systemów logicznych

• dr hab. Michał Skrzypczak
• prof. dr hab. Andrzej Szałas

  Logiki nieklasyczne, wnioskowanie aproksymacyjne, logiki wielowartościowe, automatyczne wnioskowanie, logiki programów, formalna specyfikacja i weryfikacja

• prof. dr hab. Andrzej Tarlecki

  Logika, algebra uniwersalna, teoria kategorii w informatyce

• dr hab. Szymon Toruńczyk, prof. UW
• prof. dr hab. Jerzy Tyszkiewicz

  Logika dla baz danych, teoria modeli skończonych, złożoność Kołmogorowa

• prof. dr hab. Paweł Urzyczyn

  Rachunek lambda, teoria typów, logiki dla weryfikacji

• dr Daria Walukiewicz-Chrząszcz

  Rachunek lambda, przepisywanie termów