[DL] Spotlight seminar Roberto Sebastiani

[Luciano Serafini]

[* Apologies in case of multiple posting *]

The Italian Association for Artificial Intelligence is pleased to announce the next seminar of its Spotlight Seminars on AI initiative:

Date and Time: October, 29  2026 – 5:00 PM (CET)

Online attendance: The seminars will be held virtually on the YouTube channel of the Association (https://www.youtube.com/c/AIxIAit), 

Title: Compile Once, Reason Fast: From Satisfiability to Knowledge Compilation Modulo Theories

Speaker: Prof. Roberto Sebastiani- University of Trento

Abstract: Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a logical formula representing facts in given domains of interest (e.g., linear or non-linear arithmetic over the reals or the integers, arrays, strings, bit-vectors and floating-point numbers, and their combinations thereof). In the last two decades, we have witnessed a dramatic improvement in both efficiency and expressiveness of SMT solvers, together with their skyrocketing diffusion as workhorse reasoning engines in many industrial application domains, in particular in software and hardware verification. Despite their increasing adoption in domains like planning and Neuro-symbolic AI, SMT technologies have penetrated AI communities far less dramatically. This may be mainly because, in most AI applications, tools are expected to provide very fast replies to queries, which standard SMT solvers cannot guarantee. These considerations motivate the content of this talk. First, I will provide an overview of SMT and of its main applications, including some less-known SMT functionalities (e.g., SMT optimization, enumeration & counting). Second, I will introduce an extension of SMT we have recently proposed, namely Knowledge Compilation Modulo Theories (KCMT), which combines SMT with propositional Knowledge Compilation (KC). I will describe the main ideas, functionalities, and formal results about KCMT, and suggest a list of potential AI applications. As with propositional KC, the general idea for KCMT is to push as much of the computational effort of SMT reasoning into the off-line compilation phase of a knowledge base, which may be computationally demanding, but which allows for very-fast on-line queries and whose costs are thus amortized over all on-line queries. Using a machine-learning analogy, we "train" a knowledge base offline using a large set of logical lemmas, so it can perform very-fast online logical reasoning.

Sort Bio: Roberto Sebastiani is a Full Professor of Artificial Intelligence, Automated Reasoning, and Formal Methods at the Department of Information Engineering and Computer Science (DISI) of the University of Trento in Italy. Sebastiani's academic and research career focuses heavily on logic and computation. He is widely recognized in the fields of automated reasoning and formal verification. His publication record spans more than 30 years, including several papers in the Artificial Intelligence Journal and JAIR. He has served on the steering and program committees of many conferences, and as co-chair of the SAT 2012 and IJCAR 2018 conferences. His primary area of expertise is Satisfiability Modulo Theories (SMT) and its extensions and applications, whose foundation and developments he has largely contributed to, and for which he is a co-recipient of the Computer-Aided Verification Award (2021) and of the Thoralf Skolem Award (2023).

AIXIA spotlight seminars: The seminar series aims to illustrate, explore and discuss current scientific challenges, trends, and possibilities in all branches of our articulated research field. The seminars will be held virtually on the YouTube channel of the Association (https://www.youtube.com/c/AIxIAit), every month (and made permanently available on that channel), by leading Italian researchers as well as by top international scientists. 

The seminars are mainly aimed at a broad audience interested in AI research, and they are also included in the Italian PhD programme in Artificial Intelligence; indeed, AIxIA warmly encourages the attendance of young scientists and PhD students. 

—
The Spotlight Seminars on AI Committee, 

Giuseppe De Giacomo
Luciano Serafini
Mauro Vallati
-- 
--
Le informazioni contenute nella presente comunicazione sono di natura 
privata e come tali sono da considerarsi riservate ed indirizzate 
esclusivamente ai destinatari indicati e per le finalità strettamente 
legate al relativo contenuto. Se avete ricevuto questo messaggio per 
errore, vi preghiamo di eliminarlo e di inviare una comunicazione 
all’indirizzo e-mail del mittente.

--
The information transmitted is 
intended only for the person or entity to which it is addressed and may 
contain confidential and/or privileged material. If you received this in 
error, please contact the sender and delete the material.