Logic Seminar

Organizers: Laurențiu Leuștean, Denisa Diaconescu, 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.
To be added
to the mailing list,
please subscribe to

our group
Past Seminars

    Our logo and our posters are designed by Claudia Chiriță.

Talks in 2018-2019

Thursday, June 27, 2019

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.

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

Thursday, June 13, 2019


Thursday, May 30, 2019

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

Abstract: Dynamic epistemic logics are useful in reasoning about knowledge and certain acts of learning (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: one based on [1], and the second on [2].

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

Thursday, May 16, 2019

Ionuţ Ţuţu (Royal Holloway University of London & IMAR)
An introduction to hybrid-dynamic first-order logic

Abstract: We propose a hybrid-dynamic first-order logic as a formal foundation for specifying and reasoning about reconfigurable systems. As the name suggests, the formalism we develop extends (many-sorted) first-order logic with features that are common to hybrid and to dynamic logics. This provides certain key advantages for dealing with reconfiguration, such as: (a) a signature of nominals, including operation and relation symbols, that allows references to specific possible worlds / system configurations – as in the case of hybrid logics; (b) distinguished signatures of rigid and flexible symbols, where the rigid symbols are interpreted uniformly across possible worlds – this supports a rigid form of quantification, which ensures that variables have the same interpretation regardless of the possible world where they are evaluated; (c) hybrid terms, which increase the expressive power of the logic in the context of rigid symbols; and (d) modal operators over dynamic-logic actions, which are defined as regular expressions over binary nominal relations. In this context, we advance a notion of hybrid-dynamic Horn clause and develop a series of results that lead to an initial-semantics theorem for the Horn-clause fragment of hybrid-dynamic first-order logic.

Thursday, April 10, 2019

Mihai Prunescu (University of Bucharest)
Around Hilbert's Tenth Problem

Abstract: We discuss different implications of the negative answer of Hilbert's Tenth Problem: the exponential diophantine equation over ${\mathbb N}$ and ${\mathbb Q}$, the minimal number of variables which lead to an undecidable problem over ${\mathbb Z}$, the homogenous diophantine problem over ${\mathbb Z}$.

Thursday, March 28, 2019

Mihai Prunescu (University of Bucharest)
Lindström's Theorems II

Thursday, March 14, 2019

Mihai Prunescu (University of Bucharest)
Lindström's Theorems

Abstract: Regular logic systems which are strictly stronger than the first order predicate calculus cannot satisfy in the same time Löwenheim-Skolem for statements and compacity (Lindström 1). Effectively presented such systems cannot satisfy in the same time Löwenheim-Skolem for statements and the condition that the set of generally valid sentences is recursively enumerable (Lindström 2). We sketch the proof that uses partial isomorphisms.

[1] H.-D. Ebbinghaus, J. Flum, W. Thomas, Mathematical Logic. Second edition, Undergraduate Texts in Mathematics, Springer, 1996.

Thursday, February 28, 2019

Natalia Moangă (University of Bucharest)
The hybridization of many-sorted polyadic modal logic

Abstract: Hybrid logics are obtained by enriching modal logics with nominals and state variables, that directly refer the individual points in a Kripke model. In the present work we develop a hybrid version on top of our many-sorted polyadic logic, previously defined. Our system has nominals and state variables on each sort, as well as binders that act like the universal and the existential quantfiers on state variables. In doing this, we follow various approaches for hybrid modal logic, especially the work of Blackburn and Tsakova.

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), 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, January 31, 2019 at 10:00 in Hall 214

Cătălin Dima (Université Paris-Est Créteil)
The frontier between decidability and undecidability for logics for strategic reasoning in the presence of imperfect information

Abstract: The last 15-20 years have seen a number of logical formalisms that focus on strategic reasoning. These logics aim at giving specification languages for various multi-agent game structures, in which agents have adversarial or cooperative objectives which may be qualitative or quantitative and may have various types of imperfect information. The presence of imperfect information raises a particular difficulty in that many games cannot be solved algorithmically, as well as their corresponding logical formalisms. In this tutorial I will review some techniques for proving that the Alternating-time Temporal Logic has an undecidable model-checking problem, but this problem becomes decidable when considering memoryless strategies, coalitions with distributed knowledge, hierarchical knowledge and public or coalition-public announcements. I will also give a short introduction to the model-checking tool MCMAS which relies on the memoryless semantics for ATL with imperfect information, and the problems that arise when implementing the model-checking algorithms for this case.

Thursday, December 20, 2018

Andrei Sipoș (TU Darmstadt & IMAR)
The finitary content of sunny nonexpansive retractions

Abstract: The goal of proof mining is to extract quantitative information out of proofs in mainstream mathematics which are not necessarily fully constructive. Often, such proofs make use of strong mathematical principles, but a preliminary analysis may show that they are not actually needed, so the proof may be carried out in a system of strength corresponding roughly to first-order arithmetic. Following a number of significant advances in this vein by Kohlenbach in 2011 and by Kohlenbach and Leuștean in 2012, we now tackle a long-standing open question: the quantitative analysis of the strong convergence of resolvents in classes of Banach spaces more general than Hilbert spaces.
This result was proven for the class of uniformly smooth Banach spaces by Reich in 1980. What we do is to analyze a proof given in 1990 by Morales, showing that adding the hypothesis of the space being uniformly convex, and thus still covering the case of $L^p$ spaces, can serve to eliminate the strongest principles used in the proof by way of a modulus of convexity for the squared norm of such spaces. A further procedure of arithmetization brings the proof down to System $T$ so the proper analysis may proceed. After obtaining a non-effective realizer of the metastability statement, this is majorized in order to obtain the desired rate. Subsequent considerations calibrate this bound to $T_1$. It particular, this result completes some analyses that had previously been obtained only partially, yielding rates of metastability within the above-considered class of Banach spaces for the Halpern and Bruck iterations.
These results are joint work with Ulrich Kohlenbach.

[1] U. Kohlenbach, A. Sipoș, The finitary content of sunny nonexpansive retractions, arXiv:1812.04940 [math.FA], 2018.

Thursday, December 6, 2018

Roberto Giuntini (University of Cagliari)
Classical and quantum degrees of truth: a new look at the effects of a Hilbert space

Abstract: We investigate certain Brouwer-Zadeh lattices that serve as abstract counterparts of lattices of effects in Hilbert spaces under the spectral ordering. These algebras, called $PBZ^*$-lattices, can also be seen as generalisations of orthomodular lattices and are remarkable for the collapse of three notions of “sharpness” that are distinct in general Brouwer-Zadeh lattices. We investigate the structure theory of $PBZ^*$-lattices and their reducts; in particular, we prove some embedding results for $PBZ^*$-lattices and provide an initial description of the lattice of $PBZ^*$-varieties.

    Past Seminars