# Logic Seminar

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

The logic seminar features talks on
mathematical logic,
philosophical logic and
logical aspects of computer science.
All seminars, except where otherwise indicated,
will be at 10:00 in Hall 202,
Faculty of Mathematics and Computer Science,
University of Bucharest.

## Talks in 2019-2020

### Thursday, February 27, 2020 in Google Hall 214

Ulrich Kohlenbach (Technische Universität Darmstadt)
A quantitative analysis of the ''Lion-Man" game

Abstract: We analyze, based on an interplay between ideas and techniques from logic and geometric analysis, a pursuit-evasion game. More precisely, we focus on a discrete lion and man game with an $\varepsilon$-capture criterion. We prove that in uniformly convex bounded domains the lion always wins and, using ideas stemming from proof mining, we extract a uniform rate of convergence for the successive distances between the lion and the man. As a byproduct of our analysis, we study the relation among different convexity properties in the setting of geodesic spaces.
Joint work with Genaro López-Acedo and Adriana Nicolae.

### Thursday, December 19, 2019

Marian Călborean (University of Bucharest)
First-order logic and vagueness

References:
[1] P. Cobreros, P. Egré, D. Ripley, R, Van Rooij, Tolerant, Classical, Strict, Journal of Philosophical Logic 41 (2019), 347-385.
[2] D. Graff, Shifting Sands: An Interest-Relative Theory of Vagueness, Philosophical Topics 28 (2000), 45-81.
[3] U. Keller, Some remarks on the definability of transitive closure in first-order logic and Datalog, Internal report, Digital Enterprise Research Institute (DERI), University of Innsbruck, 2004.
[4] K.G. Lucey, he ancestral relation without classes, Notre Dame Journal of Formal Logic 20 (1979), 281-284.

### Thursday, December 12, 2019

Ioana Leuștean (University of Bucharest)
Operational Semantics of Security Protocols II

### Thursday, November 21, 2019

Ioana Leuștean (University of Bucharest)
Operational Semantics of Security Protocols

Abstract: After a brief overview of the formal methods used for analysing security protocols, we will focus on the operational semantics developped in [1].

References:
[1] C. Cremers, S. Mauw, Operational Semantics and Verification of Security Protocols, Springer, 2012.

### Monday, November 4, 2019 at 09.00

Andrei Sipoș (TU Darmstadt & IMAR)
Bounds on strong unicity for Chebyshev approximation with bounded coefficients

Abstract: In the early 1990s, Kohlenbach pursued a program of applying proof-theoretic techniques in order to obtain effective results in best approximation theory, specifically moduli of uniqueness and constants of strong unicity. This was part of a larger research program of Kreisel from the 1950s called ‘unwinding of proofs’, a program that aimed at applying proof transformations to potentially non-constructive proofs in ordinary mathematics in order to extract new information. The program was later developed by Kohlenbach and his students and collaborators under the name of ‘proof mining’, extending it to a variety of mathematical areas.
What we do is to build upon the work mentioned above in order to obtain a modulus of uniqueness for best uniform approximation with bounded coefficients, as first considered by Roulier and Taylor. The main novelty is the application of Schur polynomials to obtain useful explicit formulas for the interpolation results which are needed in the proof. We present ways these formulas may be bounded and how those bounds may in turn be used to derive and verify the desired modulus.

References:
[1] A. Sipoș, Bounds on strong unicity for Chebyshev approximation with bounded coefficients, arXiv:1904.10284 [math.CA], 2019.

### Thursday, October 24, 2019

Alexandru Dragomir (University of Bucharest)
An introduction to BAN logic (a logic of authentication)

Abstract: One of the first and most discussed logical approaches to the problem of verifying security protocols is the one proposed in BAN logic (Burrows, Abadi \& Needham 1989). BAN logic is a many-sorted modal logic used for its intuitive and compelling set of inference rules devised for reasoning about an agent’s beliefs, trust and message exchange. My presentation will focus on (1) presenting the language and inference rules of BAN logic, (2) following the original paper's analysis of the Otway-Rees protocol, (3) presenting some objections to using BAN, and (4) discussing the problem of offering a semantics of BAN logic.

### Thursday, September 19, 2019 in Hall 214

Radu Iosif (CNRS - VERIMAG, France) )
Checking Deadlock Freedom of Component-based Systems

Abstract: We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology (i.e. architecture) of the system (e.g. pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. We applied our technique to the verification of several textbook examples, such as dining philosophers, mutual exclusion protocols and concurrent systems with preemption and priorities.
Joint work with Marius Bozga and Joseph Sifakis.