Friday, June 16, 2023 | 12:30 pm (CET) | Room: S.2.69 | Alpen-Adria Universität Klagenfurt
Univ.-Prof.in Dr.in Martina Seidl | Institute for Symbolic Artificial Intelligence | JKU Linz
Abstract: As the prototypical NP-complete problem SAT, the decision problem of propositional logic, is considered to be hard. Despite this hardness, SAT is very successfully applied in many practical domains, because very powerful reasoning techniques are available. There are, however, problems that cannot be efficiently encoded in SAT. For such problems, formalisms with decision problems beyond NP are necessary. One of such formalisms are quantified Boolean formulas (QBFs), the extension of propositional logic with existential and universal quantifiers over the Boolean variables. The QBF decision problem is PSPACE-complete, making QBF well suitable for encoding and solving many problems from formal verification, synthesis, and artificial intelligence. In this talk, we give a short tour through recent developments in QBF solving.
Bio: Martina Seidl is a full professor of artificial intelligence at the Johannes Kepler University (JKU) in Linz. She obtained her PhD from TU Wien where she worked several years in the Business Informatics Group. In 2010, she became assistant professor and in 2016 associate professor at the Institute for Formal Models and Verification of the JKU. Since 2020 she is head of the Institute for Symbolic Artificial Intelligence. In her research, she develops symbolic reasoning techniques based on computational logic. She especially focuses on the theory and practice of quantified Boolean formulas (QBFs) and their applications in the context of formal verification and artificial intelligence.





Bio: Laura Toni received the M.S. and Ph.D. degrees, both in electrical engineering, from the University of Bologna, Bologna, Italy, in 2005 and 2009, respectively. In 2007, she was a Visiting Scholar at the University of California at San Diego (UCSD), San Diego, CA, USA, and since 2009, she has been a frequent visitor to the UCSD, working on media coding and streaming technologies. Between 2009 and 2011, she was with the Tele-Robotics and Application Department, Italian Institute of Technology, investigating wireless sensor networks for robotics applications. In 2012, she was a Postdoctoral Fellow at UCSD, and between 2013 and 2016, she was a Postdoctoral Fellow in the Signal Processing Laboratory (LTS4) at École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland. Since July 2016, she has been a Lecturer in the Electronic and Electrical Engineering Department, University College London (UCL), U.K. Her research mainly involves interactive multimedia systems, decision-making strategies under uncertainty, large-scale signal processing, and communications. She received the UCL Future Leadership Award in 2016, the ACM Best 10% Paper Award in 2013, and the IEEE/IFIP Best Paper Award in 2012.
Bio: Lucia D’Acunto received her PhD in 2012 from Delft University of Technology, the Netherlands, with a thesis on video streaming over peer-to-peer networks. She now works as a senior research scientist at TNO, focusing on video distribution and on the impact of future internet architectures (e.g. ICN, SDN and 5G) on it. She has led and is leading various European research projects on these topics, most notably the open call projects from the European Projects TRIANGLE, 5GINFIRE and FLAME. Since 2016, Lucia is an active participant and contributor to the 3GPP SA4 group, which focusses on mobile and 5G standardization for media applications. Lucia also serves in the organizing committees of several international conferences, usually in the roles of program chair or demo chair, and in the program committees. Lucia also regularly advises European operators on network and TV technologies and contributes to 5GPPP and NEM visions on the 5G Media Vertical and pilots. Lucia has published her research in several papers and journals and holds more than 15 patent applications.