Na Seminaru za matematičku logiku i računarstvo, u ponedjeljak 1. 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

 

Sažetak:  U [1] predstavljen je ne-dobro utemeljen sistem sekvenata za logiku interpretabilnosti IL. Na prethodnim seminarima LORA-e dokazana je njegova potpunost i adekvatnost za IL obzirom na Verbruggeinu semantiku. Također je na tim seminarima dan pregled rezultata iz literature o eliminaciji reza za IL upotrebom postojećih (dobro utemeljenih) sistema sekvenata za IL. Primjerice, dan je pregled rezultata iz [3]. Istaknuto je da su dokazi tih rezultata tehnički komplicirani.

 

Na ovome seminaru prvo ćemo dati kratki podsjetnik na novi sistem sekvenata iz [1] te na koalgebarsku metodu translacije dokaza iz [2]. Zatim ćemo primijeniti tu metodu kako bismo dokazali 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/96058944808?pwd=oqRzodzkoakqUOc8tOkXUlwBdxOxHW.1