Below you can see all the talks held at the Logic Seminar in the 2023-2024 season. For forthcoming talks, see the main page.

##### Thursday, June 6, 2024

Marian Călborean (University of Bucharest)

Trees, algorithms and logics: A calculator for Priest’s Introduction to Non-classical Logics

**Abstract**:

In the “Logic and software” 2024 course (Faculty of Philosophy, Bucharest), we developed a calculator which generates tableaux proofs for various logics in Graham Priest’s 2008 “Introduction to Non Classical Logic: From if to is”, with the goal of implementing all of Priest’s variations of Beth’s tableaux method in a unified code base. The calculator is open-source, with versions in Kotlin and JavaScript, allowing easy deployment and study. It uses brute force and some optimizations for which a proof of completeness is sketched. The definition of a logic as implemented in the code is also investigated for philosophical and mathematical adequacy. This is joint work with Andrei Dobrescu.

##### Thursday, May 23, 2024

Simina Brânzei (Purdue University)

The sharp power law of local search on expanders

**Abstract**:

Local search is a powerful heuristic in optimization and computer science, the complexity of which was studied in the white box and black box models. In the black box model, we are given a graph *G*=(*V*,*E*) and oracle access to a function *f*:*V*→R. The local search problem is to find a vertex *v* that is a local minimum, i.e. with *f*(*v*)≤*f*(*u*) for all (*u*,*v*)∈*E*, using as few queries as possible. The query complexity is well understood on the grid and the hypercube, but much less is known beyond.

We show the query complexity of local search on *d*-regular expanders with constant degree is Ω(*n^(1/2)*/log*n*), where *n* is the number of vertices. This matches within a logarithmic factor the upper bound of *O*(*n^(1/2)*) for constant degree graphs from Aldous [2], implying that steepest descent with a warm start is an essentially optimal algorithm for expanders. The best lower bound known from prior work was Ω(*n^(1/8)*/log*n*), shown by Santha and Szegedy [3] for quantum and randomized algorithms.

We obtain this result by considering a broader framework of graph features such as vertex congestion and separation number. We show that for each graph, the randomized query complexity of local search is Ω(*n^(1.5)*/*g*), where *g* is the vertex congestion of the graph; and Ω(*(s/Δ)^(1/4)*), where *s* is the separation number and Δ is the maximum degree. For separation number the previous bound was Ω(*(s/Δ)^(1/8)*/log*n*), given by Santha and Szegedy [3] for quantum and randomized algorithms.

We also show a variant of the relational adversary method from Aaronson [4], which is asymptotically at least as strong as the version in Aaronson [4] for all randomized algorithms and strictly stronger for some problems.

These results may be found in the paper [1], joint work with Davin Choo and Nicholas Recker.

**References**:

[1] S. Brânzei, D. Choo, N. Recker, The Sharp Power Law of Local Search on Expanders. arXiv:2305.08269 [cs.CC], 2023.

[2] D. Aldous, Minimization algorithms and random walk on the *d*-cube. *The Annals of Probability*, 11(2):403–413, 1983.

[3] M. Santha, M. Szegedy, Quantum and classical query complexities of local search are polynomially related. In *Proceedings of the thirty-sixth annual ACM symposium on Theory of computing*, pp. 494–501, 2004.

[4] S. Aaronson, Lower bounds for local search by quantum arguments. *SIAM J. Comput.* 35(4), 804–824, 2006.

##### Thursday, May 16, 2024

Mihai Prunescu (University of Bucharest and IMAR)

On recurrent sequences of integers

**Abstract**:

There is a method to ultimately express recurrent sequences of integers by arithmetic terms. This is joint work with Lorenzo Sauras-Altuzarra.

**References**:

[1] M. Prunescu, L. Sauras-Altuzarra, On the representation of C-recursive integer sequences by arithmetic terms. arXiv:2405.04083 [math.LO], 2024.

##### Thursday, April 18, 2024

Mihai Prunescu (University of Bucharest and IMAR)

On representability by arithmetic terms

**Abstract**:

Consider number-theoretic functions like \(\tau\), which represents the number of divisors of a natural number, \(\sigma\), which yields the sum of its divisors, or Euler’s totient function \(\varphi\), which computes, for any \(n\), the number of residues modulo \(n\), which are relatively prime to \(n\). There are methods to compute these functions for a given argument \(n\) from the prime number decomposition of \(n\), but it is difficult to imagine arithmetic closed terms in \(n\) alone, computing them. Yet, those functions are Kalmár-elementary and by the results of Mazzanti and Marchenkov, such terms do exist. As well, closed arithmetic terms represent the \(n\)th prime and various other number-theoretical functions. I will show how such terms can be effectively constructed. Work in progress.

##### Thursday, April 4, 2024

Horațiu Cheval (University of Bucharest)

Partial (co)recursive functions in Coq and Lean

**Abstract**:

We present a novel method, based on domain theory, for defining partial recursive functions in interactive theorem provers like Coq and Lean, which would normally reject such definitions, as they require the termination of all functions. Our approach further extends to a representation of coinductive types and partial corecursive functions on them, which enhances the expressiveness of both systems. While Coq does contain built-in corecursion, it does not accept functions like *mirror *on infinitely deep trees, due to it violating the so-called guardedness condition, or *filter *on streams, as it is not total. Both of these can be defined in the presented encoding. Furthermore, Lean lacks entirely a native notion of coinductives, therefore the domain-theoretical representation can be used to build them from scratch in it. This is joint work with David Nowak and Vlad Rusu.

##### Thursday, March 28, 2024

Gabriel Istrate (University of Bucharest)

Equilibria in multiagent online problems with predictions

**Abstract**:

We study the power of (competitive) algorithms with predictions in a multiagent setting. To this extent we introduce a multiagent version of the ski-rental problem. In this problem agents can collaborate by pooling resources to get a group licence for some asset. If the licence price is not met agents have to rent the asset individually for the day at a unit price. Otherwise the licence becomes available for everyone in perpetuity at no extra cost. Our main contribution is a best-response analysis of a single-agent competitive algorithm that assumes perfect knowledge of other agents’ actions (but no knowledge of its own renting time). We then give an analysis of the setting when agents have a predictor for their own active time, yielding a tradeoff between robustness and consistency. We investigate the effect of using such a predictor in an equilibrium, as well as the new equilibria formed in this way. This is joint work with Cosmin Bonchiș and Victor Bogdan (West University of Timișoara).

##### Thursday, March 21, 2024

Natalia Ozunu (University of Bucharest)

Modal logic for program specification

**Abstract**:

We developed a many-sorted hybrid polyadic modal logic, which allows us to define both the syntax of a programming language and its evaluation context. Consequently, in the syntactic layer of our system, we represent a programming language and its operational semantics such that a program execution is represented as a deductive sequence of formulas having appropriate sorts. Our goals were to define an expressive and flexible system based on a classically developed many-sorted modal logic, such that one can perform both program execution and verification. We started with a generalization of the already existing approaches on many-sorted modal logic, and we continued with various forms of hybridization. At each stage we proved completeness theorems, we analyzed the theoretical properties of our logics, and we provided relevant examples.

##### Thursday, March 14, 2024

Ionuț Țuțu (IMAR)

An institution-theoretic approach to bisimilarity

**Abstract**:

Bisimulation relations play a crucial role in both process algebra and modal logic, highlighting the close connection between the two areas of science. In the former, they witness the behavioural equivalence of processes, whereas in the latter, they lead to important characterizations of modal expressivity. In this talk, we briefly revisit labelled transition systems, bisimulation relations, and their connections with process algebra and modal logic, looking for general patterns that apply to a variety of calculi and logics. We present stratified institutions, introduce an institution-theoretic notion of bisimulation, and sketch a few Hennessy-Milner results relating bisimilarity to elementary equivalence.

##### Thursday, March 7, 2024

Nicoleta Dumitru (University of Bucharest)

(Post-)Quantum Cryptography II

##### Thursday, February 29, 2024 at 14:30

Mircea Dumitru (University of Bucharest & Romanian Academy)

A Free Logic for Fictionalism II

##### Thursday, February 22, 2024

Nicoleta Dumitru (University of Bucharest)

(Post-)Quantum Cryptography

**Abstract**:

In this talk, we are going to discuss two areas of cryptography in full development, namely quantum and post-quantum cryptography. The main purpose is to clearly explain the algorithms that are the basis of the threat to the security of communication as we know it now, as well as those that can be used as substitutes for the widely used cryptosystems. Another purpose of this talk is to draw attention to the fact that modern cryptography is under the light of a high threat from the quantum universe if a computer that obeys the principles of quantum mechanics becomes truly functional.

##### Thursday, February 8, 2024

Marian Călborean (University of Bucharest)

The logic of gradable adjectives: a layered supervaluationism and parametrized degree-theory II

##### Thursday, January 25, 2024

Marian Călborean (University of Bucharest)

The logic of gradable adjectives: a layered supervaluationism and parametrized degree-theory

**Abstract**:

The adjective ‘Heavy’ is unidimensional, since it depends only on weight, while ‘clever’ is multidimensional, depending on various factors. The logic of unidimensional comparatives has been studied extensively, in two traditions: the delination approach started by Hans Kamp and Sally McConnell-Ginet and the degree-theoretical approach championed by Chris Kennedy. To add multidimensionality to the former, I propose and study a layered supervaluationism based on a hierarchy of relations by arity. For the latter, I use \((m,n)\)-Ferrers properties (Öztürk 2008, Carpentiere, Giarlotta and Watson 2018) to weaken transitivity and define an aggregation function over dimensions.

##### Thursday, January 11, 2024

Alexandru Oltean (University of Bucharest)

Formalizing Hybrid Modal Logic in Lean

**Abstract**:

Following a paper by Blackburn and Tzakova (1998), I formalized a variant of hybrid modal logic in Lean 4, together with a proof of soundness and a (work-in-progress, but close-to-finished) proof of completeness. I will focus on the practical challenges that this effort entailed and my proposed solutions; for example, regarding some properties of infinite sets to which I could devise no immediate Lean counterpart.

The code is available here. The implementation is more closely explained in my B.Sc. thesis, available here.

##### Thursday, December 14, 2023

Mircea Dumitru (University of Bucharest & Romanian Academy)

A Free Logic for Fictionalism

**Abstract**:

In *Reference without Referents*, Mark Sainsbury aims to provide an account of reference that honors the common-sense view that sentences containing empty names like “Vulcan” and “Santa Claus” are entirely intelligible, and that many such sentences — “Vulcan doesn’t exist”, “Many children believe that Santa Claus will give them presents at Christmas”, etc.— are literally true. Sainsbury’s account endorses the Davidsonian program in the theory of meaning and combines this with a commitment to Negative Free Logic, which holds that all simple sentences containing empty names are false. In this paper, I pose several problems for this account. In particular, I question the ability of Negative Free Logic to make appropriate sense of the truth of familiar sentences containing empty names, including negative existential claims like “Vulcan doesn’t exist”.

##### Thursday, December 7, 2023

Bogdan Dumitru (University of Bucharest & BitDefender)

Using SAT Solvers to Investigate the Erdős–Szekeres Conjecture for \(e(7)=33\) (slides)

**Abstract**:

Define \(e(n)\) as the smallest number such that, for any \(n\), any set of at least \(e(n)\) points in general position in the plane contains \(n\) points that are the vertices of a convex polygon. The Erdős–Szekeres conjecture states that, for any \(n \geq 3\), \(e(n) = 2^{n-2} + 1\). In this talk, we will present a reduction of the problem to Boolean Satisfiability and use a SAT solver to partially verify that \(e(7) = 33\).

##### Thursday, November 23, 2023 (online)

Antonio Piccolomini d’Aragona (University of Siena & Université d’Aix-Marseille)

Inversion results and base-completeness for two approaches to proof-theoretic validity (slides)

**Abstract**:

The name “proof-theoretic semantics” (PTS) indicates a family of constructive semantics where meaning and validity are explained in terms of the notion of proof. The meaning of the non-logical vocabulary is fixed through sets of rules governing deduction at the atomic level, called “atomic bases”.

PTS stems from Prawitz’s normalisation theorems for Gentzen’s Natural Deduction. In the original formulation, due to Prawitz himself, proofs are conceived of in terms of inferential structures equipped with reduction functions for removing maximal steps of generalised elimination rules. I shall indicate this variant with the expression “reducibility semantics”. In a more recent approach, inferential structures are left aside, and PTS is understood as a theory of consequence for formulas over atomic bases. This variant of PTS is nowadays referred to as “base(-extension)-semantics”.

Both reducibility semantics and base-semantics are expected to be semantics for intuitionistic, or at least constructive logics, and many completeness or incompleteness results for these logics have been obtained so far.

In my talk, I prove some general results on the relation between reducibility semantics and base-semantics which, when suitable conditions are met, permit one to shift from one approach to the other. From these results I then draw some consequences, relative to the issue of completeness of (recursive) logical systems. This will finally lead me to focus on a notion of base-completeness, which, to conclude, I discuss with reference to known (in)completeness results for intuitionistic logic.

##### Thursday, November 9, 2023

Traian Șerbănuță (University of Bucharest & Runtime Verification & ILDS)

Yet another formalization of matching logic in Coq

**Abstract**:

This talk will describe an exercise in formalizing and verifying, with the help of the proof assistant Coq, Laurențiu Leuștean’s notes on matching logic [1], including the syntax, the proof system, models, satisfaction, and soundness, as well as some elements of set theory (including Tarski and Kleene’s fixed point theorems as specialized for sets).

**References**:

[1] L. Leuștean, Notes on applicative matching logic, 2022.

##### Thursday, November 2, 2023

Mihai Prunescu (University of Bucharest and IMAR)

Using Z3 to Verify Inferences in Fragments of Linear Logic

**Abstract**:

Linear logic is a substructural logic proposed as a refinement of classical and intuitionistic logics, with applications in programming languages, game semantics, and quantum physics. We present a template for Gentzen-style linear logic sequents that supports verification of logic inference rules using automatic theorem proving. Specifically, we use the Z3 Theorem Prover to check targeted inference rules based on a set of inference rules that are presumed to be valid. To demonstrate the approach, we apply it to validate several derived inference rules for two different fragments of linear logic: \(\mathsf{MLL+Mix}\) (Multiplicative Linear Logic extended with a Mix rule) and \(\mathsf{MILL}\) (Multiplicative Intuitionistic Linear Logic).

##### Thursday, October 26, 2023

Gabriel Istrate (University of Bucharest)

Conway’s Army Percolation

**Abstract**:

I am studying a probabilistic model inspired by the Conway’s Army game. In the classical version of this game, the lower half-plane of an infinite chessboard is filled with queens. A classical result by John Conway (1961) shows that it is impossible to move (in a finite number of steps) a piece to the fifth line.

Motivated by an analogy to percolation theory in mathematical physics, I am studying the situation where every square of the lower half-plane contains, independently with the same probability \(p \in [0,1]\), a piece (the classical case occurs when \(p=1\)). I’m aiming to obtain estimates for the following quantities: the probability of moving a piece to a specific square on line \(k\) (where \(k \leq 4\)); the maximum density of pieces that can be moved to squares on line \(k\) (again, where \(k \leq 4\)).

In this talk, based on work in progress, I shall present both rigorous results (based on probabilistic techniques) and experimental results (based on SAT solving and integer linear programming), providing estimates for the aforementioned quantities. One interesting aspect is that the method of proving impossibility in the classical case yields poor estimates in general. On the other hand, I have identified certain mathematical objects related to the generalized Riemann zeta functions, which I will use as pagoda functions. These objects yield better estimates.

I will briefly discuss transfinite, ordinal-based extensions.

##### Thursday, October 19, 2023

Horațiu Cheval (University of Bucharest)

Matching Logic in Lean

**Abstract**:

Matching Logic is a small and expressive system aimed at program verification, constituting the theoretical underpinning of the 𝕂 framework. We present a Lean formalization of the applicative version of Matching Logic (AML), with definitions for the proof system and semantics, together with proofs of some metatheoretical results, like the deduction and soundness theorems. We also present a work-in-progress mechanism for automatically translating AML proofs from our Lean formalization to an existing encoding of AML in the Metamath proof checker. Two different methods are presented, one at the object level, and one based on metaprogramming. The implementations are available here and here.

##### Thursday, September 28, 2023 (joint with the Monthly FMI Conference)

Cristian Calude (University of Auckland)

Quantum Randomness

**Abstract**:

Random digits are used hundreds of billions of times a day to encrypt data in electronic networks. From where do they come? Die rolls? Computer programs? The digits of pi? Beam splitters? Are these numbers equally random? Are quantum random bits truly/perfect random? How can we know whether a string of digits is random? How good are quantum random number generators? Have these questions been selected at random?