<?xml version="1.0"?>
<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:dc="http://purl.org/dc/elements/1.1/"><rdf:Description rdf:about="https://repozitorij.uni-lj.si/IzpisGradiva.php?id=139401"><dc:title>Curry-Howardova korespondenca</dc:title><dc:creator>Korenjak,	Neža	(Avtor)
	</dc:creator><dc:creator>Bauer,	Andrej	(Mentor)
	</dc:creator><dc:subject>teorija tipov</dc:subject><dc:subject>lambda račun</dc:subject><dc:subject>intuicionistična logika</dc:subject><dc:subject>dedukcija</dc:subject><dc:subject>Curry-Howardova korepondenca</dc:subject><dc:description>Teorija tipov je teorija matematičnih konstrukcij. Tipi niso le zbirke objektov, tako kot množice, ampak dopustni načini konstrukcije objektov. Zato elementov tipa ne določa zgolj njihova vsebovanost, ampak predvsem način konstrukcije. Intuicionistična logika je logični sistem, kjer veljavnost izjave ne temelji na njeni resničnostni vrednosti, pač pa na obstoju konstrukcije oziroma dokaza te izjave. Izkaže se, da med teorijo tipov in intuicionistično logiko obstaja naravna povezava, imenovana Curry-Howardov izomorfizem ali korespondenca, ki nam pokaže, kako se izjave v logiki lahko pretvorijo v tipe, njihovi dokazi pa v elemente ustreznih tipov.</dc:description><dc:date>2022</dc:date><dc:date>2022-09-02 08:15:07</dc:date><dc:type>Delo diplomskega seminarja/zaključno seminarsko delo/naloga</dc:type><dc:identifier>139401</dc:identifier><dc:language>sl</dc:language></rdf:Description></rdf:RDF>