SPL will comemorate every year the World Logic Day. The first edition will take place on January 15th, 2025, and will be held in a hybrid format, at the Mathematics Department of Técnico ULisboa, room 3.10, and virtually on Zoom.
PROGRAM
16h00-16h45
Gilda Ferreira (Universidade Aberta, CMAFcIO)
Unified framework for proof translations
Abstract: 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.
16h45-17h15 COFFEE BREAK
17h15-18h15
Marcelo Finger (Instituto de Matemática e Estatística, Universidade de São Paulo, Brazil)
Logic in Times of Big Data
Abstract: 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.
18h15-19h00
João Ribeiro (Instituto Superior Técnico e Instituto de Telecomunicações)
Randomness as a computational resource
Abstract: 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.