### Thursday, March 22, 2018

**Traian Şerbănuță (University of Bucharest)
Foundations for Natural Proofs and Quantifier Instantiation**

**Abstract**: In this talk we present results from [1], explaining the efficacy of heuristics used for dealing with quantified formulas and recursive definitions.

References:

[1] C. Löding, P. Madhusudan, L. Peña, Foundations for Natural Proofs and Quantifier Instantiation, Proceedings of the ACM on Programming Languages (POPL), Vol. 2, Article 10, 2018.

### Thursday, March 15, 2018

**Adriana Stancu (University of Bucharest)
Dynamic logic of hybrid systems**

**Abstract**: In this talk we present differential dynamic logic, a first-order modal logic that reasons about the behavior of hybrid systems, introduced by André Platzer [1,2,3].

References:

[1] A. Platzer, Logics of Dynamical Systems, ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 13-24.

[2] A. Platzer, Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 426 pages, 2010.

[3] A. Platzer, Differential Dynamic Logic for Hybrid Systems, Journal of Automated Reasoning 41 (2008), 143-189.

### Friday, March 2, 2018, 12:00

** Radu Iosif (CNRS - VERIMAG, France)
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic**

**Abstract**: This paper investigates the satisfiability problem for Separation Logic, with unrestricted nesting of separating conjunctions and implications, for prenex formulae with quantifier prefix in the language $\exists^*\forall^*$, in the cases where the universe of possible locations is either countably infinite or finite. In analogy with first-order logic with uninterpreted predicates and equality, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SLk)]. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SLk) and we define two non-trivial subsets thereof, that are decidable for finite and infinite satisfiability, respectively, by controlling the occurrences of universally quantified variables within the scope of separating implications, as well as the polarity of the occurrences of the latter. The decidability results are obtained by a controlled elimination of separating connectives, described as (i) an effective translation of a prenex form Separation Logic formula into a combination of a small number of \emph{test formulae}, using only first-order connectives, followed by (ii) a translation of the latter into an equisatisfiable first-order formula.

Joint work with Mnacho Echenim and Nicolas Peltier.

### Thursday, February 22, 2018

**Natalia Moangă (University of Bucharest)
Many-sorted polyadic modal logic**

**Abstract**: We present our first results towards defining a many-sorted polyadic modal logic. While the standard modal logic has only two unary operators (box and diamond), its polyadic extension is endowed with a family of modal operators of arbitrary arities, satisfying some appropriate identities. On top of this we can define our many-sorted version, the many-sorted modal poyladic logic, the main difference being that the formulas (within the syntax) and the worlds (within the semantics) are sorted sets. We will present how those changes affect the syntax and the semantics, thus giving us the possibility to develop a new logic.

### Thursday, February 8, 2018

**Mircea Dumitru (University of Bucharest)
Modal logic as higher-order logic III**

### Thursday, January 18, 2018

**Mihai Prunescu (University of Bucharest and IMAR)
First order interpretations in groups, rings and algebras II**

### Thursday, January 11, 2018

**Mircea Dumitru (University of Bucharest)
Modal logic as higher-order logic II**

### Thursday, December 14, 2017

**Mihai Prunescu (University of Bucharest and IMAR)
First order interpretations in groups, rings and algebras**

**Abstract**: We present some results of Malcev. In a first part a general method of transforming rings in metabelian groups is recalled. In the second part we concentrate on finite dimensional algebras over arbitrary fields and we head to the theory of all finite groups.

### Thursday, December 7, 2017

**Mircea Dumitru (University of Bucharest)
Modal logic as higher-order logic**

**Abstract**: Propositional modal logic is usually viewed as a generalization and extension of propositional classical logic. The main argument of this paper is that a good case can be made that modal logic should be construed as a restricted form of second order classical logic. The paper examines one aspect of this second order connection having to do with an incompleteness phenomenon. The leading concept is that modal incompleteness is to be explained in terms of the incompleteness of standard second order logic, since modal language is basically a second order language.

### Thursday, November 23, 2017

**Marian Calborean (University of Bucharest)
Fuzzy and more. Modelling philosophical theories of vagueness on a computer**

**Abstract**: The debate on vagueness has been greatly enriched by the development of fuzzy logic and its applications, many of which are computer-based. However, since such philosophical theories of vagueness as epistemicism and super-valuationism diverge from the basic assumptions of pluri-valuationism embedded in fuzzy logic and since, inside fuzzy theory, philosophically-potent disagreements exist, e.g. in relation to the interpretation of logical connectives, we plan to develop a tool for comparing theories of vagueness, each of which receive a basic tri-partite characterization by accepted truth values, truth-functionality of connectives and valid inference rules. Starting from a dictionary of vague sentences and using recursion, the tool can derive a large number of propositions with their associated truth interpretations under each theory of vagueness. The tool is to be written in common Structured Query Language (MariaDB) with a C-like application language (PHP).

### Thursday, November 16, 2017

**Ioana Leuștean (University of Bucharest)
Łukasiewicz logic and MV-algebras II **

### Thursday, November 9, 2017

**Ioana Leuștean (University of Bucharest)
Łukasiewicz logic and MV-algebras**

**Abstract**: After a brief introduction to Łukasiewicz logic, we focus on some specific topics connecting logic, algebra and probability theory.

### Thursday, November 2, 2017

**Laurențiu Leuștean (University of Bucharest and IMAR)
Proof mining in convex optimization and nonlinear analysis**

**Abstract**: The research program of proof mining in mathematical logic - first suggested by G. Kreisel in the 1950s as 'unwinding of proofs' and developed by U. Kohlenbach in the 1990s and afterwards - is a field of study that aims to analyze, using proof-theoretic tools, the proofs of existing mathematical theorems in order to obtain their hidden quantitative content. The new information is both of quantitative nature, such as algorithms and effective bounds, as well as of qualitative nature, such as uniformities in the bounds. In this talk we give an introduction to proof mining and present some recent applications in convex optimization and nonlinear analysis.