{"id":4291,"date":"2021-02-10T14:13:29","date_gmt":"2021-02-10T13:13:29","guid":{"rendered":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/?p=4291"},"modified":"2021-05-27T20:53:10","modified_gmt":"2021-05-27T18:53:10","slug":"lira-session-bahareh-afshari-2","status":"publish","type":"post","link":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/2021\/02\/lira-session-bahareh-afshari-2\/","title":{"rendered":"LIRa Session: Guillermo Men\u00e9ndez Turata"},"content":{"rendered":"

Speaker: Guillermo Men\u00e9ndez Turata<\/p>\n

Date and Time: Thursday, June 3rd 2021, 16:30-18:00, Amsterdam time<\/a>.<\/p>\n

Venue: online<\/a><\/strong>.<\/p>\n

Title: Uniform interpolation from cyclic proofs: the case of modal mu-calculus.<\/b>
\n<\/strong><\/p>\n

Abstract. <\/em>Uniform interpolation was first established for the modal mu-calculus by D\u2019Agostino and Hollenberg via a combination of semantic and syntactic methods. A natural question is whether a purely syntactical proof of this result, in the style of Pitt\u2019s seminal work on uniform interpolation for intuitionistic logic, can be produced. One possible reason Pitt\u2019s method has not been applied to the modal mu-calculus is that it requires a setting where uniform interpolation can be proved by induction on cut-free derivations in a finitary system. While it is feasible to design cut-free calculi for fixpoint modal logics, they are often infinitary, i.e., derivations may have infinite branches. In this talk we apply Pitt\u2019s technique to the modal mu-calculus and show how to construct uniform interpolants from cyclic derivations in an annotated goal-oriented proof system introduced by Jungteerapanich and Stirling.<\/p>\n","protected":false},"excerpt":{"rendered":"

Speaker: Guillermo Men\u00e9ndez Turata
\nDate and Time: Thursday, June 3rd 2021, 16:30-18:00, Amsterdam time.
\nVenue: online.
\nTitle: Uniform interpolation from cyclic proofs: the case of modal mu-calculus.<\/p>\n

Abstract. Uniform interpolation was first established for the modal mu-calculus by D\u2019Agostino and Hollenberg via a combination of semantic and syntactic methods. A natural question is whether a purely syntactical proof of this […]<\/p>\n","protected":false},"author":12,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[4],"tags":[],"class_list":["post-4291","post","type-post","status-publish","format-standard","hentry","category-events"],"_links":{"self":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/4291","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/users\/12"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/comments?post=4291"}],"version-history":[{"count":3,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/4291\/revisions"}],"predecessor-version":[{"id":4404,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/posts\/4291\/revisions\/4404"}],"wp:attachment":[{"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/media?parent=4291"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/categories?post=4291"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/projects.illc.uva.nl\/lgc\/seminar\/wp-json\/wp\/v2\/tags?post=4291"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}