Below you can see a list of past talks at the Logic Seminar. For forthcoming talks, see the main page.
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.