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 hybrid, both remotely and in the Google Hall of the Faculty of Mathematics and Computer Science, University of Bucharest.

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.

Claudia Chiriță (LOS)

A short story on logics with typed modalities

Abstract: We introduce a family of modal logics aimed at modeling discrete evolutionary systems.
These are extensions of ordinary equational and relational logics with typed modalities.
Unlike the classical notion of modality, typed modalities have the advantage of keeping track
of changes of system configurations. We employ inner types to capture triggers of changes and
outer types to capture outcomes. As an example, we model the biological process of membrane
budding. We discuss some implementation details and glance at connections with the theory of bigraphs.

Ştefan Ciobâcă (Alexandru Ioan Cuza University of Iaşi)

Verifying the Conversion into CNF in Dafny

Abstract: We present two computer-verified implementations of the CNF conversion for propositional logic.
The two implementations are fully verified: functional correctness and termination is machine-checked
using the Dafny language for both. The first approach is based on repeatedly applying a set of
equivalences and is often presented in logic textbooks. The second approach is based on Tseitin’s
transformation and is more efficient. We present the main ideas behind our formalization and we
discuss the main difficulties in verifying the two algorithms.

References:

[1] V. Iordache, Ş Ciobâcă,
Verifying the Conversion into CNF in Dafny, in: A. Silva, R. Wassermann, R. de Queiroz (eds),
Logic, Language, Information, and Computation, WoLLIC 2021. LNCS 13038, Springer, 150-166 (2021)

Pedro Pinto (TU Darmstadt)

Halpern and Mann iterative schemas: A path towards generalization

Abstract: In this talk I shall discuss recent joint work with Bruno Dinis, where we considered an
iterative schema which alternates between Halpern and Krasnoselskii-Mann style iterations. We prove,
under suitable conditions, the strong convergence of this algorithm in the general nonlinear setting
of CAT(0) spaces. Besides obtaining quantitative information, we will see how such a proof was
made possible by techniques and ideas from the proof mining program. Our results generalize recent
work by Boț, Csetnek and Meier, and Cheval and Leuştean.

References:

[1] B. Dinis and P. Pinto, Strong convergence for the alternating Halpern-Mann iteration in CAT(0)
spaces. arXiv:2112.14525 [math.FA], 2021.

[2] R. I. Boț, E. R. Csetnek, and D. Meier, Inducing strong convergence into the asymptotic behaviour
of proximal splitting algorithms in Hilbert spaces. Optim. Methods Softw., 34(3):489-514, 2019.

[3] H. Cheval, L. Leuștean, Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration.
arXiv:2107.07176 [math.OC], 2021.

[4] F. Ferreira, L. Leuştean, P. Pinto, On the removal of weak compactness arguments in proof mining.
Advances in Mathematics, 354:106728, 2019.

[5] U. Kohlenbach, L. Leuştean, Effective metastability of Halpern iterates in CAT(0) spaces.
Advances in Mathematics, 231(5):2526-2556, 2012.

Mircea Dumitru (University of Bucharest and Romanian Academy)

Modal frame incompleteness. An account through second 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 makes use of the embedding of modal logic in second order logic and henceforth it
goes on examining 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 as a kind of
exemplification of standard order incompleteness. More- over the modal incompleteness phenomenon
is essentially rooted in the weaker expressive power of the language of sentential modal logic
as compared to the stronger expressive power of the language of second order logic.

References:

[1] M. Dumitru, Modal frame incompleteness. An account through second order logic, in M. Fitting (ed),
Selected Topics from Contemporary Logics, Landscapes în Logic 2, College Publications, London, pp. 183-202, 2021.

Bogdan Dumitru (University of Bucharest)

Notes on abundant elements in union-closed sets

Abstract: In this presentation we explore an elementary problem, posed by Peter Frankel in 1979, a problem that is still open.
The main attraction of the problem resides in its simple formulation: any finite union-closed family of sets ${\mathcal A}$ has an element
that is contained in at least half of the member-sets. A family ${\mathcal A}$ of sets is union-closed if for every two member-sets
$A_1$, $A_2$ from ${\mathcal A}$, the union is also contained in ${\mathcal A}$.

This a special seminar dedicated to presentations of students' research projects.

Maria-Cristina Borza (University of Bucharest)

Theoretical developments on many-sorted modal logic

Abstract: This presentation aims to introduce many-sorted generalizations of bisimulations.
We prove that the disjoint unions, generated submodels and bounded morphisms are all special
cases of bisimulation, we show that bisimilarity implies modal equivalence, and examine a
special case in which the converse is valid. We also introduce the generalization for finite
models and we prove the analogue of Filtration Theorem.

and

Alexandru-Mihai Weng (University of Bucharest)

Lean4 implementation of Weakly Extensional Heyting Arithmetic

Abstract: In this talk we will start by discussing about the main ideas introduced in the Lean4
theorem prover, that helps us to formalize various subjects commonly approached in mathematics.
Further, in a pragmatic way, we will briefly illustrate some use cases of this proof assistant
that will strengthen the ideas discussed previously. Finally, as a base for future integration of
proof mining techniques in Lean4, we will present our implementation of the logical system use
in proof mining, weakly extensional Heyting arithmetic in all finite types, and show some difference
between its definitions and actual implementation of them.

Antonio Di Nola (Università degli Studi di Salerno)

Łukasiewicz Logic and Neural Networks

Abstract: We show that a particular class of multilayer perceptrons, which describes possibly
non-linear phenomena is linked with Łukasiewicz logic. We will describe how we
can name a neural network with a formula and, viceversa, how we can associate a class of
neural networks to each formula. Moreover, we introduce the definition of Łukasiewicz Equivalent
Neural Networks to stress the strong connection between different neural networks via Łukasiewicz
logical objects. More in general, we can say that starting from a syntax, plus a logic, plus
Universal Algebra we get:

(•) a symbolic representation of classes of neural networks

(•) a pillar of a bridge between a logical calculus and Neural Networks.

This seems to be a paradigm that can be used in many different ways.

Gabriel Istrate
(West University of Timișoara)

Towards Game-Theoretic Models of Moral and Other-Regarding Agents

Abstract: In the first part of the talk I will discuss the need for
the development of a logic-based specification formalism for
decision-theoretic and game-theoretic concepts, ultimately resulting
in a software library for decision and game theory. I will outline
some requirements for such a library including

- cognitive plausibility
- expresiveness
- tractability

Paulo Oliva (Queen Mary University of London)

Kripke Semantics for Intuitionistic Łukasiewicz Logic

Abstract: This paper proposes a generalization of the Kripke semantics of intuitionistic
logic $\mathbf{IL}$ appropriate for intuitionistic Łukasiewicz logic $\mathbf{IŁL}$ — a logic in
the intersection between $\mathbf{IL}$ and (classical)
Łukasiewicz logic. This generalised Kripke semantics is based on the poset sum construction,
used in Bova and Montagna (Theoret Comput Sci 410(12):1143–1158, 2009) to show the decidability
(and PSPACE completeness) of the quasiequational theory of commutative, integral and bounded
GBL algebras. The main idea is that $w \Vdash \psi$—which for $\mathbf{IŁL}$ is a relation
between worlds $w$ and formulas $\psi$, and can be seen as a function taking values in
the booleans $(w \Vdash \psi ) \in {{\mathbb {B}}}$—becomes a function taking values in
the unit interval $(w \Vdash \psi ) \in [0,1]$.
An appropriate monotonicity restriction (which we call sloping functions) needs to be put on
such functions in order to ensure soundness and completeness of the semantics.

References:

[1] A. Lewis-Smith, P. Oliva, E. Robinson,
Kripke Semantics for Intuitionistic Łukasiewicz Logic,
Studia Logica 109:313-339, 2019.

Denisa Diaconescu (University of Bucharest)

A Real-Valued Modal Logic

Abstract: Two core families of many-valued modal logics emerge: order-based modal logics, including modal
extensions of Gödel logics, where only the order type of the truth values matters, and continuous
modal logics, such as those based on Łukasiewicz logic where propositional connectives are
interpreted by continuous functions over sets of real numbers. In this talk we focus on continuous many-valued modal logics.

Abelian logic was introduced independently by Meyer and Slaney [1] as a relevant logic, and
Casari [2] as a comparative logic. We show that continuous many-valued modal logic corresponds
to a fragment of a minimal modal extension of Abelian logic K(A) [3,4].

We present a sound and complete labelled tableau calculus for K(A) and obtain a coNEXPTIME
upper bound for checking validity in this logic. For the more manageable modal-multiplicative
fragment of K(A) we give an EXPTIME upper bound for checking validity and establish the completeness
of an analytic sequent calculus and an axiomatisation system that, unlike other such systems for
continuous many-valued modal logic, has only finitary rules.

References:

[1] R. K. Meyer and J. K. Slaney. Abelian logic from A to Z. In Paraconsistent Logic: Essays on the Inconsistent,
245–288. Philosophia Verlag, 1989.

[2] E. Casari. Comparative logics and abelian l-groups. In C. Bonotto, R. Ferro, S. Valentini, and
A. Zanardo, editors, Logic Colloquium ’88, 161–190. Elsevier, 1989.

[3] D. Diaconescu, G. Metcalfe, L. Schnüriger. Axiomatizing a Real-Valued Modal Logic. AiML 2016,
King's College Publications, 236-251, 2016.

[4] D. Diaconescu, G. Metcalfe, L. Schnüriger. A Real-Valued Modal Logic. Logical Methods
in Computer Science 14(1):1-27, 2018.

Adrian Crăciun (West University of Timişoara)

Scheme-Based Algorithm Synthesis by Lazy Thinking (a retrospective)

Abstract: Lazy Thinking is a deductive, scheme-based synthesis method, proposed by Bruno
Buchberger as part of a mathematical theory exploration model and implemented to some extent
in the Theorema system.

Lazy Thinking works as follows: a proof of the correctness of an algorithm (i.e. its specification)
using an algorithm scheme and using complete knowledge about the specification is attempted.
All definitions and properties
of concepts involved in the specifications are known. The proof is likely to fail, as no
information about the unknown subalgorithms is available. Following an analysis of the failing proof,
conjectures are generated and added to the knowledge, such that the failure can be overcome.
These conjectures turn out to be specifications for the unknown subalgorithms. Algorithms that
satisfy the generated specifications can then either be retrieved from the knowledge base, or
synthesized by lazy thinking in subsequent rounds of exploration.

We give some examples of scheme-based theory exploration, including the synthesis of a Groebner
Bases algorithm.
We will also give some remarks on potential developments of the ideas presented here.

Moritz Müller (Universitat de Barcelona)

On the parameterized complexity of $\Delta_0$ truth

Abstract: We consider the problem, given a $\Delta_0$ formula $\varphi(x)$ and a natural
number $n$ in unary, whether $\varphi(n)$ is true. We are interested in instances of the problem
where n is much bigger than $\varphi$. More precisely, we consider the parameterized problem with
parameter $|\varphi|$. We show unconditionally that this problem does not belong to the parameterized
version of $AC^0$. We also show that certain natural {\em upper bounds} on the parameterized complexity
of the problem imply separations of classical complexity classes. These results are obtained by
an analysis of a parameterized halting problem. A related problem concerns the provability
of the MRDP theorem in bounded arithmetic.

Isabela Drămnesc (West University of Timişoara)

Deductive synthesis of sorting algorithms on lists and on binary trees in Theorema

Abstract: This talk presents recent results published in ICTAC'21 and JLAMP'21.
We describe the principles and the implementation of AlCons (Algorithm Constructor), a system
for the automatic proof--based synthesis of sorting algorithms on lists and on binary trees,
in the frame of the Theorema system. The core of the system is a dedicated prover based on
specific inference rules and strategies for constructive proofs over the domains of lists
and of binary trees, aimed at the automatic synthesis of sorting algorithms and their auxiliary
functions from logical specifications. The specific distinctive feature of our approach is
the use of multisets for expressing the fact that two lists (trees) have the same elements.
This allows a more natural expression of the properties related to sorting, compared to the
classical approach using the permutation relation (a list is a permutation of another). Moreover,
the use of multisets leads to special inference rules and strategies which make the proofs
more efficient, as for instance: expand/compress multiset terms and solve meta-variables using
multiset equalities. Additionally, we use a Noetherian induction strategy based on the relation
induced by the strict inclusion of multisets, which facilitates the synthesis of arbitrary recursion
structures, without having to indicate the recursion schemes in advance. The necessary auxiliary
algorithms (like, e.g., for insertion and merging) are generated by the same principles from
the synthesis conjectures that are automatically produced during the main proof, using a ``cascading"
method, which in fact contributes to the automation of theory exploration. The prover is
implemented in the frame of the Theorema system and works in natural style, while the
generated algorithms can be immediately tested in the same system.

Antonio Di Nola (Università degli Studi di Salerno)

Non Archimedean Random Variables and Łukasiewicz Logics

Abstract: First Rota's problem is an informal problem on how reformulate probability without making
appeal to sets of points like the sample space. In particular Rota calls for ``algebras of random variables".
The pointfree approach of Mundici is in terms of "algebras of random variables" in the sense of Nelson.
This means that one uses a category of rings or algebraic structures ($C^*$-algebras in this case) which is
equivalent to the categories of interest.

Indeed, Mundici mentions the possibility of treating probability in MV-algebras with infinitesimals.
Our main aim is to show that such a development is indeed possible and to extend Mundici's results to
non-archimedean random variables. We also will show that algebras of non archimedean random variables are
models of an extension of Łukasiewicz logic.

Florin Crăciun (Babeş-Bolyai University)

Region Types for Region-based Memory Management

Abstract: Region-based memory management is an old idea of heap memory management. In this talk,
we present our results on the use of region type systems to ensure the safe use of regions.
We also discuss our ongoing work on applying regions to the Rust language.

Marian Călborean (University of Bucharest)

Reasoning by brute force. Implementing a natural deduction proof calculator with minimal heuristics

Abstract: One result of the `Logic and software' elective course held in 2022 at the Faculty of Philosophy,
University of Bucharest was the interactive development of a natural deduction calculator that successfully
proves propositional exercises in classical textbooks. The calculator has versions in Python and PHP, both
common programming languages, allowing the easy study and change of the software code corresponding to NK rules.
It also uses brute force - running all allowable rules until the conclusion is adequately derived,
then retracing the steps to display the shortest path to it; no human-like rules-of-thumb or backwards
reasoning were used. Since computational complexity required speed optimizations, a demonstration
of their soundness and completeness is sketched.

Dorel Lucanu (Alexandru Ioan Cuza University of Iași)

An Introduction to Alk and its Logical Foundation

Abstract: Alk is an educational platform designated to help in learning algorithms and
acquiring algorithmic thinking. It can be used for writing, executing, experimenting,
and analyzing algorithms. Alk platform includes Alk Language, an interpreter, debugger,
a symbolic execution engine, and support for algorithm analysis. The platform is used as
support for the course Algorithm Design at FII-UAIC.
In this talk, we give a brief introduction to Alk and its foundations based on
matching logic.

The talk takes place at the Runtime Verification (RV) Bucharest headquarters (Popa Tatu 18).

Amélie Ledein (Inria, Deducteam, LMF)

Dedukti, a standard language for the interoperability of proof systems

Dedukti is a logical framework to encode
various logics to allow interoperability of proofs between different formal tools, like Coq, PVS or Isabelle.
This logical framework is based on $\lambda\Pi$-calculus modulo theory, a $\lambda$-calculus
with dependent types, and extended with rewriting rules.
After a presentation of the $\lambda\Pi$-calculus modulo theory, I will talk about translations
to Dedukti, as well as interoperability challenges.
Finally, I will mention other work done by Deducteam.

Radu Iosif (CNRS - VERIMAG)

On the Expressiveness of a Logic of Separated Relations

Abstract: We compare the model-theoretic expressiveness of the existential fragment of Separation
Logic over unrestricted relational signatures (SLR) with only separating conjunction as
logical connective and higher-order inductive definitions, traditionally known as the symbolic
heap fragment, with (Monadic) Second Order Logic ((M)SO). While SLR and MSO are incomparable on
structures of unbounded treewidth, it turns out that SLR can be embedded in SO, in general,
and that MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by
a parameter given as input. We also discuss the problem of defining a fragment of SLR that
is equivalent to MSO over models of bounded treewidth. Such a fragment would then become
the most general Separation Logic with a decidable entailment problem, a key ingredient of
practical verification methods for self-adapting (reconfigurable) component-based and distributed systems.

Joint work with Florian Zuleger (TU Wien).

Past seminars

- 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