Přednáška si klade za cíl seznámit s obecnou teorií substrukturálních logik. Důraz bude kladen na algebraické
metody používané v této teorii. Předpokládá základní znalost universální algebry.
Poslední úprava: IUUK (25.03.2013)
The lecture's aim is to introduce the general theory of substructural logics. We will focus on
algebraic methods applied in this theory. Basic knowledge of universal algebra is assumed.
Literatura -
Poslední úprava: IUUK (04.04.2013)
[1] N. Galatos, P. Jipsen, T. Kowalski, H. Ono. Residuated Lattices: an algebraic glimpse at substructural logics. Studies in Logics and the Foundations of Mathematics, Elsevier, 2007.
[2] N. Galatos, P. Jipsen. Residuated Frames. To appear in Transactions of AMS.
[3] V. Pratt. Action logic and pure induction. In: J. van Eijck (ed.), Logics in AI, LNAI
478, 1991, 97-120.
[4] C. Retoré. The Logic of Categorial Grammars: Lecture Notes. Report N° RR-5703, INRIA, 2005 (http://hal.archives-ouvertes.fr/docs/00/07/03/13/PDF/RR-5703.pdf).
Poslední úprava: IUUK (04.04.2013)
[1] N. Galatos, P. Jipsen, T. Kowalski, H. Ono. Residuated Lattices: an algebraic glimpse at substructural logics. Studies in Logics and the Foundations of Mathematics, Elsevier, 2007.
[2] N. Galatos, P. Jipsen. Residuated Frames. To appear in Transactions of AMS.
[3] V. Pratt. Action logic and pure induction. In: J. van Eijck (ed.), Logics in AI, LNAI
478, 1991, 97-120.
[4] C. Retoré. The Logic of Categorial Grammars: Lecture Notes. Report N° RR-5703, INRIA, 2005 (http://hal.archives-ouvertes.fr/docs/00/07/03/13/PDF/RR-5703.pdf).
Sylabus -
Poslední úprava: IUUK (25.03.2013)
Přednáška si klade za cíl seznámit s obecnou teorií substrukturálních logik. První část přednášky bude věnována původním motivacím, které pocházejí z teorie důkazů. Definujeme formálně substrukturální logiky jako rozšíření logiky FL (Full Lambek calculus). Další část se bude zabývat teorií residuovaných svazů, které hrají roli algebraické sémantiky pro substrukturální logiky podobně jako Booleovské algebry tvoří algebraickou sémantiku pro klasickou logiku. Zavedeme pojem residuovaného rámce s jehož pomocí ukážeme, že jednotlivé substrukturální logiky jsou úplné vůči odpovídajícím varietám residuovaných svazů. Dále zmíníme některé další aplikace residuovaných rámců na výpočetní aspekty substrukturálních logik. Závěr bude věnován některým souvislostem a aplikacím substrukturálních logik v teoretické informatice.
Důkazově teoretická motivace substrukturalních logik [1]: pojem substrukturálních logik, sekventového kalkulu, strukturální pravidlo, základní substrukturální logiky.
Algebraická sémantika substrukturálních logik [1]: residuované svazy a jejich vlastnosti.
Relační sémantika [2]: residuované rámce a jejich aplikace, úplnost, (ne)rozhodnutelnost.
Některé aplikace: kategoriální gramatiky [4], action algebras [3].
Poslední úprava: IUUK (25.03.2013)
The lecture's aim is to introduce the general theory of substructural logics. The first part of the lecture will be devoted to original motivations, which come from proof theory. We will formally define substructural logics as extensions of Full Lambek calculus. The next part of the lecture will deal with the theory of residuated lattices, which play the role of algebraic semantics of sobstructural logics, in analogy with Boolean algebras forming the algebraic semantics of classical logic. We will introduce the concept of residuated frame and use it to prove that individual substructural logics are complete with respect to the corresponding varieties of residuated lattices. We will then mention some further applications of residuated frames to computational aspects of substructural logics. Finally, we will deal with some connections and applications of substructural logics to theoretical computer science.
Proof theoretic motivation of substructural logics [1]: the notion of substructural logic, sequent calculus, structural rule, basic substructural logics.
Algebraic semantics of substructural logics [1]: residuated lattices and their properties.
Relational semantics [2]: residuated frames and their applications, completeness, (un)decidability.
Some applications: categorial grammars [4], action algebras [3].
