Semestr zimowy 2025/2026

C++23 to najnowsza wersja języka C++. Język C++ prawdza się, gdy chcemy zapewnić wysoką wydajność programu. Doskonale nadaje się do zastosowań systemowych, inżynierskich i algorytmicznych. Język ten jest stale rozwijany a kolejne jego specyfikacje, czyli C++11, C++14, C++17, C++20 i C++23, przyniosły wiele zmian i udogodnień. W porównaniu z językiem C++98 (standard z roku 1998) przeszedł on tak dużą transformację, że można śmiało powiedzieć, że jest to nowy język programowania. Aby w pełni wykorzystać potencjał współczesnego języka C++ należy go używać wraz z biblioteką standardową STL. C++ i STL to doskonałe narzędzie do zaimplementowania oprogramowania bardzo wysokiej jakości.

Przedmiot jest kontynuacją Logiki dla Informatyków przeznaczoną dla studentów zainteresowanych teorią informatyki. Celem jego jest rozszerzenie podstaw wiedzy z zakresu logiki matematycznej i dziedzin pokrewnych o narzędzia potrzebne do zaawansowanych studiów w obszarach związanych z logiką i weryfikacją czy teorią języków programowania, bez wchodzenia w tematykę ściśle badawczą. W tym celu będziemy koncentrować się na podstawowych zagadnieniach trzech aspektów logiki matematycznej: algebry uniwersalnej, teorii dowodu i podstawach semantyki logik, z naciskiem na perspektywę i użyteczność w informatyce

Kurs przedmiotu Metody Implementacji Algorytmów w roku 2025/2026.

Na wykładzie wprowadzone jest teoria i podstawowe metody, które umożliwiają efektywne programowanie grafiki z użyciem kart graficznych. Wykład nie jest jednak kursem biblioteki OpenGL. 

Wykład jest wprowadzeniem do projektowania układów cyfrowych przy użyciu języka opisu sprzętu Verilog oraz ich implementacji na układach FPGA. W ramach zajęć student nauczy się również metod testowania sprzętu oraz zapozna się z podstawami formalnej weryfikacji układów cyfrowych.

Wstęp do informatyki 2025/26

Wstępny kurs programowania na przykładzie języka Python.

Na seminarium czytać będziemy prace dotyczące rozstrzygalności i złożoności problemów spełnialności (czy dana formuła ma model), skończonej spełnialności (czy dana formuła ma model skończony) oraz związanych z nimi problemów odpowiadania na zapytania do baz danych/baz wiedzy (dla danej bazy D, teorii logicznej T i zapytania q, czy prawdą jest, że każdy model/skończony model D i T spełnia q?)

Interesować nas będą fragmenty logiki pierwszego rzędu (two-variable fragment, guarded fragment, unary negation fragment, guarded negation fragment, …) oraz logiki deskrypcyjne.

Materiał będzie się częściowo pokrywał z materiałem przedmiotu Problemy Decyzyjne w Logice, ale będzie też sporo innych rzeczy i osoby, które ten przedmiot zaliczyły mogą śmiało zapisać się na seminarium.

Niewykluczone, że spotkamy się z pewnymi problemami otwartymi, które będzie można próbować rozwiązać.