20.500.12556/RUL-174150 Eliminacija rezov v linearni logiki delo diplomskega seminarja Cut elimination in linear logic Vpeljemo sekventni račun, njegova strukturna pravila ter logični pravili za veznik $\land$, nato pa se omejimo na linearno logiko ter veznik $\land$ razdelimo na dva. Vpeljemo še vse ostale veznike v linearni logiki ter razložimo njihov pomen, nato vpeljemo pravilo reza. Formuliramo izrek o eliminaciji reza, nato vsakemu rezu pripišemo mero, imenovano stopnja, in izrek dokažemo z dvojno indukcijo, zunanjo na številu rezov v drevesu izpeljave, notranjo na stopnji reza. Znotraj indukcije ločimo primere glede vrsto reza in rezani veznik. Definiramo glavni rez in mu znižamo stopnjo za vsak veznik posebej, pri eksponentih pa definiramo še posplošeni rez in mu nato znižamo stopnjo. Rezu (in posplošenemu rezu) znižamo stopnjo tudi, ko ni glaven, nato pa se lotimo še baze indukcije, s čimer zaključimo dokaz izreka. We introduce sequent calculus, its structural rules and the logical rules for the logical connective $\land$. We then limit the sequent calculus to linear logic nad split $\land$ into two connectives. We further introduce all other connectives in linear logic and explain their interpretations, then we introduce the cut rule. We formulate the cut elimination theorem then ascribe a numeric value, called degree, to each cut and prove the theorem using double induction, the outer induction on the number of cuts in the proof tree, the inner induction on the degree of the cut. Within the induction we split cases based on the type of cut and the formula being cut. We define the principal cut and lower its degree it for each connective seperately. We define the generalised cut rule for the exponentials and lower its degree. We lower the degree of the non-principal cut rule (and the non-principal generalised cut rule) and then proceed to the induction base, with which we finish the proof. sekventni račun linearna logika eliminacija rezov sequent calculus linear logic cut elimination true false false Slovenski jezik Angleški jezik Delo diplomskega seminarja/zaključno seminarsko delo/naloga 2025-09-28 08:15:04 2025-09-28 08:15:09 2025-11-18 03:57:30 0000-00-00 00:00:00 2025 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 510.6 154856 251008515 20369.pdf 20369.pdf 1 6290DABAF972B8CA6AC9E9CE41F80EAB 295614bab054d26bea79e3f8f4a68a61b1e27350b6024f04c9cd5cf2eb8a4ec3 4aec4db6-9c32-11f0-9328-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=218910 Fakulteta za matematiko in fiziko 0 0 0