Na Seminaru za matematičku logiku i računarstvo, u ponedjeljak 8. lipnja 2026. u 17:15 sati, u predavaonici 105, PMF-MO,

Sebastijan Horvat održat će predavanje 

 

Eliminacija reza za logiku interpretabilnosti IL upotrebom koalgebarske translacije dokaza (2)

 

Sažetak:  Na prošlom seminaru napravili smo kratki podsjetnik na novi sistem sekvenata iz [1] te koalgebarsku metodu translacije dokaza iz [2]. Također smo istaknuli uvjete za primjenu te metode kao i dovoljne uvjete koje je potrebno ispuniti za eliminabilnost nekog pravila u sistemu. Na ovome seminaru dokazat ćemo rezultat eliminacije reza za logiku interpretabilnosti IL. Opravdat ćemo da je rezultat dobiven na jednostavniji način nego, primjerice, u [3].

 

[1] Horvat, S., Sierra Miranda, B., Studer, T. (2026). Non-wellfounded Proof Theory for Interpretability Logic. In: Pozzato, G.L., Uustalu, T. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2025. Lecture Notes in Computer Science(), vol 15980. Springer, Cham.

[2] Miranda, B.S., Studer, T., Zenger, L. (2024). Coalgebraic proof translations of non-wellfounded proofs. In: Ciabattoni, A., Gabelaia, D., Sedlar, I. (eds.) Advances in Modal Logic, vol. 15, pp. 527–548. College Publications

[3] Sasaki, K. (2002). A cut-free sequent system for the smallest interpretability logic. Studia Logica 70, 353–372

 

Link za Zoom prijenos: https://zoom.us/j/94309747954?pwd=D94gl2kRVFta2dxpGewgx65j9b2Ky7.1