ABSTRACT. This work extends Brzozowski derivatives of regular expressions to alphabets equipped with similarity-based symbol matching. It proves that fuzzy derivatives preserve regularity, induce finitely many states over finite alphabets, correspond semantically to language derivatives, and can be simulated by ordinary derivative automata over a quotient alphabet. The theorems are formalized in Rocq.

ABSTRACT. Graph protection problems have emerged as an important area in combinatorics and theoretical computer science, especially in the study of dynamic and online models [1]. The eternal graph framework captures situations where a solution must be maintained indefinitely under continuous adversarial actions. The classical vertex cover problem is well-studied; however, its eternal variants introduce new challenges due to the need for adaptability. In the Eternal Relaxed Vertex Cover (ERVC) problem, the defender is allowed to locally modify the solution by exchanging vertices in response to edge attacks. A set F is an eternal relaxed vertex cover (ERVC) if for every sequence of edges (e_i) there exists a sequence of vertex sets (F_i) such that: F_1 = F, for each i >= 1, F_{i+1} = (F_i \ {v_i}) U {u_i} where u_i is incident to e_i, and v_i is in F_i intersect N[u_i]. The minimum size of such a set is called the eternal relaxed vertex covering number, denoted by \tau_r^\infty(G). While eternal domination and related protection problems have been extensively studied [2], the ERVC problem remains largely unexplored on structured graph classes. In this work, we study ERVC on threshold graphs [3], exploiting their recursive structure and perfect elimination ordering properties. A graph is a threshold graph if it can be constructed from a single vertex by repeatedly adding either: an isolated vertex, or a dominating vertex. We present an efficient algorithm to compute the eternal relaxed vertex covering number for threshold graphs. Additionally, we establish bounds on the eternal relaxed vertex covering number \tau_r^\infty(G) in terms of classical graph parameters.

ABSTRACT. Colour Refinement is a combinatorial algorithm that computes a vertex colouring for an input graph to reveal its structural asymmetries. It has a precise correspondence with the 2- variable fragment of the counting logic C. This connection has yielded a deep understanding of the graphs and relational structures that can be defined in the logic. In this work, we shift the focus to definability of vertices. Those are vertices which can be “expressed” uniquely via a formula in the logic. They correspond to the vertices that receive a unique colour with respect to the algorithm. We show strong and tight lower bounds on vertex definability.

ABSTRACT. We develop a lattice-theoretic framework for query evaluation over incomplete databases under a group action on the space of possible worlds. Incomplete information is modeled as a space of possible worlds organized by the lattice of partitions. Queries and group actions induce two canonical operators on this lattice: a query refinement operator and a symmetry closure operator arising from stabilisers and their cores as normal subgroups. We study their interaction and characterize precise fixed-point conditions under which these operators are compatible in the sense of commuting on the partition lattice. This yields necessary and sufficient conditions for the existence of a decomposition of the valuation space into independent components, reducing query evaluation to componentwise computation. When these conditions fail, query and symmetry are intrinsically coupled and no such decomposition is possible.

ABSTRACT. The study of non-classical logics has long been intertwined with the investigation of algebraic structures that generalize Boolean algebras. Well-known examples include De Morgan algebras, Heyting algebras, Ockham algebras, and p-algebras, each of which gives rise to a distinct logical calculus. A recurring limitation in many of these frameworks is their reliance on a single negation operation or on negations that interact in a highly constrained manner. In this paper, we introduce and systematically study quad algebras, a new class of algebraic structures that accommodates multiple negation operations simultaneously. Quad algebras subsume both Boolean algebras and De Morgan algebras as special cases, thereby providing a strictly richer algebraic setting for investigating the interplay between different negation operators. We begin by establishing the fundamental algebraic theory of quad algebras, examining their lattice-theoretic properties and characterizing important subclasses. A central algebraic result shows that every quad algebra admits a natural ring structure induced by the Boolean negation present in the signature. Specifically, we prove that quad algebras are term-equivalent to a class of commutative rings in which every element satisfies the identity x⁴ = x. This generalizes the classical correspondence between Boolean algebras and Boolean rings (rings satisfying x² = x) established by Stone and places quad algebras within a broader ring-theoretic tradition. The identity x⁴ = x reflects the presence of a richer negation structure and yields a family of rings that properly extends the class of Boolean rings. On the logical side, we introduce a propositional calculus L_QA whose algebraic semantics is given by quad algebras, and we develop a corresponding four-valued semantics for it. The four truth values arise naturally from the structure of quad algebras and admit a transparent semantic interpretation in terms of the interaction between the two negation operators. We establish the soundness and completeness of L_QA with respect to this 4-valued semantics, thereby giving a precise logical meaning to the algebraic identity x⁴ = x. We further situate our work within the landscape of many-valued logic by comparing L_QA with Dunn’s four-valued semantics for the logic of first-degree entailment (FDE). While both systems employ four truth values and build on De Morgan-type structures, they differ in important respects: Dunn’s semantics is motivated by information-theoretic considerations and treats the four values as combinations of truth and falsity attributions, whereas the 4-valued semantics for L_QA arises from the interaction of two independent negation operators within the quad algebra framework. We identify the precise structural relationship between the two semantic frameworks and show how L_QA extends and departs from FDE in a logically meaningful way. Taken together, these results establish quad algebras as a coherent and novel contribution to the algebraic study of non-classical logics, providing a new setting in which multiple negations can be explored through both algebraic and semantic methods. Full proofs of all results presented here can be found in our published paper.

ABSTRACT. Real-life social interactions are complex and multifaceted, with different relationship types creating overlapping, interdependent networks. Understanding this complexity requires aggregating multiple individual social networks into a single, collective meta-network. Social networks possess many desirable properties. When each individual social network satisfies certain beneficial characteristics, it is natural to consider how the aggregation process can preserve these reserved properties. While with the cognitive and spatial limits of individual social networks, they always meet several deficiencies. We suggest a shift in how social network aggregation is understood. Instead of mere preservation, explore its potential as an active, corrective tool to eliminate these social network deficiencies. By synthesising diverse individual perspectives, we aim to use aggregation not only to reflect localised observations but also to uncover the true underlying social structures and to correct the inherent imperfections of individual networks. In this paper, we first represent social networks as undirected graphs $G = \langle A,E \rangle$ \cite{barabasi2014linked}. Building upon this graph-based approach, we formalise several properties inherent in social networks, including ``connectivity''\footnote{A social network is said to satisfy the property of connectivity if for every pair of distinct vertices \( u, v \in A \), there exists a path from \( u \) to \( v \).}, ``six degrees of separation''\footnote{A social network satisfies six degrees of separation if \(\forall \; a, b \in A \quad |P(a,b)| \leq 6\). Here $P(a, b)$ denotes the shortest path from $a$ to $b$.}, and ``weak ties''. Within our framework, when a social network lacks a desirable property or exhibits negative phenomena such as the ``majority illusion’’\footnote{The consensus among members of the local actor set regarding the existence of ties directly contradicts the global reality.}, we refer to these conditions as social network deficiencies. We employ the axiomatic method, rooted in social choice theory, to more thoroughly investigate the aggregation of social networks. Building on the framework of graph aggregation \cite{endriss2018graph}, our initial focus was on preserving desirable network properties. On the positive preservation side, we demonstrate that certain democratic aggregation rules, such as the nomination rule, preserve properties that strengthen network connections, such as connectivity, while others lead to impossibility results requiring oligarchic or dictatorial rules \cite{yi2026sna}. Despite these preservation results, a critical transition in our research was necessitated by the reality of observed social networks. Since we recognise that observed individual networks are inherently flawed due to epistemic limitations and cognitive boundaries, individual social networks frequently fail to exhibit the preferred structure and display several deficiencies. We pivot from standard preservation to a novel perspective. Can we use aggregation as a means to eliminate social network deficiencies? We reinterpret Condorcet's paradox within a social network context, treating aggregation as a corrective mechanism rather than a source of collective irrationality in preference aggregation. We demonstrate this corrective potential by aggregating a Condorcet-like profile of social networks. In classical social choice, Condorcet's paradox illustrates cyclic majorities and irrational outcomes. However, our network-theoretic reinterpretation yields a starkly contrasting result. We show that while the individual networks in the profile fail to satisfy triadic closure\footnote{A social network satisfies triadic closure if for any three distinct vertices $a,b,c\in A$, $(a,b),(b,c)\in E$ implies $(a,c)\in E$.}, the aggregated collective network successfully achieves it. This restatement provides a powerful proof of concept that aggregation can indeed eliminate structural defects. However, applying classic social choice axioms to eliminate network defects introduces severe theoretical limits. We establish a strong negative baseline: no aggregation rule that is both unanimous and grounded can eliminate a network deficiency if all individuals share the exact same flawed structure. To circumvent this negative baseline and develop a positive corrective framework, our ongoing research investigates two approaches of theoretical relaxation. The first is domain restrictions on profiles \cite{dietrich2010restrictdomains}. Rather than demanding a universal elimination of deficiencies across all conceivable profiles, we explore domain restrictions by imposing structural constraints on the individual input networks. Our goal is to find out under which profile or network conditions and constraints certain aggregation rules can effectively eliminate these social network deficiencies. Another consideration is about relaxing groundedness for structural inference. Similar to scholars who reject independence in judgment aggregation to avoid logical paradoxes\cite{list2002rejectindependent}, we challenge the groundedness axiom. Strict groundedness forces the collective networks to inherit individuals' local blind spots. However, an unobserved edge does not always mean there is no information transfer in a social network; it is sometimes just a limited viewpoint rather than a true disconnection. We relax this axiom to view aggregation as a process of uncovering the true social structure. This empowers the aggregation rule to perform structural inference, identifying ``latent ties'' (e.g., inferring an unobserved $(A,C)$ link from existing $(A,B)$ and $(B,C)$ guarantee the information transport between $A$ and $C$) and bridging these unobserved gaps to eliminate the social network deficiencies.

ABSTRACT. In this work, we argue that ignorance can be inherently understood as a hyperintensional notion. When faced with two logically or necessarily equivalent propositions, an agent may be ignorant of one while not of the other. To capture formally this intuition, we employ a topic-sensitive semantics, enabling the modeling of an agent's attitude toward the content of a proposition. Within this framework, we reevaluate three existing logical systems, usually characterized by standard Kripke semantics, to account for three forms of ignorance: ignorance whether, ignorance as unknown truth, and disbelieving ignorance. For each form, we present a sound and complete system. To highlight the advantage of this approach, we apply it to address the problem of logical omniscience rephrased in terms of ignorance. The resulting framework considers an agent's capacity to grasp the content of a proposition, bridging the gap between standard relational settings for ignorance representation and natural intuitions about the role of content in forming one's ignorance.

ABSTRACT. This work-in-progress project is motivated by enhancing our theoretical understanding of the information exchange that leads to belief polarization. We approach this subject with the aim of using modal logic to model agents that update their beliefs based on the bias they already have. We propose a direction that builds on known formalisms in doxastic and epistemic logic where we add an update operation to an agents' strength of evidence, which leads to a stronger belief. This abstract briefly discusses these ideas and outlines objectives of on-going work.

ABSTRACT. We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both events come with different modalities. In the logical semantics, formulas are interpreted in a world of an epistemic model (an S5 Kripke model) given a history of prior announcements and receptions. Consequently, agents' knowledge depends on two kinds of uncertainty: agents not only consider several possible worlds but they also reason over different histories of epistemic actions (of possibly different length). From this, two notions of validity arise. On the one hand, standard validities are formulas thtrue in every state of every epistemic model when no prior sending and receiving events have happened. Always-validities, on the other hand, are formulas that are true in every state of every model, after any prior history of such events. A reduction-based axiomatisation AA for standard validities has been proposed in a prior work. Here, we present an axiomatisation AA* for always-validities which is an infinitary system. Interestingly, the single-agent case requires an adaptation of our axiomatisation. We present the logic and the method to axiomatise always-validities, and explain why the method for multiple agents needs to be adapted for a single agent.

ABSTRACT. Machine learning classifiers work by being given a dataset of instances described by feature values and class labels, and then learning to predict the label of a new instance. Some methods do this in an interpretable way, producing simple if-then rules that a person can read directly. A learned rule set of this kind may say that one feature pattern usually predicts one label, except when a more specific pattern predicts the opposite. People naturally read such outputs as defaults and exceptions, but a readable rule set is not automatically a defeasible theory: it may look defeasible without any formal guarantee that its predictions correspond to principled nonmonotonic reasoning. We identify a single syntactic condition on learned conjunctive rule sets, called strict global exception closure, under which the classifier is provably a KLM defeasible theory whose predictions agree with defeasible entailment under Rational Closure, Lexicographic Closure, and System W simultaneously.

ABSTRACT. We investigate the proof-theoretic structure of incorrect/incomplete proofs, that is, derivations containing syntactic errors or incomplete inferential steps that nonetheless preserve partial semantic validity. Building on Hilbert’s epsilon calculus, we formalize how such derivations can be corrected through semantic projection and weakest preconditions, leading to valid Herbrand disjunctions. We show that the epsilon calculus provides a natural framework for analyzing tolerance of falsity in proofs and for identifying conditions under which an incorrect proof can be semantically repaired. This approach extends Hilbert’s program beyond correctness, toward a logic of error and recovery. Moreover we show that the extended first epsilon theorem is false-tolerant.

ABSTRACT. The classical natural deduction system $\mathbf{NK}$ can be obtained from the intuitionistic system $\mathbf{NJ}$ by adding a double negation elimination inference rule ($DNE$). On the other hand, the intuitionistic and classical sequent calculi $\mathbf{LJ}$ and $\mathbf{LK}$ are differentiated by the number of formulae that can be contained in the right-hand side of a sequent. In an $\mathbf{LJ}$-derivation, the right-hand side of a sequent can contain at most one formula; $\mathbf{LK}$ is obtained by lifting this restriction, giving it the property of right multiplicity. This distinction between $\mathbf{LJ}$ and $\mathbf{LK}$ is notably different from the distinction between $\mathbf{NJ}$ and $\mathbf{NK}$: the first is purely structural, and the second involves the explicit addition of a classical inference pattern. We demonstrate how the same classical strength, in terms of what can be derived, emerges from $DNE$ and right multiplicity in $\mathbf{NK}$ and $\mathbf{LK}$, respectively. In particular, we show that the classical strength of $\mathbf{LK}$ arises from right multiplicity through its interactions with the negation and implication rules in a way that is formally analogous to how $DNE$ interacts with the equivalent rules in $\mathbf{NK}$.

ABSTRACT. The notion of proof is central to both mathematical logic and computer-assisted reasoning, traditionally understood as a sequence of locally verifiable inference steps. While this formal view enables automation and verification, it often obscures the structural insights underlying mathematical arguments. Proof analysis aims to recover this structure, with cut-elimination and Herbrand’s theorem playing a key role in extracting computational content from proofs. However, these classical tools face limitations in the presence of induction, where proofs implicitly represent infinite reasoning. To address this, proof schemata provide finite representations of infinite families of proofs, enabling schematic cut-elimination methods such as CERES and the extraction of Herbrand systems. In parallel, cyclic proofs offer an alternative framework for inductive reasoning using globally justified cycles instead of explicit induction rules. This work investigates the relationship between these two formalisms. We present a translation from a restricted class of cyclic proofs in the system CLKID^omega into proof schemata, enabling the direct application of schematic analysis techniques. Under suitable restrictions on quantification and inductive definitions, this translation facilitates the extraction of Herbrand systems from cyclic proofs. The approach is illustrated using the 2-Hydra example, demonstrating that proof schemata can capture inductive arguments beyond Peano Arithmetic. At the same time, we show that proof schemata and Peano Arithmetic are incomparable in expressive power.

ABSTRACT. Modal logics are non-classical logics that extend classical logic with modal operators □ and ♢ respectively representing necessity and possibility. An implementation of model finding in quantified modal logics is given by the finite model finder MoMo for quantified mono-modal logics. While results of its evaluation prove the practicality of this method, challenges specific to the translational approach for model finding followed by MoMo can be observed. This extended abstract addresses them and discusses potential solutions to overcome them.

ABSTRACT. The interest in explanations in the context of AI research is often directly associated with the field of explainable AI (XAI), where one of the goals is to automatically generate explanations of the outputs of AI-based systems—in particular the outputs of machine learning systems [4]. Still, especially in relation to normative questions, there is an established line of research aimed at automating explanations of other phenomena; notably, AI-based systems have been used for generating explanations of legal outcomes [1]. We consider related research where explanatory dialogue games generated from argumentation frames are developed [2, 6], and we extend these approaches by (i) considering agent uncertainty, modeled via argumentation frames with preferences, which gives rise to a new type of locution, or speech act, in the dialogues and by (ii) considering the role of specific relations between norms in the case of explanations with deontic or normative components, as in [6], and thus also a new type of locution in the dialogues. Explanations, as they are considered here, can be defined as answers to “why-questions,” a definition taken from research in the humanities and social sciences [4]. From this research certain features have been identified as important for explanations to be understandable and useful to humans: “good” explanations are contrastive, selective, non-probabilistic and social. It is claimed in [1] that legal explanations naturally have each of these features, but it is not clear to what extent these features remain desirable for normative or deontic explanations (of which legal explanations are a subclass). This is because much of the research considered in [4] is concerned with explanations which are causal in nature, and there is reason to believe that normative explanations are not the same as, nor reducible to causal explanations [7]. In particular, theories of contrastive explanation make explicit reference to causal histories [3], and we want to address two types of explanations of normative issues which appeal, not to the causal history of some putative fact coming to be, but instead (i) to the relative quality of the evidence in favor of concluding that fact or (ii) to the relation between some norm(s) from which the fact would follow and other more basic norms or principles. Thus, we move toward explanations which are not strictly contrastive because the setting is no longer purely causal. In order order to allow for explanations of these types, we propose a framework like those discussed in [2, 6], with some additional features. First, we define the argumentation frames on which the dialogues are based. We consider argumentation frames which incorporate pref- erences over arguments because we want to consider agent uncertainty, and this is modeled via arguments that rest on premises of varying quality. Specifically, we use structured argumenta- tion frames where the logical content of each argument defines which arguments it attacks, and we make use of a preference ordering over the set of arguments based on a preference ordering over the potential argument premises, as, for example, in [5]. This captures how the strength of certain beliefs/evidence can affect the strength of arguments, and this doxastic component bears on deontic explanations despite its independent interest; for example, agents can explain disagreements about violations via appeal to individual beliefs about the facts or norms. We then consider a new locution in the dialogues based on these argumentation frames, whereby arguments can be defended from attacking arguments by appeal to the preference ordering. In natural language these new locutions represent statements like “while that would be a reason to reject my claim, it is not supported by the evidence,” and such locutions allow us to give explanatory meaning to the preferences included in the argumentation frame. A second modification to the methods of [2, 6] that we consider is to allow for locutions which question norms themselves; while in [6] it is possible to question obligations following from norms, there is no way to question norms directly. However, such “why-norm-questions” are common in ethical and legal discourse. In order to incorporate these questions into our dialogue games we consider two ideas for extensions to the underlying argumentation frames. The first idea is to include an additional knowledge base which encodes the relational structure between the norms; general norms like “thou shalt not lie” might be the normative grounding for more specific norms like “don’t say you are coming, if you are not going to come,” and the knowledge base would capture these inter-norm relations which could be exploited for explanation. The second proposal is to include an additional labeling on the norms, which encodes the principles or values on which each norm is based, e.g. honesty, fairness, etc. Then, agents could respond to “why-norm-questions” by providing these principles. We also consider requirements on these types of locutions which might make such dialogues more plausible; e.g. we could require that agents only question norms they do not rely on in their previously moved arguments. By including these novel locutions and encoding this extra information in the argumentation frame, we are able to explore the role of “why-norm-questions” in explanatory dialogues. In sum, although the push to include conceptual research on explanations introduces key desiderata for “good explanations” in the context of XAI, we have to carefully consider whether these apply equally to normative explanations. We argue that the requirement of contrastive explanations should be relaxed in order to support questions about the norms themselves, and that explanations of certain facts need not always appeal to counterarguments against alternatives, but may also be supported by arguments in favor of their evidential or doxastic grounds. Finally, we present and investigate extended argumentation frameworks which can support dialogue games with additional locutions for the proposed purposes. References: [1] Katie Atkinson, Trevor Bench-Capon, and Danushka Bollegala. “Explanation in AI and law: Past, present and future”. In: Artificial Intelligence 289 (2020). [2] Xiuyi Fan and Francesca Toni. “On Computing Explanations in Argumentation”. In: Pro- ceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. 2015, pp. 1496– 1502. [3] Tim Miller. “Contrastive explanation: a structural-model approach”. In: The Knowledge Engineering Review 36 (2021), e14. [4] Tim Miller. “Explanation in artificial intelligence: Insights from the social sciences”. In: Artificial Intelligence 267 (2019), pp. 1–38. [5] Sanjay Modgil and Henry Prakken. “A general account of argumentation with preferences”. In: Artificial Intelligence 195 (2013), pp. 361–397. [6] Kees van Berkel and Christian Straßer. “Towards Deontic Explanations Through Dia- logue”. In: ArgXAI-24: 2nd International Workshop on Argumentation for eXplainable AI. 2024. [7] Kate Vredenburgh. “The Right to Explanation”. In: The Journal of Political Philosophy 30.2 (2022), pp. 209–229.

ABSTRACT. Dynamic Epistemic Logic (DEL) extends epistemic logic by modelling how knowledge is revised through communication events, represented by dynamic modalities. Among the simplest and historically most influential systems of DEL is Public Announcement Logic (PAL). Unlike in epistemic logic, that models agents' knowledge through static sets of possible worlds, PAL focuses on how public communication updates agents' knowledge, through transformations of these structures. In PAL then, an announcement by A updates an epistemic model (S5 Kripke model) into a new model. While the semantics of PAL is inherently dynamic, with updates of epistemic models, its proof-theoretic side has been lacking a syntactic representation of such a dynamism for a long time. In a previous work, we introduced dynamic hypersequents to represent with purely syntactical means the inherent dynamism of PAL. Within this framework we proposed a calculus for the single-agent fragment of PAL. Building on this and on a method to represent agents' uncertainty in hypersequents, we now introduce indexed dynamic hypersequents and propose a hypersequent calculus for the full logic of public announcements. This calculus is sound and complete, and enjoys several important properties: in particular, all its structural rules, including the contraction rules as well as the cut-rule, are provably admissible.