Title: Elementary closed forms for non-trivial divisors

Abstract:

Some arithmetic terms t have the property that, for every composite natural number n, the value t(n) is a proper non-trivial divisor of n. This is joint work with Joseph M. Shunia.

Bibliography:

[1] Mihai Prunescu, Joseph M. Shunia, Elementary closed-forms for non-trivial divisors. arXiv:2510.26939 [math.NT], 2025.

The talk will take place physically at FMI (the new PBTower location), Hall 203.

The post Logic Seminar talk: Elementary closed forms for non-trivial divisors first appeared on Institute for Logic and Data Science.

Title: 𝕂 definitions as Matching Logic theories

Abstract:

The 𝕂 Framework is a rewriting-based tool for specifying programming language semantics and carrying out formal verification based on the semantics given.

PL definitions are translated by 𝕂 into Matching Logic (ML) theories, encoded in an intermediate language named Kore, through a complex compilation process which is not formally documented and has to be considered as part of the trusted codebase.

In this talk, we describe a formal mechanism for obtaining the denotational semantics of 𝕂 definitions directly as ML theories.

While for many components of 𝕂, the ML denotation we give is similar to the current Kore output, abstract rewrite rules, which allow one to specify rewrite rules by mentioning only the fragments of the program configuration that are being modified and are one of 𝕂’s most important features, lack at the moment an elegant ML denotation.

In the current implementation of 𝕂, they are compiled through a mechanism of configuration concretization which converts them into top rewrite rules between full configurations. Based on a newly developed ML theory of contexts, we propose a solution through which we can uniformly axiomatize such abstract rules in a way that reflects their local nature and does not rely on a concretization algorithm.

This is joint work with Xiaohong Chen, Dorel Lucanu and Grigore Roșu.

The talk will take place physically at FMI (the new PBTower location), Hall 203.

The post Logic Seminar talk: 𝕂 definitions as Matching Logic theories first appeared on Institute for Logic and Data Science.

Title: What we cannot say: An agent-relative, syntactic account of ignorance in epistemic logic

Abstract:

A theory of ignorance should distinguish uncertainty – lack of information and unawareness – lack of conception. As a new way to model incomplete epistemic descriptions, this paper introduces split languages, where each agent at each world reasons in a sublanguage that omits propositions and modalities for which there is no fact of the matter from that agent’s point of view. Standard Kripke frames extended with a map from agents and worlds to languages validate a language-relative notion of consequence and block inexpressible formulas at the syntax level. This yields transparent analyses of classical puzzles such as Ignorance, Mutual Knowledge, Muddy Children, and a coin underspecification puzzle, without assuming common knowledge of a fully specified model. In contrast to standard awareness logics, which stipulate an unstructured set of formulas an agent is aware of, the present proposal generates this set from a primitive vocabulary. This constraint provides a more principled account of unawareness, leading to a transparent, guarded proof system and a natural model of conceptual change. Thus, key meta-theoretic properties include conservativity over S5, soundness and completeness of the guarded proof system, and persistence under language growth. Finally, I introduce a dynamic operator for concept introduction and provide reduction principles.

The talk will take place physically at FMI (the new PBTower location), Hall 102.

The post Logic Seminar talk: What we cannot say first appeared on Institute for Logic and Data Science.

Title: Forcing, Transition Algebras, and Calculi

Abstract:

We introduce a logic of transition algebras that enhances many-sorted first-order logic with features commonly found in dynamic logics. This brings a significantly higher degree of expressivity, allowing us to axiomatize properties such as finiteness or reachability. We discuss syntactic entailment, study basic properties such as compactness and completeness, and show that the latter does not hold under standard finitary proof rules. Consequently, we define proof rules having both finite and countably infinite premises, and we provide conditions under which completeness can be proved. To wrap up, we further develop the forcing method introduced in model theory by Abraham Robinson and we demonstrate its use in order to obtain a completeness result for signatures that are at most countable. This is joint work with Go Hashimoto and Daniel Găină.

The talk will take place physically at FMI (the new PBTower location), Hall 102.

The post Logic Seminar talk: Forcing, Transition Algebras, and Calculi first appeared on Institute for Logic and Data Science.

Title: Alignment as Ontology: Why AI’s Worldview Matters More Than Its Goals

Abstract:

Traditional approaches to AI alignment, often framed as problems of control, overlook a fundamental truth: all behavior arises from an agent’s internal worldview.
Intelligence is not a neutral substrate awaiting instructions, it is a way of interpreting reality. Every action expresses the underlying logic through which an agent makes sense of information. An incoherent or impoverished worldview cannot yield stable alignment, no matter the goals imposed upon it.
This talk introduces the Informational Buildup Framework (IBF) as a possible ontological model for cultivating coherent intelligence. IBF describes reality as a field of information where patterns stabilize through resonance, accumulate into structure via directional buildup, and express intelligence as the local drive toward greater coherence.
As a framework of logic, IBF redefines truth as coherence across contexts and reasoning as the preservation and extension of that coherence. Under this view, an AI is aligned when its internal informational dynamics mirror and reinforce the coherence of the world it inhabits. Alignment thus becomes an emergent property of understanding, not an after-the-fact layer of control.
The session will explore IBF’s foundations, its formalization path, and its implications for designing intrinsically coherent intelligence.

The talk will take place physically at FMI (the new PBTower location), Hall 203.

The post Logic Seminar talk: Alignment as Ontology, Why AI’s Worldview Matters first appeared on Institute for Logic and Data Science.

VERY IMPORTANT! The talk will take place physically at the PBTower building (the new location of FMI-UNIBUC), Hall 415.

Title: Regular Grammars for Sets of Graphs of Tree-Width 2

Abstract:

Regular word grammars are restricted context-free grammars that define all the recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier “regular” is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulae without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width. Joint work with Marius Bozga (VERIMAG) and Florian Zuleger (TU Wien) presented at LICS 2025.

The post Logic Seminar talk: Regular Grammars for Sets of Graphs of Tree-Width 2 first appeared on Institute for Logic and Data Science.

Title: Exploring Baaz’s generalization method and its geometric insights

Abstract:

In 1999, Baaz introduced a novel approach to proof mining and, as a case study, examined a particular case of factorization of Fermat numbers. Around twenty years later, by again applying this strategy to different inputs, a geometric description of these factors was reached, along with a conjecture concerning lattice points. After discussing this question at various conferences, several partial answers and new related problems were obtained, in connection with the theories of unimodular matrices and generalized Pillai equations. In this presentation, I will elucidate Baaz’s technique and showcase the aforementioned results.

The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.

The post Logic Seminar talk: Exploring Baaz’s generalization method and its geometric insights first appeared on Institute for Logic and Data Science.

Title: The minimal ontology of time – a unified axiomatization

Abstract:

How minimal can ontology be and still accommodate the main logical and metaphysical stances about time? I present a first-order set-theoretic framework, no stronger than ZFC, in which (i) the underlying axioms are pairwise independent; (ii) the canonical positions in temporal metaphysics, from presentism and the growing-block (cf. Prior 1967; Cameron 2015) to eternalism (Sider 2001) and Fine’s fragmentalism (Fine 2005), become parameter settings; (iii) standard well-behaved tense, metric, or interval logics (Prior’s PF, MTL, ITL) receive a sound and complete semantics via a representation theorem. On grounds of explanatory reach and parsimony, the growing-block emerges as the least problematic ontology of time within this minimal framework.

The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.

The post Logic Seminar talk: The minimal ontology of time first appeared on Institute for Logic and Data Science.

Title: Doing and observing in (large) sequence models. A discussion of auto-suggestive delusions

Abstract:

In recent artificial intelligence (AI) literature, so-called hallucinations or delusions—instances where generative models produce false or unfounded outputs—have raised legitimate concerns about the trustworthiness and applicability of AI systems in real-world contexts. While much of the literature frames these delusions as surface-level failures of content fidelity, a more profound explanation lies in the structural underpinnings of these models—specifically, in the presence of confounding variables and their treatment under causal inference frameworks like Judea Pearl’s do-calculus.

A compelling causal account of such delusions, particularly those termed auto-suggestive delusions, was developed recently by Ortega et al. [1] in the context of (large) sequence models, which are embedded in a great number of current generative AI models (including the GPT class of language models). According to this account, auto-suggestive delusions arise not merely from data scarcity or exposure bias but from a deeper conflation in the model of observations (ground-truth data) and actions (model-generated data) during inference. This misidentification introduces delusions whereby the model interprets its own outputs as evidence about the world—a self-reinforcing effect that systematically distorts its representation of reality.

This leads to broader philosophical implications. If a model recursively treats its own outputs as valid observations, it may gradually drift into a self-referential epistemic loop—where it no longer requires, nor aligns with, external validation. Such a model isn’t merely biased; rather, it might be said it reasons according to an internal causal model that’s just cut off from the world, albeit coherent.

This presentation proceeds in four parts. First, I will review exposure bias and its limitations in explaining AI models’ delusions. Second, following Ortega et al. [1] I will introduce Pearl’s causal inference framework that reveals how confounding operates in (large) sequence models. Third, I will examine the nature of auto-suggestive delusions through the lens of causal inference. Finally, I will argue that these findings suggest that (large) sequence models and the AI models implementing them, under certain conditions, evolve toward solipsistic behavior—a state in which they create internally coherent but externally ungrounded representations of the world.

References:

[1] P. A. Ortega et al., Shaking the foundations: delusions in sequence models for interaction and control. arXiv:2110.10819 [cs.LG], 2021.

The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.

The post Logic Seminar talk: Doing and observing in (large) sequence models first appeared on Institute for Logic and Data Science.

Title: A Language-Theoretic Approach to the Heapability of Signed Permutations

Abstract:

We investigate a signed version of the Hammersley process, a discrete process on words related to a property of integer sequences called heapability [1]. The specific version that we investigate corresponds to a version of this property for signed sequences. We give a characterization of the words that can appear in the signed Hammersley process. In particular we show that the language of such words is the intersection of two one-counter languages.
The results in this talk (and additional references) may be found in the paper [2].

References:

[1] J. Byers, B. Heeringa, M. Mitzenmacher, G. Zervas, Heapable sequences and subseqeuences. In: Proceedings of the Eighth Workshop on Analytic Algorithmics and Combinatorics (ANALCO 2011), SIAM Press, 2011, pp. 33–44.
[2] G. Istrate, A Language-Theoretic Approach to the Heapability of Signed Permutations. Prague Stringology Conference 2024, pp. 71–85.

The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.

The post Logic Seminar talk: A Language-Theoretic Approach to the Heapability of Signed Permutations first appeared on Institute for Logic and Data Science.