Logic Seminar

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).

• 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