Below you can see a list of past talks at the Logic Seminar in this season. For forthcoming talks, see the main page.

##### 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?