Učitavanje video playera...
01:12:45
Sebastijan Horvat: Eliminacija reza za IL upotrebom koalgeb. translacije dokaza
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
