# IMAR/FMI 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 12:00 in Hall 220,
Faculty of Mathematics and Computer Science,
University of Bucharest.
to the mailing list,

our group

## Talks in 2014-2015

### Friday, June 19, 2015

Adriana Bălan (Polytehnica University of Bucharest)
Coalgebraic logic over (po)sets

Abstract: Positive modal logic, as introduced by Dunn in the 90s, is the negation-free fragment of the basic modal logic K. Replacing the models (Kripke frames) by coalgebras for an arbitrary (weak-pullback preserving) functor on the category of sets yields the positive fragment of coalgebraic logic, as developed in joint work with A. Kurz and J. Velebil.

Reference:
A. Bălan, A. Kurz, J. Velebil, Positive fragments of coalgebraic logics, to appear in Log. Meth. Comput. Sci. CALCO2013 Special Issue, arXiv:1402.5922 [math.CT].

### Friday, June 12, 2015

Andrei Sipoș (IMAR & FMI)
Ultraproducts and metastability II

### Friday, June 5, 2015

Andrei Sipoș (IMAR & FMI)
Ultraproducts and metastability I

Abstract: We formulate the problem of finding uniform rates of metastability and we illustrate how J. Avigad and J. Iovino showed that ultraproducts of metric spaces can provide us non-constructive existence proofs. We illustrate the method with several applications.

Reference:
J. Avigad, J. Iovino, Ultraproducts and metastability, New York Journal of Mathematics 19 (2013), 713-727.

### Friday, May 29, 2015

Andrei Sipoș (IMAR & FMI)
Ellerman's generalized ultraproducts II

### Friday, May 22, 2015 10:00 in Hall 202

Matei Popovici (University Politehnica of Bucharest)
Truely perfect recall and commitment in Alternating-Time Temporal Logics

Abstract: Multiagent systems are a paradigm for modeling interactions between heterogeneous software components or between software and humans. Verifying properties of such interactions is critical for deploying systems which rely on them. Alternating-Time Temporal Logic (short ATL) offers a promising solution. ATL extends Temporal Logics with a coalition modal operator < A > f, which expresses that coalition A has a strategy to enforce f. ATL also comes with tussle: selecting the "right" semantics. Several options are possible, by making different assumptions on the abilities of agents: perfect/imperfect memory (or recall) and perfect/imperfect information. However, there are situations when these semantics are problematic: we show that agents with perfect recall & imperfect information may still forget when proceeding to satisfy a sub-goal. Also, they may relent their strategies, in a similar situations. We propose an ATL-semantics which addresses the "forgetting" and "commitment" issues. We study the expressive power, validities and model-checking, for our proposed semantics.

### Friday, May 15, 2015

Andrei Sipoș (IMAR & FMI)
Ellerman's generalized ultraproducts I

Abstract: We show how Ellerman's work can streamline some classical results involving Kripke structures and/or ultraproducts by using sheaf-based first-order model theory.

Reference:
D. P. Ellerman, Sheaves of structures and generalized ultraproducts, Annals of Mathematical Logic 7 (1974), 163-195.

### Friday, April 24, 2015

Mihai Prunescu (IMAR)
A group of Thompson and one of its effects in model theory

Abstract: We introduce Thompson's group V and we construct a formal statement true in all finite groups but not in all groups.

### Friday, April 17, 2015

Andrei Sipoș (IMAR & FMI)
Forcing in Model Theory II

Abstract: We show how finite forcing in conjunction with infinitary logic can be used to derive omitting types results. Then we develop the parallel theory of infinite forcing, emphasizing the differences in the classes of structures created.

### Friday, April 3, 2015

Andrei Sipoș (IMAR & FMI)
Forcing in Model Theory I: Finite Forcing

Abstract: We illustrate Robinson's almost direct translation into model theory of Cohen's forcing method from set theory and how it can be used in conjunction with well-behaved fragments of infinitary logic to yield an almost purely syntactical theory of types and their realization and omitting and to determine the widest available generalizations of model completion and existential completion, concepts which in addition serve as a strong motivation for developing the forcing terminology.

### Friday, March 27, 2015

Alexandru Dragomir (University of Bucharest)
Edgington's Verificationist Thesis and Fitch's Paradox in an Epistemic-Temporal Framework

Abstract: (1) I will begin by offering a short introduction to Epistemic Logic and presenting the Verificationist Thesis and Fitch's paradox in an epistemic-modal logic. Then, I will proceed to presenting three Epistemic Temporal logical frameworks created by Hoshi (2009): TPAL (Temporal Public Announcement Logic), TAPAL (Temporal Arbitrary Public Announcement Logic) and TPAL+P! (Temporal Public Announcement Logic with Past Operators).
(2) Edgington (1985) offered an interpretation of the Verificationist Thesis that blocks Fitch's paradox and I will propose a way to formulate it in a TAPAL-based language. The language I will use is a combination of TAPAL and TPAL+P! with an Indefinite Past Operator (TAPAL+P!+P). Using indexed satisfiability relations (as introduced in (Wang 2010; 2011)) I will offer a prospective semantics for this language. I will investigate whether the tentative reformulation of Edgington's Verificationist Thesis in TAPAL+P!+P is free from paradox and adequate to Edgington's ideas on how the Verificationist Thesis should be interpreted.

Reference:
D. Edgington, The Paradox of Knowability, Mind 94 (1985), 557-568.
T. Hoshi, Epistemic dynamics and protocol information, PhD Thesis, Stanford University, ILLC Dissertation Series DS-200X-NN, 2009.
Y. Wang, Epistemic Modelling and Protocol Dynamics, PhD Thesis, University of Amsterdam, ILLC Dissertation Series DS-2010-06, 2010.
Y. Wang, Reasoning about protocol change and knowledge, in ICLA'11 Proceedings of the 4th Indian conference on Logic and its applications, 2011, Springer, 189-203.

### Friday, March 20, 2015

Gabriel Istrate (West University of Timisoara and the e-Austria Research Institute)
Partition into heapable sequences, heap tableaux and a multiset extension of Hammersley's process

Abstract: We investigate partitioning of integer sequences into heapable subsequences (previously defined and established by Mitzenmacher et al.). We show that an extension of patience sorting computes the decomposition into a minimal number of heapable subsequences (MHS). We connect this parameter to an interactive particle system, a multiset extension of Hammersley's process, and investigate its expected value on a random permutation. In contrast with the (well studied) case of the longest increasing subsequence, we bring experimental evidence (with some theoretical justifications as well) that the correct asymptotic scaling is $(1+\sqrt{5})/2\cdot \ln(n)$. Finally we give a heap-based extension of Young tableaux, prove a hook inequality and an extension of the Robinson-Schensted correspondence to such heap tableaux.

Reference:
Gabriel Istrate, Cosmin Bonchiș, Partition into heapable sequences, heap tableaux and a multiset extension of Hammersley's process, 2015.

### Friday, March 6, 2015

Radu Iosif (CNRS - VERIMAG, France)
Decidable Horn Systems with Difference Constraints

Abstract: This paper tackles the problem of the existence of solutions for recursive systems of Horn clauses with second-order variables interpreted as sets of integers, and harnessed by a simple first-order theory of integers, such as difference bounds arithmetic. We start by the definition of a simple class of Horn systems with one second-order variable and one recursive rule, for which we prove the decidability of the problem "does the system has a solution ?". The proof relies on a construction of a tree automaton recognizing all cycles in the weighted graph corresponding to every unfolding tree of the Horn system. We constrain the tree to recognize only cycles of negative weight by adding a Presburger formula that harnesses the number of times each rule is fired, and reduce our problem to the universality of a Presburger-constrained tree automaton. We studied the complexity of this problem and found it to be in 2EXPTIME with a EXPTIME-hard lower bound. In the second part, we drop the univariate restriction and consider multivariate second-order Horn systems with a structural restriction, called flatness. Finally, we show the decidability of this class of systems, within the same complexity bounds.

Reference:
Radu Iosif, Decidable Horn Systems with Difference Constraints, arXiv:1503.00258 [cs.FL], 2015.

### Friday, February 27, 2015

Andrei Sipoș (IMAR & FMI)
Proving Morley's Theorem III

Abstract: I will wrap up Morley's proof and then move on to the Baldwin-Lachlan characterization of uncountably categorical theories in terms of Vaughtian pairs.

### Friday, February 20, 2015

Andrei Sipoș (IMAR & FMI)
Proving Morley's Theorem II

Abstract: This part will finish the exposition of Morley's original proof, focusing on tools such as indiscernibles, saturation or relatively prime models.

### Friday, February 13, 2015

Andrei Sipoș (IMAR & FMI)
Proving Morley's Theorem I

Abstract: By proving the old conjecture of Łoś stating that a theory having exactly one model in one uncountable cardinality has this property in every uncountable cardinality, Morley inaugurated a new phase of model theory research. We shall explore his methods, along with several alternative proofs and extensions to other logics, if time permits.

### Friday, December 19, 2014

Claudia Chiriță (Royal Holloway, University of London)
Dealing with preferences: on constraint algebras and graded satisfaction

Abstract: We describe a general technique for enriching algebraic specifications with soft constraints meant to enable the formal description of preferences, magnitude of satisfaction and best solution (with respect to a set of preferences). This allows us to quantify the compatibility of two specifications, and thus provides a possible procedure for the selection of the most promising provider of a given resource in the context of service discovery and binding. The construction that we propose relies on the approach to soft constraints specific to valued constraint satisfaction problems (VCSP) and on the institution-independent theory of algebraic specifications.

and Denisa Diaconescu (FMI and University of Bern)
Mutually exclusive nuances of truth in Moisil logic

Abstract: Nuances of truth provide an alternative and robust way to reason about vague information: a many-valued object is determined by some Boolean objects, its nuances. However, a many-valued object cannot be recovered only from its Boolean nuances. This idea is mathematically expressed by a categorical adjunction between Boolean algebras and Lukasiewicz-Moisil algebras.
Moisil's determination principle plays a central role in the study of Lukasiewicz-Moisil algebras and Moisil logic. Since in the original approach, the determination principle fails for subalgebras, we explore a more expressible notion of nuances, namely mutually exclusive nuances of truth, which among others, save the determination principle for subalgebras.

### Friday, December 12, 2014

Gheorghe Stefanescu (FMI)
Self-assembling interactive modules: a research programme

Abstract: We propose a research programme for getting structural characterisations for 2-dimensional languages generated by self-assembling tiles. This is part of a larger programme on getting a formal foundation of parallel, interactive, distributed systems.

Reference:
Gheorghe Stefanescu, Self-assembling interactive modules: a research programme, 2014.

### Friday, December 5, 2014

Radu Iosif (CNRS - VERIMAG, France)
Abstraction Refinement for Trace Inclusion of Data Automata

Abstract: A data automaton is a finite automaton equipped with variables (counters) ranging over a multi-sorted data domain. The transitions of the automaton are controlled by first-order formulae, encoding guards and updates. We observe, in addition to the finite alphabet of actions, the values taken by the counters along a run of the automaton, and consider the data languages recognized by these automata. The problem addressed in this paper is the inclusion between the data languages recognized by such automata. Since the problem is undecidable, we give an abstraction-refinement semi-algorithm, proved to be sound and complete, but whose termination is not guaranteed. The novel feature of our technique is checking for inclusion, without attempting to complement one of the automata, i.e. working in the spirit of antichain-based non-deterministic inclusion checking for finite automata. The method described here has various applications, ranging from logics of unbounded data structures, such as arrays or heaps, to the verification of real-time systems.

Reference:
Radu Iosif, Adam Rogalewicz, Tomas Vojnar, Abstraction Refinement for Trace Inclusion of Data Automata, arXiv:1410.5056 [cs.LO].

### Friday, November 28, 2014

Andrei Sipoș (IMAR & FMI)
Categorial Interpretations III

### Friday, November 21, 2014

Andrei Sipoș (IMAR & FMI)
Categorial Interpretations II

Abstract: We move forwards to the intepretation of logic in categories.

### Friday, November 14, 2014

Andrei Sipoș (IMAR & FMI)
Categorial Interpretations I

Abstract: The classical theory of models corresponding to (fragments of) first-order logic can be generalized in order to show deeper connections between different theories. As a prerequisite, we first depict the suitable categories which, in the process, replace the ordinary category of sets, namely various flavours of toposes.

### Friday, October 31, 2014

Radu Iosif (CNRS - VERIMAG, France)
Deciding Entailments in Inductive Separation Logic with Tree Automata

Abstract: Separation Logic (SL) with inductive definitions is a natural formalism for specifying complex recursive data structures, used in compositional verification of programs manipulating such structures. The key ingredient of any automated verification procedure based on SL is the decidability of the entailment problem. In this work, we reduce the entailment problem for a non-trivial subset of SL describing trees (and beyond) to the language inclusion of tree automata (TA). Our reduction provides tight complexity bounds for the problem and shows that entailment in our fragment is EXPTIME-complete. For practical purposes, we leverage from recent advances in automata theory, such as inclusion checking for non-deterministic TA avoiding explicit determinization. We implemented our method and present promising preliminary experimental results.

Reference:
Radu Iosif, Adam Rogalewicz, Tomas Vojnar, Deciding Entailments in Inductive Separation Logic with Tree Automata, arXiv:1402.2127 [cs.LO].