Oferta dydaktyczna Instytutu Informatyki

Poniższa lista przedstawia przedmioty, które są uczone w Instytucie Informatyki, niektóre z nich co roku, niektóre z mniejszą częstotliwością Każdy student Instytutu Informatyki studiuje wg indywidualnego toku studiów, wybierając (zgodnie z pewnymi zasadami) z tej listy swoje przedmioty.

Jeżeli zastanawiasz się nad studiami u nas, jeżeli chcesz wiedzieć, czy na Uniwersytecie można zostać inżynierem, jeżeli interesuje Cię 1000 zł stypendium miesięcznie - zapraszamy na naszą stronę główną

Wprowadzenie do logiki formalnej

Nazwa angielska (title in English): Introduction to Formal Logic
Prowadzący (lecturer): Hans de Nivelle
Liczba punktów (ECTS): 7
Liczba punktów 2007 (ECTS since 2007): 6
Rodzaj (type): podstawowy
Rodzaj od 2007 (type since 2007): informatyczny.I2
Liczba godzin (hours in semester):
wykład:30
ćwiczenia+pracownia:30
Egzamin (exam): tak
Możliwe zajęcia w języku angielskim (can be taught in English): tak
Przedmiot zostal uaktualniony na biezacy rok (updated): nie
Semestr (semester): letni

Wymagania (prerequisites)

Opis (description)

The course is given by Hans de Nivelle and Malgorzata Biernacka.

We teach the basis of what every computer scientist needs to know about logic. A computer scientist needs to understand the notion of formal proof, and understand that it is possible to write down proofs at such a level of detail that they can be formally checked.

One needs to know about constructive logic, because in constructive logic every proof is an algorithm: If one has proven that something exists, then one also knows how to compute it.

One needs to know about automated proof search, because automated proof search is used in AI and in data bases.

One needs to know about the possibility of proving programs correct, because it is possible that some day, such correctness proofs will be the main method for ensuring correctness of programs.

Program (program)

The standard logical operators, equality, quantifiers.

Capture avoiding Substitution, alpha-Equivalence.

Sequent Calculus, usage of Sequent Calculus. The cut rule, cut elimination, Herbrand's theorem.

Semantics of first-order Logic. Soundness and Completeness of Sequent Calculus.

Principle of Excluded Middle, Intuitionistic Logic, Natural Deduction.

Transforming Proofs from Natural Deduction to Sequent Calculus and Back.

Higher-Order Logic. Usage of higher-order logic for proving interesting properties of integers and datastructures. Modelling of algorithms in Higher-Order Logic.

Curry-Howard isomorphism, notion of inductive type, computation as normalization, the Coq system.

Introduction to automated theorem proving: Unification, resolution and paramodulation.

Literatura (references)

Jeżeli jesteś zainteresowany studiowaniem w naszym instytucie, zapraszamy na stronę poświęconą tegorocznej rekrutacji.

Nazwa użytkownika (user name):
Hasło (password):