There are no prerequisites.
Logic in computer science
2021/2022
Programme:
Computer Science and Mathematics, Second Cycle
Year:
1 ali 2 year
Semester:
first or second
Kind:
optional
Group:
A
ECTS:
6
Language:
slovenian, english
Lecturers:
Hours per week – 1. or 2. semester:
Lectures
3
Seminar
0
Tutorial
2
Lab
0
Content (Syllabus outline)
The course is divided into core and optional parts. Core part:
syntax, formal system, bound variables, substitution.
Lambda-calculus and simple types.
Natural deduction, propostional and predicate calculus. Proof terms.
Optional parts:
Curry-Howard correspondence
Constructive interpretation of logic, and its significance for computer science.
Temporal logic and its use in computer science.
Modal logic and its use in knowledge modeling.
Other calcululi: pi-calculus, event calculus, etc.
Automated theorem proving.
Readings
M. Huth & M. Ryan: "Logic in computer science, 2nd Edition", Cambridge University Press, 2004.
Girard: “Proofs and Types”, Cambridge University Press, 1989, ASIN: 0521371813.
D. Bridges & E. Bsihop: “Constructive Analysis, 2nd ed.”, Springer Verlag, 1985, ISBN: 0387150668, 477 str.
P. Martin-Lof: “An Intuitionistic Theory of Types”. Twenty-Five Years of Constructive Type Theory. Editors: G. Sambin and J. Smith. Oxford Science Publications, 1998. Str. 127–172.
Objectives and competences
The objective is to show students how logic and computer science are connected, as logic is an essential tool in many areas of computer science. Students will obtain basic mathematical and logical knowledge, which they will be able to use at solving computer-science tasks.
Intended learning outcomes
Knowledge and understanding of basics of matehamatical logic, especially in relation to computer science.
Learning and teaching methods
Lectures, tutorials and consultations.
Assessment
Continuing (homework, midterm exams, project work)
Final (written and oral exam)
grading: 5 (fail), 6-10 (pass) (according to the Statute of UL)
Lecturer's references
BAUER, Andrej, STONE, Christopher A. RZ: a tool for bringing constructive and computable mathematics closer to programming practice. V: Computation and logic in the real world : Third Conference on Computability in Europe, CiE 2007, Siena, Italy, June 18-23, 2007 : proceedings, (Lecture notes in computer science, ISSN 0302-9743, 4497). Berlin, Heidelberg: Springer, cop. 2007, str. 28-42. [COBISS-SI-ID 14631769]
AWODEY, Steve, BAUER, Andrej. Sheaf toposes for realizability. Archive for mathematical logic, ISSN 0933-5846, 2008, vol. 47, no. 5, str. 465-478. [COBISS-SI-ID 15321689]
BAUER, Andrej, KAVKLER, Iztok. A constructive theory of continuous domains suitable for implementation. V: Joint Workshop Domains VIII - Computability over Continuous Data Types, Novosibirsk, September 11-15, 2007, (Annals of pure and applied logic, ISSN 0168-0072, Vol. 159, iss. 3). Amsterdam: Elsevier, 2009, str. 251-267. [COBISS-SI-ID 15329625]
HAJDINJAK, Melita, BAUER, Andrej. Similarity measures for relational databases. Informatica, ISSN 0350-5596, May 2009, vol. 33, no. 2, str. 143-149, ilustr. [COBISS-SI-ID 7110996]
BAUER, Andrej, STONE, Christopher A. RZ: a tool for bringing constructive and computable mathematics closer to programming practice. Journal of logic and computation, ISSN 0955-792X, 2009, vol. 19, no. 1, str. 17-43. [COBISS-SI-ID 15325785]
BAUER, Andrej, TAYLOR, Paul. The Dedekind reals in abstract Stone duality. Mathematical structures in computer science, ISSN 0960-1295, 2009, vol. 19, iss. 4, str. 757-838. [COBISS-SI-ID 15322201]
