Friday   November 7, 2025 - Andrea Volpi (Università di Udine)

Title:  Effectiveness and strong graph indivisibility

Abstract: A relational structure is strongly indivisible if for every partition M = X0 ⊔ X1, the induced substructure on X0 or X1 is isomorphic to M . Cameron (1997) showed that a graph is strongly indivisible if and only if it is the complete graph, the completely disconnected graph, or the random graph. We analyze the strength of Cameron’s theorem using tools from computability theory and reverse mathematics. We show that Cameron’s theorem is effective up to computable presentation, and give a partial result towards showing that the full theorem holds in the ω-model REC. We also establish that Cameron’s original proof makes essential use of the stronger induction scheme IΣ02. This is joint work with Damir Dzhafarov and Reed Solomon.

Thursday  July 17, 2025 - Giovanni Varricchione (Utrecht University)

Title:  Logic, Automata and Reinforcement Learning

Abstract:  In recent years, after many breakthroughs in neural machine learning, there has been a strong interest in combining neural approaches with notions and ideas typical of symbolic AI. This led to the birth of neuro-symbolic machine learning, a field encompassing all those approaches that combine the ability to reason typical of symbolic AI approaches to the generalizability of neural machine learning. 

In this talk, I will present my PhD research, which can be placed in the area of neuro-symbolic reinforcement learning. I will first give an overview of reinforcement learning, presenting background notions needed to make the talk as self-contained as possible. Then, I will present three of my published works. The first papers I will present will focus on reward machines, a recently proposed way of defining reward functions in reinforcement learning via automata. I will first show how it is possible to generate reward machines from partially-ordered plans and use them to train agents to achieve tasks in the most flexible way (Varricchione et al., ECAI 2024), and then how reward machines can be obtained from Alternating-time Temporal Logic specifications and used to train coalitions of agents (Varricchione et al., EUMAS 2023). The last paper I will present will instead focus on enforcing safety constraints in reinforcement learning. This is done by exploiting Pure-Past Linear-time Temporal Logic formulae, which are used to constrain action selection based on whether they are true or not given what has happened so far (Varricchione et al., AAAI 2024).

Tuesday  July 1, 2025  at 11:00 - Stefan Grosser (Mc Gill University)

Title:  Constructive Criticisms of Complexity: Unifying Proofs and Algorithms

Abstract: For decades, fundamental questions in complexity theory have remained wide open. A classic counting argument by Shannon shows that most Boolean functions on n bits require circuits of size 2^n/n, yet we lack even superlinear circuit size lower bounds for any explicit function in NP. This raises two natural questions: (i) can we make these counting arguments constructive, and (ii) why have we struggled so much to find an explicit hard function?

In this talk, we rigorously examine two algorithmic and metamathematical notions of constructivity in complexity theory, and how they are related to circuit lower bounds and barrier results. We will demonstrate that

(i) New constructive proofs of known nonconstructive lower bounds imply strong, breakthrough lower bounds.

(ii) Some nonconstructive proofs of lower bounds cannot be made constructive.

We show how these ideas can be used to make unconditional progress on an old question in proof complexity and bounded arithmetic.

Thursday  June 12, 2025  at 10:00 - Gabriele Buriola (Univeristà di Verona)

Title:  Ordinal analysis of Well-Ordering Principles and Well Quasi-Orders Closure Properties

Abstract: IThis talk explores a series of preservation principles concerning well-orders and well quasi-orders, wqo. Well-orders are foundational in mathematical logic, playing a central role in set theory—especially through the concept of ordinals—and in proof theory, notably in ordinal analysis, which aims to associate ordinals with formal theories. Given their importance, functions between well-orders are a natural subject of study, leading to the formulation of Well-Ordering Principles (WOP). For a function g from countable ordinals to countable ordinals, the principle WOP(g) formalizes the assertion: “For all α, if α is a well-order, then g(α) is a well-order.”

Well quasi-orders are the quasi-order analog of well-orders and are fundamental in areas ranging from combinatorics to theoretical computer science. Correspondingly, suitable analogs of WOPs can be defined for wqos. Specifically, for a set operation G that preserves the wqo property (such as disjoint union), the Well Quasi-order closure Property WQP(G) formalizes the statement: “For all Q, if Q is a wqo, then G(Q) is a wqo.”

In this talk, we present recent results concerning the ordinal and proof-theoretic analysis of WOPs and WQPs, focusing on variants of Kruskal’s Tree Theorem and operations such as the iterated union and product of wqos.

Thursday  MArch 27, 2025  at 13:00 - Jacobo Toràn  (University of ulm)

Title:  The complexity of Graph Isomorphism in Resolution

Abstract: In the talk I will present a connection between descriptive complexity and the resolution proof system,  by showing that the number of variables needed to distinguish a pair of graphs by  first-order logic sentences exactly matches the  clause width needed to refute the corresponding graph isomorphism formula in propositional narrow resolution. Using this connection, we obtain upper and lower bounds for refuting graph isomorphism formulas in (normal) resolution. In particular,  I will show that if $k$ is the minimum number of variables needed to distinguish two graphs with $n$ vertices each, then there is an $n^{\bigoh{k}}$ resolution refutation size upper bound for the corresponding isomorphism formula, as well as lower bounds of~$2^{k-1}$ and~$k$ for the tree-like resolution size for this formula. This also implies a general resolution size lower bound of ${\exp} \big( \bigomega{k^2/n} \big)$ for the case of colored graphs with constant color class sizes.Another consequence of the  results, is  an  exponential lower bound for graph isomorphism formulas in the proof system SRC-1, a system that extends resolution with a global symmetry rule.

Thursday  November 28, 2024  at 10:00 - Mauro di Nasso  (University of Pisa)

Title:  Arithmetic Ramsey Theory, a nonstandard take

Abstract: In recent years there has been a growing interest in Ramsey theory and related problems in combinatorics of numbers. Historically, the earliest results in this field are Schur's Theorem ("In every finite coloring of the naturals there exists a monochromatic triple a, b, a+b")and van der Waerden's Theorem ("In every finite coloring of the naturals there exist monochromaticarithmetic progressions of arbitrary length"). A peculiar aspect of this area of research is the wide variety of methods used: in addition to the tools of elementary combinatorics, also methods of discrete Fourier analysis, ergodic theory, and ultrafilter space algebra have been successfully applied. Recently, a further line of research has been undertaken, in which combinatorial properties of sets of integers are studied by methods of nonstandard analysis. In this seminar I will discuss these methods and present examples and new applications.

Monday  May  8/23  Alberto Marcone (Università di Udine)

Title:  3 is much larger than 2 in reverse mathematics

Abstract: A partial order is a well-partial order (wpo) if it does not contain infinite descending chains and infinite antichains. In the

1960's Nash-Williams introduced a strengthening of this notion, called better partial order (bpo), which has better closure properties than wpo

and was therefore used to show that many partial orders are wpo.  

In this talk we deal with the foundations of bpo theory from the viewpoint of reverse mathematics, a research program in mathematical logic that aims at establishing the weakest axioms needed to prove a statement. From this perspective, even the statement that finite partial orders are bpo is nontrivial. About twenty years ago I showed that "2 is bpo" (where 2 is the antichain with two elements) is provable in RCA0, the base theory of reverse mathematics, and asked about the strength of "3 is bpo". No progress was made on the question until last year, when Anton Freund showed that "3 is bpo" implies ACA0^+, providing a significant lower bound for the strength of the statement. Although the question is not completely settled yet (the upper bound is the stronger theory ATR0), we can now affirm that 3 is much larger than 2.

Building on this result, in recent work with Freund, Pakhomov and Soldà, we characterized the partial orders that a theory such as ACA0 (which does not prove that 3 is bpo) proves to be bpo.

Monday  Dec 5/22  Toni Huynh  (Sapienza University)

Title:  Strengthening Convex Relaxations of 0/1-Sets Using Boolean Formulas

Abstract: In this talk, we present a novel connection between circuit complexity and integer programming. In convex integer programming, various procedures have been developed to strengthen convex relaxations of sets of integer points.

On the one hand, there exist several general-purpose methods that strengthen relaxations without specific knowledge of the set of feasible integer points, such as popular linear programming or semi-definite programming hierarchies.  On the other hand, various methods have been designed for obtaining strengthened relaxations for very specific sets that arise in combinatorial optimization, such as the travelling salesman problem.

We propose a new efficient method that interpolates between these two approaches.  Our procedure strengthens any convex set containing a set S of 0/1-points by exploiting certain additional information about S.  Namely, the required extra information will be in the form of a Boolean formula F defining the target set S.  The new relaxation is obtained by "feeding'' the convex set S into the formula F.

We analyze various aspects regarding the strength of our procedure. As one application, interpreting an iterated application of our procedure as a hierarchy, our findings simplify, improve, and extend previous results by Bienstock and Zuckerberg on covering problems. This is joint work with Samuel Fiorini and Stefan Weltge.

Monday  Nov 21/22 - Luca San Mauro  (Sapienza University)

Title:  Learning families of algebraic structures

Abstract: Algorithmic Learning Theory (ALT), initiated by Gold and Putnam in the 1960s, comprehends several formal frameworks for the inductive inference. Broadly construed, ALT models the ways in which a learner may achieve systematic knowledge about a given environment, by accessing more and more data about it. In classical paradigms, the objects to be inferred are either formal languages or computable functions. In this talk, we present the following framework: An agent receives larger and larger pieces of an arbitrary copy of a countable structure and, at each stage, is required to output a conjecture about the isomorphism type of such a structure. The learning is successful if the conjectures eventually stabilize to a correct guess. We offer a complete model theoretic characterization of which families of structures are learnable. We also discuss a descriptive set theoretic interpretation of our framework, which allows us to define a hierarchy of non-learnability.

This is joint work with Nikolay Bazhenov, Vittorio Cipriani, and Ekaterina Fokina. 

Monday  Nov 14/22 -  Giuseppe Perelli (Sapienza University)

Title:    From Synthesis to Rational Synthesis: a Logic-Based Approach for Multi-Agent Systems Verification

Abstract: Synthesis is the problem of programming an intelligent agent and its interaction with the environment in a way that its behaviour is correct by construction, that is, it fulfils a given task no matter how the environment reacts. The solution to this problem can be interpreted as the winning strategy in a suitably defined two-player (formal) game. Rational Synthesis (RS) is a recent evolution of Synthesis, in which the setting is not viewed as an adversarial dispute, but rather as a Multi-Agent System, where each agent has their own specification. In terms of games, RS corresponds to no longer maximizing an individual payoff against all possible environment's behaviours (two-player zero-sum), but rather synthesising a strategy profile that is in some sort of equilibrium, i.e., prevents agents to improve payoff by deviating from it (multi-player nonzero-sum).

I will give an overview to the Synthesis and Rational Synthesis, presenting recent results and developments, and showing how the logic-based approach comes in very handy for representing and solving these problems. Finally, I will outline some current and future direction I am taking within the field.