Location: Courses | CL Homepage | Dept. of Appl. Inf. (AI and DP) | Faculty of Math., Physics, and Inf. | Comenius Univ. Bratislava | Slovakia

1-AIN-625 Introduction to Mathematical Logic for Programmers



Here you will find the course information sheet.


To give mathematical foundations of declarative programming languages. Programs are definitions of recursive functions. Computational model is based on the reduction of terms. Data structures are coded into the domain of natural numbers. The course has computer labs in the programming system CL.


Primitive Recursive Functions. Basic functions and operations (composition of functions and primitive recursion). Explicit definitions. Bounded minimalization. Pairing function and arithmetization. Backward recursion. Recursion with substitution in parameters. Nested simple recursion. Recursion with measure. Regular recursive definitions.

General Recursive Functions. Beyond primitive recursion: Ackermann-Péter function, universal function for primitive recursive functions. Primitive recursive indices. Transfinite recursion. General recursive functions. Regular minimalization. μ-Recursive functions.

Partial Recursive Functions. First recursion theorem (fixed point theorem). Computation model. Equivalence of the operational and denotational semantics. Partial recursive functions. Unbounded minimalization. Arithmetization of computation. Kleene normal-form theorem. Universal function. Recursive indices. Enumeration theorem. Partial μ-recursive functions. Recursively undecidable problems. Recursively decidable, semidecidable and undecidable problems. Church thesis.





* – updated within last 7 days Last modified: 2015-09-17T15:12+0200