The logic seminar features talks on mathematical logic, philosophical logic and logical aspects of computer science.

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.

To receive announcements about the seminar, please send an email to logic_seminar@fmi.unibuc.ro.

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.

References:

[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

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.

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.

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.

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.

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.

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.

References:

[1] A. Sipoş,
On extracting variable Herbrand disjunctions,
arXiv:2111.12133 [math.LO] (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.

- LOS/IMAR Logic Seminar in 2020-2021
- FMI/IMAR Logic Seminar in 2019-2020
- FMI/IMAR Logic Seminar in 2018-2019
- FMI/IMAR Logic Seminar in 2017-2018
- FMI/IMAR Logic Seminar in 2016-2017
- FMI/IMAR Logic Seminar in 2015-2016
- FMI/IMAR Logic Seminar in 2014-2015
- IMAR Logic Seminar in 2013-2014
- IMAR Logic Seminar in 2012-2013
- FMI Logic in Computer Science Seminar in 2014
- FMI Logic in Computer Science Seminar in 2013