{"id":773,"date":"2024-09-26T13:34:32","date_gmt":"2024-09-26T13:34:32","guid":{"rendered":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/?page_id=773"},"modified":"2026-01-07T17:44:02","modified_gmt":"2026-01-07T17:44:02","slug":"world-logic-day","status":"publish","type":"page","link":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/en\/world-logic-day\/","title":{"rendered":"World Logic Day"},"content":{"rendered":"\n<p>SPL will comemorate every year the <a href=\"https:\/\/www.unesco.org\/en\/days\/world-logic\">World Logic Day<\/a>.  The first edition took place on January 15th, 2025, and was held in a hybrid format,  at the Mathematics Department of T\u00e9cnico ULisboa, room 3.10, and <a rel=\"noreferrer noopener\" href=\"https:\/\/videoconf-colibri.zoom.us\/j\/92016223452?pwd=O57003PIx8ToRjcHlIun11DQALxekF.1\" target=\"_blank\">virtually on Zoom<\/a>.  <\/p>\n\n\n\n<p><\/p>\n\n\n\n<p><\/p>\n\n\n\n<p><font size=\"4\"><strong>PROGRAM<\/strong><\/font><strong> <\/strong><\/p>\n\n\n\n<p><strong>January 15th, 2025<\/strong><\/p>\n\n\n\n<p><\/p>\n\n\n\n<p><strong>16h00-16h45<\/strong><br><strong><a href=\"https:\/\/webpages.ciencias.ulisboa.pt\/~gmferreira\/\">Gilda Ferreira<\/a><\/strong> (Universidade Aberta, CMAFcIO)  <br><em> Unified framework for proof translations <\/em><br><strong> Abstract:<\/strong> Several proof translations exist between classical and intuitionistic logic (negative translations), as well as between intuitionistic and linear logic (Girard translations). These translations serve various purposes, including transferring properties between systems, simplifying proofs, facilitating the extraction of constructive computational content from proofs, and controlling the use of logical resources. In this presentation, we will show that all these systems can be expressed as extensions of a basic logical system (essentially, intuitionistic linear logic). By establishing a common logical basis, we are able to formalize a unified approach to devising and simplifying such proof translations. This approach clarifies the relationships between different logical systems, and reveals the underlying structure that connects them. Through this simplification process, we obtain the most well-known translations in the literature. This is joint work with Paulo Oliva and Clarence Protin.<\/p>\n\n\n\n<p><strong>16h45-17h15 COFFEE BREAK<\/strong><\/p>\n\n\n\n<p><strong>17h15-18h15<\/strong><br><a href=\"https:\/\/www.ime.usp.br\/mfinger\/\"><strong>Marcelo Finger<\/strong><\/a> (Instituto de Matem\u00e1tica e Estat\u00edstica, Universidade de S\u00e3o Paulo, Brazil)<br><em>Logic in Times of Big Data<\/em><br><strong>Abstract:<\/strong> In this talk, I will present a personal view of the area of Computational Logic and its future. Having developed a career in Computational Deductive Logic, and going through several forms of automated reasoning, from modal to sub-classical, to probabilistic and fuzzy, and fuzzy-probabilistic reasoning, since the pandemic I find myself immersed in Big Data research. Neural networks are as much part of my research activities as is Logic. I will talk about these developments and report on the search to put those two areas together. I will describe recent work on Lukasiewicz infinitely-valued logics and its use in the representation piecewise linear function, and how this can be used to formally prove properties of neural networks, such as reachability and robustness. I will summarize with a few comments on future research and challenges for the area.<\/p>\n\n\n\n<p><strong>18h15-19h<\/strong>00<br><strong><a href=\"https:\/\/math.tecnico.ulisboa.pt\/faculty\/professor?who=jribeiro\">Jo\u00e3o Ribeiro<\/a><\/strong> (Instituto Superior T\u00e9cnico e Instituto de Telecomunica\u00e7\u00f5es)<br><em>Randomness as a computational resource<\/em><br><strong>Abstract:<\/strong> Randomness is a fundamental concept in the sciences at large. Algorithms that use randomness are often simpler and faster than their deterministic counterparts, and revolutionary technologies, such as a secure Internet, would not exist without it. Generating high quality randomness is not easy, and so we may see it as an important computational resource, just like time and space. In this talk, I will discuss how thinking about randomness as a computational resource has led to fruitful research directions and unexpected applications in computer science.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>SPL will comemorate every year the World Logic Day. The first edition took place on January 15th, 2025, and was held in a hybrid format, at the Mathematics Department of T\u00e9cnico ULisboa, room 3.10, and virtually on Zoom. PROGRAM January 15th, 2025 16h00-16h45Gilda Ferreira (Universidade Aberta, CMAFcIO) Unified framework for proof translations Abstract: Several proof &hellip;<\/p>\n<p class=\"read-more\"> <a class=\"\" href=\"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/en\/world-logic-day\/\"> <span class=\"screen-reader-text\">World Logic Day<\/span> Read More &raquo;<\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"site-sidebar-layout":"default","site-content-layout":"default","ast-global-header-display":"","ast-main-header-display":"","ast-hfb-above-header-display":"","ast-hfb-below-header-display":"","ast-hfb-mobile-header-display":"","site-post-title":"","ast-breadcrumbs-content":"","ast-featured-img":"","footer-sml-layout":"","theme-transparent-header-meta":"","adv-header-id-meta":"","stick-header-meta":"","header-above-stick-meta":"","header-main-stick-meta":"","header-below-stick-meta":"","footnotes":""},"_links":{"self":[{"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/pages\/773"}],"collection":[{"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/comments?post=773"}],"version-history":[{"count":8,"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/pages\/773\/revisions"}],"predecessor-version":[{"id":956,"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/pages\/773\/revisions\/956"}],"wp:attachment":[{"href":"https:\/\/groups.tecnico.ulisboa.pt\/~spl.daemon\/wp-json\/wp\/v2\/media?parent=773"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}