Below you can see all the talks held at the Logic Seminar in the 2022-2023 season. For forthcoming talks, see the main page.
Thursday, June 22, 2023
Marian Călborean (University of Bucharest)
Reasoning by brute force II. Implementing a natural deduction proof calculator for monadic predicate logic with minimal heuristics
Abstract:
One result of the ‘Logic and software’ elective course held at the Faculty of Philosophy, University of Bucharest was the interactive development of a natural deduction calculator that successfully proves 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 allowable rules until the conclusion is derived, then retracing the steps to display the shortest path to it; no backwards reasoning techniques were used. Since computational complexity required speed optimizations, a demonstration of their soundness and completeness is sketched.
Thursday, May 25, 2023
Eugenio Omodeo (DMG, Università degli studi di Trieste)
Does every computably enumerable set admit a univocal Diophantine specification?
For the abstract and references, see this file.
Thursday, May 18, 2023 at 15:00 in Council Hall (joint with the TCS Seminar)
Elena Grigorescu (Purdue University, West Lafayette, IN, USA)
Local Codes for Insertion and Deletion Errors
Abstract:
Locally Decodable Codes (LDCs) are error-correcting codes for which individual message symbols can be quickly recovered despite errors in the codeword. LDCs for Hamming errors have been studied extensively in the past few decades, where a major goal is to understand the amount of redundancy that is necessary and sufficient to decode from large amounts of error.
In this talk I will describe our recent results on LDCs and their variants, when the errors are in the form of insertions and deletions (a.k.a. synchronization errors), rather than classical Hamming errors. Local codes against insertions and deletions are well-motivated by recent progress on DNA storage technologies. I will conclude with several open problems. The talk will be self-contained. (Based on joint work with Alex Block, Jeremiah Blocki, Kuan Cheng, Shubhang Kulkarni, Xin Li, Yu Zheng, Minshen Zhu.)
Thursday, April 27, 2023
Andrei Sipoș (University of Bucharest & IMAR & ILDS)
The computational content of super strongly nonexpansive mappings and uniformly monotone operators
Abstract:
Strongly nonexpansive mappings are a core concept in convex optimization. Recently, they have begun to be studied from a quantitative viewpoint: U. Kohlenbach has identified in [1] the notion of a ‘modulus’ of strong nonexpansiveness, which leads to computational interpretations of the main results involving this class of mappings (e.g. rates of convergence, rates of metastability). This forms part of the greater research program of ‘proof mining’, initiated by G. Kreisel and highly developed by U. Kohlenbach and his collaborators, which aims to apply proof-theoretic tools to extract computational content from ordinary proofs in mainstream mathematics. The quantitative study of strongly nonexpansive mappings has later led to finding rates of asymptotic regularity for the problem of ‘inconsistent feasibility’ [2, 5], where one essential ingredient has been a computational counterpart of the concept of rectangularity, recently identified in [3] as a ‘modulus of uniform rectangularity’.
Last year, Liu, Moursi and Vanderwerff [4] have introduced the class of ‘super strongly nonexpansive mappings’, and have shown that this class is tightly linked to that of uniformly monotone operators. What we do is to provide a modulus of super strong nonexpansiveness, give examples of it in the cases e.g. averaged mappings and contractions for large distances and connect it to the modulus of uniform monotonicity. In the case where the modulus is supercoercive, we give a refined analysis, identifying a second modulus for supercoercivity, specifying the necessary computational connections and generalizing quantitative inconsistent feasibility.
The results in this talk (and additional references) may be found in the paper [6].
References:
[1] U. Kohlenbach, On the quantitative asymptotic behavior of strongly nonexpansive mappings in Banach and geodesic spaces. Israel Journal of Mathematics 216, no. 1, 215–246, 2016.
[2] U. Kohlenbach, A polynomial rate of asymptotic regularity for compositions of projections in Hilbert space. Foundations of Computational Mathematics 19, no. 1, 83–99, 2019.
[3] U. Kohlenbach, N. Pischke, Proof theory and non-smooth analysis. Philosophical Transactions of the Royal Society A 381, Issue 2248, 20220015 [21 pp.], 2023.
[4] L. Liu, W. M. Moursi, J. Vanderwerff, Strongly nonexpansive mappings revisited: uniform monotonicity and operator splitting. arXiv:2205.09040 [math.OC], 2022.
[5] A. Sipoș, Quantitative inconsistent feasibility for averaged mappings. Optimization Letters 16, no. 6, 1915–1925, 2022.
[6] A. Sipoș, The computational content of super strongly nonexpansive mappings and uniformly monotone operators. arXiv:2303.02768 [math.OC], 2023.
Thursday, April 6, 2023
Denisa Diaconescu (University of Bucharest & Runtime Verification)
VLSM: A General Framework for Reasoning About Faulty Distributed Systems II
Thursday, March 30, 2023
Denisa Diaconescu (University of Bucharest & Runtime Verification)
VLSM: A General Framework for Reasoning About Faulty Distributed Systems
Abstract:
Formally modeling and reasoning about distributed systems with faults is a challenging task [1]. Depending on the system model, an execution of a distributed protocol may be subject to many kinds of faults, from simple recoverable component crashes to Byzantine adversarial actions [4]. Each kind of failure may then require specific actions for evasion or recovery by the affected components.
To address this problem, we recently proposed the theory of Validating Labeled State transition and Message production systems (VLSMs) as a general approach to modeling and verifying distributed protocols executing in the presence of faults [5]. In particular, VLSM executions can be subject to equivocation behavior. Equivocation refers to claiming different beliefs about the state of the protocol to different parts of the system in order to steer the protocol-following components into making inconsistent decisions; messages received from equivocating components seem to be valid messages [3]. For example, if a system tries to come to a consensus about the value of a bit, an equivocating component may claim the bit is 0 to one part of the system, and 1 to the other. Equivocation behavior cannot be produced by a single protocol execution, but only by multiple protocol executions, i.e., an equivocating component behaves as if running multiple copies of the protocol.
Our VLSM-based modeling and verification methodology for distributed protocols follows the correct-by-construction approach for design and development [2]: we define an abstract class of protocols (satisfying some generic abstract properties), prove general results about protocols belonging to the class, and then obtain correct-by-construction protocols by concretely instantiating the abstract components, or, alternatively, prove that concrete protocols satisfy those requirements.
References:
[1] Pedro Fonseca, Kaiyuan Zhang, Xi Wang & Arvind Krishnamurthy (2017): An Empirical Study on the Correctness of Formally Verified Distributed Systems. In: European Conference on Computer Systems, pp. 328–343, doi:10.1145/3064176.3064183.
[2] David Gries (1981): The Science of Programming. Springer, doi:10.1007/978-1-4612-5983-1.
[3] Alexander Jaffe, Thomas Moscibroda & Siddhartha Sen (2012): On the price of equivocation in Byzantine agreement. In: Symposium on Principles of Distributed Computing, pp. 309–318, doi:10.1145/2332432.2332491.
[4] Leslie Lamport, Robert Shostak & Marshall Pease (1982): The Byzantine Generals Problem. ACM Transactions on Programming Languages and Systems 4(3), pp. 382–401, doi:10.1145/357172.357176.
[5] V. Zamfir, M. Calancea, D. Diaconescu, W. Kołowski, B. Moore, K. Palmskog, T. F. Șerbănuță, M. Stay, D. Trufaș, & J. Tušil (2022): Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems. arXiv:2202.12662 [cs.DC].
Thursday, March 16, 2023
Mihai Prunescu (University of Bucharest & IMAR)
Zero-knowledge proofs
Abstract: We introduce the notion of zero-knowledge proof and some of its realizations in graphs and in sigma-protocols. Also, some applications in logic and in other cryptographic protocols are presented.
Thursday, March 9, 2023
Traian Șerbănuță (University of Bucharest & Runtime Verification)
Implementing Program Verification in the 𝕂 Framework
Abstract: In this talk we will briefly introduce 𝕂, a rewriting-based framework for defining programming languages semantics, discuss Reachability Logic, the language-agnostic program verification logic for 𝕂, and give some hints about the current implementation.
Thursday, March 2, 2023
Mircea Dumitru (University of Bucharest & Romanian Academy)
Semantics for Quantified Modal Logics
Abstract: The talk presents several semantics for quantified modal logics: standard semantics, constant domains and possibilist quantifiers, weak necessity and truth-value gaps, semantics for “actually”, Kit Fine on the de re / de dicto distinction, and counterpart theory (David Lewis and Graeme Forbes styles, respectively). I shall also discuss some philosophical issues surrounding the formal semantics for quantified modal logics.
Thursday, February 16, 2023
Ionuț Țuțu (IMAR)
A short guide to implementing theorem provers
Abstract: We briefly venture into the world of experimental theorem proving to see what it takes to bring proof calculi to life, making them readily available for teaching and for further research purposes. In contrast to many mainstream theorem provers such as E, Vampire, Gandalf, Isabelle, or Lean, which are based on some specific logics (or families of logics), the approach we propose here is generic. That is, we separate those aspects of a theorem prover that are language independent (e.g., basic proof management) from aspects that are language dependent, such as the base logical system(s) or the kind of inference rules used in proofs. Our effort is supported by SpeX, a rewrite-based environment that facilitates the development of formal-specification languages and tools.
Thursday, February 2, 2023
Cezar Câmpeanu (University of Prince Edward Island)
Cover Languages — Main Results and Applications
Abstract: The concept of Deterministic Finite Cover Automata (DFCA) was first introduced in 1998 at WIA ’98. Several minimization algorithms have been developed for this type of automata recognizing finite languages. The idea was then extended to include the non-deterministic versions of cover automata. The latest extension includes deterministic automata with do-not-care symbols and multiple entries. It has been proven that most problems related to non-deterministic versions of cover automata are NP-hard. In this talk, we present a survey of results and some recent applications of cover automata.
Thursday, November 24, 2022 (online)
Eugenio Omodeo (DMG, Università degli studi di Trieste)
Julia Robinson, existential definability, and Hilbert’s 10th problem
Abstract: Julia Bowman Robinson put forward in 1952 her notions of existential definability and exponential growth, both regarding relations on natural numbers. She foresaw that one of the new century problems posed by David Hilbert in the year 1900 would be settled by singling out an exponential-growth, existentially definable relation. The problem in question called for an algorithm that would establish, for any given polynomial P with integer coefficients, whether the equation P = 0 has integer solutions or not.
Julia Robinson’s outlook had a decisive influence in the research that led, almost twenty years later, to a proof of the algorithmic unsolvability of Hilbert’s 10th problem. She had designed from the outset a scheme for getting a specification of exponentiation in polynomial terms, out of any alike specification of an exponential-growth relation. In a 1969 paper, she would propose an improved version of her reduction scheme, of which a possible further refinement shines through a 1975 paper that she wrote in collaboration with Yuri V. Matiyasevich.
By retracing the stages of Julia Robinson’s contribution to the existential definition of exponentiation, this seminar does not simply intend to pay homage to an outstanding scientist. From an in-depth revisitation of her studies on Hilbert’s 10th, along with the contributions of Martin Davis and Yuri Matiyasevich, a novel characterization of a key concept in computability might emerge: that of a listable set.
Thursday, November 17, 2022
Marian Călborean (University of Bucharest)
A notational extension of classical first-order logic to deal with vague language
Abstract: Vague language is treated as statistical dispersion, using the interplay of preference relations and monadic predicates. A notational extension of classical first-order logic allows defining a tolerant and a strict predicate for each monadic predicate. Results include the failure of weak non-contradiction and of a weak law of excluded middle, and the validity of weak tolerance principles. The logic proposed is compared to other order-sorted logics.
Thursday, November 10, 2022
Andrea Sgarro (DMG University of Trieste)
Possibility theory and the arithmetic of fuzzy numbers
Abstract: Taking inspiration from the seminal work in probability theory by A. N. Kolmogorov and H. R. Pitt, we intend to lay a sound foundation for fuzzy arithmetic, which is based on possibility theory beside fuzzy logic. A possibilistic interpretation of fuzzy arithmetic has long been known, however without taking it to its full consequences: in this paper we stress the basic role of the two limit-cases of possibilistic interactivity, namely deterministic equality versus non-interactivity, thus getting rid of weak points which have so far enfeebled more traditional approaches to fuzzy arithmetic.
Thursday, November 3, 2022
Bogdan Macovei (University of Bucharest)
Lean-certified Dynamic Epistemic Logic with Actions for Security Protocols
Abstract: We define a complete system of epistemic propositional dynamic logic with actions, that is fully defined and certified with the proof assistant Lean. Within our system, we specify security protocols as sequence of actions and we use epistemic reasoning for analyzing their properties.
Thursday, October 20, 2022
Mihai Prunescu (University of Bucharest & IMAR)
On a theorem of Gallai and related questions
Abstract: A theorem was stated by Tibor Gallai without proof and was later proven by several authors, in particular E. Witt or R. Rado. The theorem says that for every k-coloring of ℤn and every finite subset F⊆ℤn, there exists a homothetic image of F which is monochrome. This fact suggests various ultimately unsolvable sequences of SAT instances.