The logic seminar is a joint LOS-IMAR seminar.
Organizers: Laurențiu Leuștean and 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 Thursdays between 10:00 and 11.50. The seminars are online.

Thursday, October 21, 2021

Mihai Prunescu (University of Bucharest and IMAR)
On Representations of Intended Structures in Foundational Theories

Abstract: Often philosophers, logicians, and mathematicians employ a notion of intended structure when talking about a branch of mathematics. In addition, we know that there are foundational mathematical theories that can find representatives for the objects of informal mathematics. In this paper, we examine how faithfully foundational theories can represent intended structures, and show that this question is closely linked to the decidability of the theory of the intended structure. Joint work with Neil Barton and Moritz Muller.
[1] N. Barton, M. Müller, M. Prunescu, On Representations of Intended Structures in Foundational Theories. Journal of Philosophical Logic (2021).
DOI: 10.1007/s10992-021-09628-2

Thursday, October 28, 2021

Bogdan Macovei (LOS)
DELP: Dynamic Epistemic Logic for Security Protocols

Abstract: The formal analysis of security protocols is a challenging field, with various approaches being studied nowadays. The famous Burrows-Abadi-Needham Logic was the first logical system aiming to validate security protocols. Combining ideas from previous approaches, in this paper we define a complete system of dynamic epistemic logic for modeling security protocols. Our logic is implemented, and few of its properties are verifyied, using the theorem prover Lean.

Thursday, November 11, 2021

Ionuţ Ţuţu (IMAR)
A Rewriting-based Toolset for Specification Processing

Abstract: We explore some of the features that promote term rewriting and, in particular, Maude as a meta-language for working with logical systems, and showcase a set of rewriting-based tools that support the syntactic analysis and processing of formal specifications. Along the way, we discuss basic aspects related to the development of interpreters of specification languages, including user-interface design, parsing specifications, and executing commands. All this is done in a logic-agnostic manner, meaning that the techniques we describe apply to a wide variety of logical formalisms. To illustrate the approach, we introduce SpeX, a general platform for working with formal specifications, and demonstrate the steps required for integrating new logical formalisms within SpeX.

Thursday, November 18, 2021, 10:30

Andrei Popescu (University of Sheffield)
Inductive and Coinductive Reasoning with Isabelle/HOL

Abstract: I will describe basic and advanced mechanisms for inductive and coinductive reasoning available in the interactive theorem prover Isabelle/HOL. They cover inductive and coinductive predicates founded on Knaster-Tarski fixed points, inductive and coinductive datatypes, structural recursion and corecursion, corecursion "up-to" and mixed recursion-corecursion. The concepts will be illustrated with examples formalized in Isabelle, but they should be understandable to computer scientists, logicians and mathematicians with no knowledge of Isabelle.

Thursday, November 25, 2021

Traian Şerbănuţă (LOS & Runtime Verification)
Consensus in Distributed Systems. Formalizing Correct by Construction Protocols

Abstract: This presentation will attempt to review the basic definitions andresults concerning the consensus problem for distributed protocols (byzantine faults, safety, liveness), discuss Vlad Zamfir's idea of correct-by-construction protocols and our attempts at formalizing his approach.

Thursday, December 2, 2021

Răzvan Diaconescu (IMAR)
Experimental Mathematics by Rewriting

Abstract: This talk is about how to support mathematical investigation and development through machine performed computational experiments. Its unique character lies in a computational method and its associated programming technique. This is based an extended form of model-theoretic rewriting which includes some powerful features such as non-determinism and rule-based programming. It is also universal in the sense that that it is applicable in principle to a wide variety of mathematical domains. Its solid and transparent mathematical and logical foundations lead to a programming experience that is very close to doing mathematics, which means it is much more suitable for mathematicians than other forms of do-it-yourself programming. The talk will touch directly two aspects of this activity: model-theoretic foundations and case studies.

Thursday, December 9, 2021

Andrei Sipoş (LOS and IMAR)
On extracting variable Herbrand disjunctions

Abstract: Some quantitative results obtained by proof mining take the form of Herbrand disjunctions that may depend on additional parameters. We attempt to elucidate this fact through an extension to first-order arithmetic of the proof of Herbrand's theorem due to Gerhardy and Kohlenbach which uses the functional interpretation.
[1] A. Sipoş, On extracting variable Herbrand disjunctions, arXiv:2111.12133 [math.LO] (2021).

Thursday, December 16, 2021

Bogdan Dumitru (University of Bucharest)
SAT Solvers: Introduction and applications

Abstract: SAT solving theory and practice made dramatic progress in the last decade, to the point where problems with millions of variables and clauses can be solved in a timely manner. We explore the ingredients of modern SAT solvers and study some of their applications.

Past seminars