Logic Seminar

Research Center for Logic, Optimization and Security (LOS), FMI, UB

Organizers: Laurențiu Leuștean, Andrei Sipoș

The logic seminar features talks on
mathematical logic,
philosophical logic and
logical aspects of computer science.
The seminars are online, using Google Meet as the underlying platform. All seminars, except where otherwise indicated, will be at 10:00.

Past Seminars

    Our logo is designed by Claudia Chiriță.

Talks in 2020-2021

Thursday, June 3, 2021

Gabriel Ciobanu (Alexandru Ioan Cuza University of Iași and Romanian Academy (ICS))
Choice principles and infinities for finitely supported structures

Abstract: Finitely supported structures are related to permutation models of Zermelo-Fraenkel set theory with atoms (ZFA) and to the theory of nominal sets. They were originally introduced in 1930s by Fraenkel, Lindenbaum and Mostowski to prove the independence of the axiom of choice and the other axioms in ZFA. We use a set theory defined by the axioms of ZFA set theory extended with an additional axiom for finite support. The consistency (validity) of choice principles in various models of Zermelo-Fraenkel set theory (ZF) and of ZFA (including the symmetric models and the permutation models) was investigated deeply in the last century. The choice axiom was proved to be independent from the axioms of ZF and ZFA. In the new theory of finitely supported structures, we analyze the consistency of various choice principles (and equivalent/related results), as well as the consistency of results regarding cardinality and infinity. We prove the inconsistency of choice principles for finitely supported structures (i.e., their formulations with respect to the finite support requirement are not valid). Related to this inconsistency of choice principles, we present some pairwise non-equivalent definitions for the notion of infinity (difficult to imagine, we have seven forms of infinity for finitely supported structures). We compare these forms, and present examples of atomic sets satisfying a certain form of infinity, while they do not satisfy others. In particular, we focus on the notion of Dedekind infinity and on uniformly supported sets.

[1] A. Alexandru, G. Ciobanu, Foundations of Finitely Supported Structures: a set theoretical viewpoint, Springer, 2020.

Thursday, May 27, 2021

Cătălin Dima (University Paris-Est Créteil)
Rational Synthesis in the Commons with Careless and Careful Agents

Abstract: Turn-based multi-agent games on graphs are games where the states are controlled by a single player who decides which edge to follow. Each player has a temporal objective that he tries to achieve, and one player is the designated `controller', whose objective captures the desirable outcomes of the whole system. Cooperative rational synthesis is the problem of computing a Nash equilibrium (w.r.t. the individual temporal objectives) that satisfies the controller’s objective. In this presentation, we tackle this problem in the context where each action has a cost or a benefit on one shared common pool energy resource. The paper investigates the problem of synthesizing the controller such that there exists an individually rational behavior of all the agents that satisfies the controller's objective and does not deplete the resource. We consider two types of agents: careless and careful. Careless agents only care for their temporal objective, while careful agents also pay attention not to deplete the system's resource. We study the complexity of the problem of cooperative rational synthesis with parity or Büchi objectives, careful or careless agents, and costs encoded in binary or unary.
Based on joint work with Rodica Condurache (Alexandru Ioan Cuza University of Iași), Youssouf Oualhadj (University Paris-Est Créteil) and Nicolas Troquard (Free University of Bozen-Bolzano).

Thursday, May 20, 2021

Florin Crăciun (Babeș-Bolyai University)

Thursday, May 13, 2021

Bruno Dinis (University of Lisbon)
Functional interpretations for nonstandard arithmetic

Abstract: In the past few years there has been a growing interest in trying to make explicit constructive aspects of nonstandard methods with the use of functional interpretations. Functional interpretations are maps of formulas from the language of one theory into the language of another theory, in such a way that provability is preserved. These interpretations typically replace logical relations by functional relations. Functional interpretations have many uses, such as relative consistency results, conservation results and extraction of computational content from proofs. After giving a short introduction to nonstandard analysis, I will present several recent functional interpretations in the context of nonstandard arithmetic as well as some results that come from these interpretations.

[1] B. van den Berg, E. Briseid, P. Safarik, A functional interpretation for nonstandard arithmetic. Ann. Pure Appl. Logic 163 (2012), no. 12, 1962-1994.
[2] B. Dinis, J. Gaspar, Intuitionistic nonstandard bounded modified realisability and functional interpretation. Ann. Pure Appl. Logic 169 (2018), no. 5, 392-412.
[3] B. Dinis, J. Gaspar, Hardwiring t-truth in functional interpretations. In preparation.
[4] B. Dinis, É. Miquey, Realizability with stateful computations for nonstandard analysis. 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), 19:1-19:23.
[5] F. Ferreira, J. Gaspar, Nonstandardness and the bounded functional interpretation. Ann. Pure Appl. Logic 166 (2015), no. 6, 701-712.
[6] S. Sanders, The unreasonable effectiveness of nonstandard analysis. J. Logic Comput. 30 (2020), no. 1, 459-524.

Thursday, April 22, 2021

Gabriel Istrate (West University of Timișoara)
Kernelization, Proof Complexity and Social Choice

Abstract: We display an application of the notions of kernelization and data reduction from parameterized complexity to proof complexity: Specifically, we show that the existence of data reduction rules for a parameterized problem having (a). a small-length reduction chain, and (b). small-size (extended) Frege proofs certifying the soundness of reduction steps implies the existence of subexponential size (extended) Frege proofs for propositional formalizations of the given problem. We apply our result to infer the existence of subexponential Frege and extended Frege proofs for a variety of problems. Improving earlier results of Aisenberg et al. (ICALP 2015), we show that propositional formulas expressing (a stronger form of) the Kneser-Lovasz Theorem have polynomial size Frege proofs for each constant value of the parameter $k$. Previously only quasipolynomial bounds were known (and only for the ordinary Kneser-Lovasz Theorem). Another notable application of our framework is to impossibility results in computational social choice: we show that, for any fixed number of agents, propositional translations of the Arrow and Gibbard-Satterthwaite impossibility theorems have subexponential size Frege proofs.
This is joint work with Cosmin Bonchiș and Adrian Crăciun.

Thursday, April 15, 2021

Dorel Lucanu (Alexandru Ioan Cuza University of Iași)
(Co)Initial (Co)Algebra Semantics in Matching Logic

Abstract: Matching logic is a unifying foundational logic for defining formal programming language semantics, which adopts a minimalist design with few primitive constructs that are enough to express all properties within a variety of logical systems, including FOL, separation logic, (dependent) type systems, modal mu-logic, and more. In this presentation, we will show how the initial algebra semantics and the final (coinitial) coalgebra semantics are captured as theories in Matching Logic. The presentation will be examples-based.
This is joint work with Xiaohong Chen and Grigore Roșu.

[1] X. Chen, D. Lucanu, G. Roșu. Matching logic explained. Journal of Logical and Algebraic Methods in Programming 120 (2021), 100638.
[2] X. Chen, D. Lucanu, G. Roșu. Initial algebra semantics in matching logic. UIUC Technical Report (2020).

Thursday, April 8, 2021

Gheorghe Ştefănescu (University of Bucharest)
Adaptive Virtual Organisms: A Compositional Model for Complex Hardware-software Binding

Abstract: The relation between a structure and the function it runs is of interest in many fields, including computer science, biology (organ vs. function) and psychology (body vs. mind). Our paper addresses this question with reference to computer science recent hardware and software advances, particularly in areas as Robotics, Self-Adaptive Systems, IoT, CPS, AI-Hardware, etc.
At the modelling, conceptual level our main contribution is the introduction of the concept of ``virtual organism" (VO), to populate the intermediary level between reconfigurable hardware agents and intelligent, adaptive software agents. A virtual organism has a structure, resembling the hardware capabilities, and it runs low-level functions, implementing the software requirements. The model is compositional in space (allowing the virtual organisms to aggregate into larger organisms) and in time (allowing the virtual organisms to get composed functionalities).
The virtual organisms studied here are in 2D (two dimensions) and their structures are described by 2D patterns (adding time, we get a 3D model). By reconfiguration, an organism may change its structure to another structure in the same 2D pattern. We illustrate the VO concept with a few increasingly more complex VO’s dealing with flow management or a publisher-subscriber mechanism for handling services. We implemented a simulator for a VO, collecting flow over a tree-structure (TC-VO), and the quantitative results show reconfigurable structures are better suited than fixed structures in dynamically changing environments.
Finally, we briefly show how Agapia - a structured parallel, interactive programming language where dataflow and control flow structures can be freely mixed - may be used for getting quick implementations for VO’s simulation.

[1] C. I. Păduraru, G. Ştefănescu. Adaptive virtual organisms: A compositional model for complex hardware-software binding. Fundamenta Informaticae 173, no. 2-3, 139-176, 2020.

Thursday, April 1, 2021

Alexandru Dragomir (University of Bucharest)
An Introduction to Protocols in Dynamic Epistemic Logic

Abstract: Dynamic epistemic logics are useful in reasoning about knowledge and acts of learning, seen as epistemic actions. However, not all epistemic actions are allowed to be executed in an initial epistemic model, and this is where the concept of a protocol comes in: a protocol stipulates what epistemic actions are allowed to be performed in a model. The aim of my presentation is to introduce the audience to two accounts of protocols in DEL: Hoshi's [1], and Wang's [2].

[1] T. Hoshi. Epistemic dynamics and protocol information. PhD thesis, Stanford, CA, USA. AAI3364501 (2009).
[2] Y. Wang. Epistemic Modelling and Protocol Dynamics. PhD thesis, University of Amsterdam. (2010).

Thursday, March 25, 2021

Mircea Marin (West University of Timișoara)
Regular matching problems for infinite trees

Abstract: We study the matching problem ``$\exists\sigma:\sigma(L)\subseteq R$?" where $L,R$ are regular tree languages over finite ranked alphabets $X$ and $\Sigma$ respectively, and $\sigma$ is a substitution such that $\sigma(x)$ is a set of trees in $T(\Sigma\cup H)\setminus H$ for all $x\in X$. Here, $H$ denotes a set of holes which are used to define a concatenation of trees. Conway studied this problem in the special case for languages of finite words in his classical textbook ``Regular algebra and finite machines" and showed that if $L$ and $R$ are regular, then the problem ``$\exists \sigma:\forall x\in X:\sigma(x)\neq\emptyset\wedge\sigma(L)\subseteq R$?" is decidable. Moreover, there are only finitely many maximal solutions, which are regular and effectively computable. We extend Conway's results when $L,R$ are regular languages of finite and infinite trees, and language substitution is applied inside-out. We show that if $L\subseteq T(X)$ and $R\subseteq T(\Sigma)$ are regular tree languages then the problem ``$\exists\sigma\forall x\in X:\sigma(x)\neq\emptyset\wedge\sigma_{io}(L)\subseteq R$?" is decidable. Moreover, there are only finitely many maximal solutions, which are regular and effectively computable. The corresponding question for the outside-in extension $\sigma_{oi}$ remains open, even in the restricted setting of finite trees. Our main result is the decidability of ``$\exists\sigma:\sigma_{io}(L)\subseteq R$?" if $R$ is regular and $L$ belongs to a class of tree languages closed under intersection with regular sets. Such a special case pops up if $L$ is context-free.
This is joint work with Carlos Camino, Volker Diekert, Besik Dundua and Géraud Sénizergues.

[1] C. Camino, V. Diekert, B. Dundua, M. Marin, G. Sénizergues, Regular matching problems for infinite trees, arXiv:2004.09926 [cs.FL], 2021.

Thursday, March 18, 2021

Andrei Sipoș (University of Bucharest)
A proof mining case study on the unit interval

Abstract: In 1991, Borwein and Borwein [1] proved the following: if $L>0$, $f:[0,1] \to [0,1]$ is $L$-Lipschitz, $(x_n)$, $(t_n) \subseteq [0,1]$ are such that for all $n$, $x_{n+1}=(1-t_n)x_n +t_nf(x_n)$ and there is a $\delta>0$ such that for all $n$, $t_n \leq \frac{2-\delta}{L+1}$, then the sequence $(x_n)$ converges. The relevant fact here is that the main argument used in their proof is of a kind that hasn't been analyzed yet from the point of view of proof mining, and thus it may serve as an illustrative new case study. We shall present our work on the proof [2], showing how to extract a uniform and computable rate of metastability for the above family of sequences.

[1] D. Borwein, J. Borwein, Fixed point iterations for real functions. J. Math. Anal. Appl. 157, no. 1, 112-126, 1991.
[2] A. Sipoș, Rates of metastability for iterations on the unit interval. arXiv:2008.03934 [math.CA], 2020.

Thursday, March 11, 2021

Mihai Prunescu (University of Bucharest)
Exponential Diophantine equations over ${\mathbb Q}$

Abstract: In a previous exposition [1] we have seen that the solvability over ${\mathbb Q}$ is undecidable for systems of exponential Diophantine equations. We now show that the solvability of individual exponential Diophantine equations is also undecidable, and this happens as well for some narrower families of exponential Diophantine equations.

[1] M. Prunescu, The exponential Diophantine problem for ${\mathbb Q}$. The Journal of Symbolic Logic, Volume 85, Issue 2, 671-672, 2020.

Thursday, March 4, 2021

Pedro Pinto (Technische Universität Darmstadt)
Unwinding of proofs

Abstract: The unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question: ``What more do we know if we have proved a theorem by restricted means than if we merely know that it is true?" This research program has since been dubbed proof mining and has been greatly developed during the last two decades and emerged as a new form of applied proof theory [1,2]. Through the use of proof-theoretical tools, the proof mining program is concerned with the unveil of hidden finitary and combinatorial content from proofs that use infinitary noneffective principles. In this talk, we set out to give a brief introduction to the proof mining program, focusing on the following points:

  • functional interpretations in an introductory way;
  • the bounded functional interpretation [3,4];
  • a concrete translation example: the metric projection argument.
We finish with a brief discussion of some recent results [5,6].

[1] U. Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer, 2008.
[2] U. Kohlenbach. Proof-theoretic methods in nonlinear analysis. In M. Viana B. Sirakov, P. Ney de Souza, editor, Proceedings of the International Congress of Mathematicians - Rio de Janeiro 2018, Vol. II: Invited lectures, pages 61-82. World Sci. Publ., 2019
[3] F. Ferreira and P. Oliva. Bounded functional interpretation. Annals of Pure and Applied Logic, 135:73-112, 2005.
[4] F. Ferreira. Injecting uniformities into Peano arithmetic. Annals of Pure and Applied Logic, 157:122-129, 2009.
[5] B. Dinis and P. Pinto. Effective metastability for a method of alternating resolvents. arXiv:2101.12675 [math.FA], 2021.
[6] U. Kohlenbach and P. Pinto. Quantitative translations for viscosity approximation methods in hyperbolic spaces. arXiv:2102.03981 [math.FA], 2021.

Thursday, February 25, 2021

Horațiu Cheval (University of Bucharest)
Formalizing Gödel's System $T$ in Lean

Abstract: In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order arithmetic to that of a quantifier-free system of primitive recursive functionals of higher type. His work has since enabled other advances in proof theory, notably the program of proof mining. We give a brief overview of Gödel's system $T$ and then explore a formalization thereof as a deep embedding in the Lean proof assistant.

[1] mathlib Community, The Lean Mathematical Library, 2019.

Thursday, February 18, 2021

Horațiu Cheval (University of Bucharest)
An introduction to Lean

Abstract: Lean is a proof assistant and programming language developed by Leonardo de Moura at Microsoft Research starting from 2013, based on dependent types and Coquand's Calculus of Inductive Constructions. It offers typical functional programming features, as well as a rich and extensible tactic language for writing proofs. The standard library, mathlib [1], implements an ever-increasing number of definitions and theorems, from basic facts about real numbers to more advanced topics like algebraic geometry or category theory, providing a structured framework for formalizing mathematics. We present an introduction to Lean's theory, methods of writing proofs and then look at how concrete mathematics is done in mathlib.

[1] mathlib Community, The Lean Mathematical Library, 2019.

Thursday, December 17, 2020

Adriana Stancu (University of Bucharest)
Formal verification of SeL4

Abstract: This presentation introduces the SeL4 system, a microkernel first designed in Haskell, whose implementation in C has now a full formal proof of correctness. The focus is on the methods used to abstract the C code implementation into Isabelle/HOL theorems: syntactic translation, memory model and some abstraction levels added to refine the system representation, this involves usage of additional tools like a C-to-Isabelle parser and AutoCorres that will be shortly described.

[1] G. Heiser, The seL4 Microkernel. An introduction. White paper, The seL4 Foundation, 2020.

Adriana Stancu (University of Bucharest)
AutoCorres tutorial

Abstract: AutoCorres is a tool for abstracting C code into Isabelle/HOL (Isabelle's specialization in Higher Order Logic). This presentation will introduce some basic proof rules used in most of the Isabelle's theorems that will be needed to follow some introductory exercises of using AutoCorres tool with sample C programs. The study cases cover the following topics: proving correctness of programs with loops and proving statements about programs that manipulate heap memory.

[1] D. Greenaway, Automated proof-producing abstraction of C code, PhD Thesis, University of New South Wales, Sidney, 2014.

Thursday, December 3, 2020

Andrei Sipoș (University of Bucharest / IMAR)
A quantitative multi-parameter mean ergodic theorem

Abstract: In [1], Avigad, Gerhardy and Towsner proof-theoretically analyzed the classical textbook proof due to Riesz of the mean ergodic theorem for Hilbert spaces in order to extract uniform rates of metastability. In [2], Kohlenbach and Leuștean extracted rates from a simplified argument of Garrett Birkhoff that applies to uniformly convex Banach spaces. What we do here [3] is to analyze another proof of Riesz which was inspired by Birkhoff's one and which delineates more clearly the role played by uniform convexity. The corresponding argument has the advantage that it can be used to prove a more general mean ergodic theorem for a finite family of commuting linear contracting operators.

[1] J. Avigad, P. Gerhardy, H. Towsner, Local stability of ergodic averages. Trans. Amer. Math. Soc. 362, no. 1, 261-288, 2010.
[2] U. Kohlenbach, L. Leuștean, A quantitative mean ergodic theorem for uniformly convex Banach spaces. Ergodic Theory Dynam. Systems 29, 1907-1915, 2009.
[3] A. Sipoș, A quantitative multi-parameter mean ergodic theorem, arXiv:2008.03932 [math.DS], 2020.

Thursday, November 5, 2020

Andrei Sipoș (University of Bucharest / IMAR)
What proof mining is about

Abstract: Proof mining is an applied subfield of mathematical logic that aims to analyze proofs in mainstream mathematics using tools from proof theory. This area has been largely developed in the last couple of decades by the school of Ulrich Kohlenbach (see e.g. his monograph [1]). Here, I attempt to gently introduce the field to the working logician, by adapting my recent articles on The Proof Theory Blog [2,3].

[1] U. Kohlenbach, Applied proof theory: Proof interpretations and their use in mathematics, Springer Monographs in Mathematics, Springer, 2008.
[2] A. Sipoș, What proof mining is about, Part I, The Proof Theory Blog, 2020.
[3] A. Sipoș, What proof mining is about, Part II: Structures and metatheorems, The Proof Theory Blog, 2020.

    Past Seminars