Pogojev za vključitev v delo ni.
Logika v računalništvu
2021/2022
Program:
Interdisciplinarni magistrski študijski program 2. stopnje Računalništvo in matematika
Letnik:
1 ali 2 letnik
Semester:
prvi ali drugi
Vrsta:
izbirni
Skupina:
A
ECTS:
6
Jezik:
slovenski, angleški
Nosilec predmeta:
Izvajalec (kontaktna oseba):
Ure na teden – 1. ali 2. semester:
Predavanja
3
Seminar
0
Vaje
0
Laboratorij
2
Vsebina
Vsebina je razdeljena na obvezni del in na izbrana poglavja. Obvezni del:
Sintaksa, formalni sistem, vezane spremenljivke, substitucija.
Lambda-račun in preprosti tipi.
Naravna dedukcija, izjavni račun, predikatni račun. Dokazni termi (proof terms).
Izbrana poglavja:
Curry-Howardova korespondenca
Konstruktivna interpretaciji logike, njen pomen za računalništvo.
Časovna logika in uporaba v računalništvu.
Modalna logika in uporaba pri modeliranju znanja.
Ostali računi: pi-račun , dogodkovni račun ipd.
Dokazovalniki izrekov.
Temeljni literatura in viri
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.
Cilji in kompetence
Cilj predmeta je študente spoznati s povezavami med logiko in računalništvom, saj je logika na mnogih področjih računalništva nepogrešljivo orodje. Študent bo spoznal matematično ozadje iz področja logike, ki ga bo nato lahko učinkovito uporabljal pri reševanju računalniških nalog.
Predvideni študijski rezultati
Znanje in razumevanje osnov matematične logike, predvsem v povezavi z računalništvom.
Metode poučevanja in učenja
Predavanja, vaje, konzultacije.
Načini ocenjevanja
Sprotno preverjanje (domače naloge, kolokviji in projektno delo).
Končno preverjanje (pisni in ustni izpit).
(ocene: 5 (negativno), 6-10 (pozitivno), ob upoštevanju Statuta UL)
Reference nosilca
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]
