arXiv subjects

Alessandra Palmigiano

Publications and source records attributed to Alessandra Palmigiano.

At least 19 recordsLinked to original sources

arXiv2026

A proof-theoretic approach to abstract interpretation

This paper develops a proof-theoretic framework for abstract interpretation by systematically associating logical systems with finite abstractions. Building on earlier work on the internal logics of abstractions, we propose a general procedure for generating a logic whose Lindenbaum-Tarski algebra is isomorphic to a given abstract lattice. The approach identifies logical connectives preserved by the concretization map and derives corresponding proof rules and axioms. The paper establishes soundness and completeness results under suitable conditions, extends the framework to Cartesian products and multi-variable settings, and investigates the logical structure of non-Cartesian abstractions such as octagons. These observations suggest new connections between abstract interpretation, proof theory, and algebraic logic, providing a foundation for a systematic logical analysis of program abstractions.

cs.LO↗

arXiv2026

Refutation calculi for lattice-based logics: from display to tableaux

Refutation calculi are formal systems developed to derive the invalid formulas of a given logic. While the notion of refutation calculi has played a key role in the development of tableaux calculi, a refutation approach to display calculi has not yet been attempted. In this paper, we introduce refutation display calculi for basic LE-logics, i.e., those logics canonically associated with basic normal lattice expansions of any signature. In particular, we prove soundness and completeness via proof-analysis results on derivable sequents. Finally, we obtain terminating tableaux calculi from these refutation display calculi.

math.LO↗

arXiv2026

Modular constructive Lyndon interpolation for nondistributive logics

We establish the Lyndon interpolation property for basic lattice expansion logics (LE-logics) in arbitrary signatures using display calculi. Our approach is constructive, yielding interpolants algorithmically from derivations, and modular, in the sense that interpolation for axiomatic extensions can be obtained by verifying a local interpolation property for the analytic structural rules corresponding to the additional axioms. To this end, we identify a class of interpolation-safe structural rules preserving local Lyndon interpolation. As applications of the general framework, we show that the tense version of Holliday's fundamental modal logic enjoys the Lyndon interpolation property.

math.LO↗

arXiv2026

Inception Display Calculi

Display calculi were introduced by Nuel Belnap in `Display logic' (1982) as a natural extension of Gentzen's sequent calculi, as a uniform and modular framework capable of encompassing broad classes of logics. In `Unified correspondence as a proof-theoretic tool', the properly displayable (D)LE-logics are syntactically characterized as the logics axiomatised by analytic inductive axioms for any signature. We extend the framework of proper display calculi for LE-logics to include axiomatic extensions with axioms that are inductive but not necessarily analytic inductive. This class of axioms covers and properly extends all Sahlqvist axioms. The present framework takes inspiration from Schroeder-Heister's calculus of Higher-Level Rules and captures the whole acyclic fragment of the substructural hierarchy when generalized to arbitrary signatures. We apply unified correspondence theory and the algorithm ALBA to uniformly generate analytic rules for the aforementioned axiomatic extensions.

math.LO↗

arXiv2025

Questions as cognitive filters

In this paper, we develop a logico-algebraic framework for modeling decision-making through deliberation in multi-agent settings. The central concept in this framework is that of interrogative agendas, which represent the cognitive stances of agents regarding which features should be considered relevant in the final decision. We formalize an agent's interrogative agenda as an equivalence relation that identifies outcomes differing only in aspects the agent deems irrelevant. Moreover, we characterize the sublattices of the resulting lattice that correspond to relevant interrogative agendas for deliberation scenarios governed by different ``winning rules." We then introduce a two-sorted logico-algebraic structure-comprising the lattice of relevant interrogative agendas and the Boolean algebras of agent coalitions-to model the interaction between agents and agendas during deliberation. Finally, we discuss which interaction conditions can and cannot be defined within this framework.

cs.LO↗

arXiv2025

Algorithmic correspondence and analytic rules

We introduce the algorithm MASSA which takes classical modal formulas in input, and, when successful, effectively generates: (a) (analytic) geometric rules of the labelled calculus G3K, and (b) cut-free derivations (of a certain `canonical' shape) of each given input formula in the geometric labelled calculus obtained by adding the rule in output to G3K. We show that MASSA successfully terminates whenever its input formula is a (definite) analytic inductive formula, in which case, the geometric axiom corresponding to the output rule is, modulo logical equivalence, the first-order correspondent of the input formula. In proving the correctness of MASSA, we also show that the algorithm for the elimination of second-order quantifiers SCAN is complete with respect to the class of inductive analytic formulas. Finally, we show how our algorithm can be extended to the class of inductive formulas and to modal logic with quantifiers.

math.LO↗

arXiv2025

Normative implications

We continue to develop a research line initiated in \cite{wollic22}, studying I/O logic from an algebraic approach based on subordination algebras. We introduce the classes of slanted (co-)Heyting algebras as equivalent presentations of distributive lattices with subordination relations. Interpreting subordination relations as the algebraic counterparts of input/output relations on formulas yields (slanted) modal operations with interesting deontic interpretations. We study the theory of slanted and co-slanted Heyting algebras, develop algorithmic correspondence and inverse correspondence, and present some deontically meaningful axiomatic extensions and examples.

math.LO↗

arXiv2024

Flexible categorization using formal concept analysis and Dempster-Shafer theory

The framework developed in the present paper provides a formal ground to generate and study explainable categorizations of sets of entities, based on the epistemic attitudes of individual agents or groups thereof. Based on this framework, we discuss a machine-leaning meta-algorithm for outlier detection and classification which provides local and global explanations of its results.

cs.AI↗

arXiv2024

Correspondence and Inverse Correspondence for Input/Output Logic and Region-Based Theories of Space

We further develop the algebraic approach to input/output logic initiated in \cite{wollic22}, where subordination algebras and a family of their generalizations were proposed as a semantic environment of various input/output logics. In particular: we extend the modal characterizations of a finite number of well known conditions on normative and permission systems, as well as on subordination, precontact, and dual precontact algebras developed in \cite{de2024obligations}, to those corresponding to the infinite class of {\em clopen-analytic inequalities} in a modal language consisting both of positive and of negative unary modal operators; we characterize the syntactic shape of first-order conditions on algebras endowed with subordination, precontact, and dual precontact relations which guarantees these conditions to be the first-order correspondents of axioms in the modal language above; we introduce algorithms for computing the first-order correspondents of modal axioms on algebras endowed with subordination, precontact, and dual precontact relations, and conversely, for computing the modal axioms of which the conditions satisfying the suitable syntactic shape are the first-order correspondents; finally, we extend Celani's dual characterization results between subordination lattices and subordination spaces to a wider environment which also encompasses precontact and dual precontact relations, and relative to an infinite class of first order conditions relating subordination, precontact and dual precontact relations on distributive lattices. The modal characterizations established in the present paper pave the way to establishing faithful embeddings for infinite classes of input/output logics, and hence to their implementation in LogiKEy, Isabelle/HOL, Lean, or other interactive systems.

cs.LO↗

arXiv2024

Unified inverse correspondence for LE-logics

We generalize Kracht's theory of internal describability from classical modal logic to the family of all logics canonically associated with varieties of normal lattice expansions (LE algebras). We work in the purely algebraic setting of perfect LEs; the formulas playing the role of Kracht's formulas in this generalized setting pertain to a first order language whose atoms are special inequalities between terms of perfect algebras. Via duality, formulas in this language can be equivalently translated into first order conditions in the frame correspondence languages of several types of relational semantics for LE-logics.

math.LO↗

arXiv2024

Non-distributive description logic

We define LE-ALC, a generalization of the description logic ALC based on the propositional logic of general (i.e. not necessarily distributive) lattices, and semantically interpreted on relational structures based on formal contexts from Formal Concept Analysis (FCA). The description logic LE-ALC allows us to formally describe databases with objects, features, and formal concepts, represented according to FCA as Galois-stable sets of objects and features. We describe ABoxes and TBoxes in LE-ALC, provide a tableaux algorithm for checking the consistency of LE-ALC knowledge bases with acyclic TBoxes, and show its termination, soundness and completeness. Interestingly, consistency checking for LE-ALC is in PTIME for acyclic and completely unravelled TBoxes, while the analogous problem in the classical ALC setting is PSPACE-complete.

math.LO↗

arXiv2024

Modal reduction principles: a parametric shift to graphs

Graph-based frames have been introduced as a logical framework which internalizes an inherent boundary to knowability. They also support the interpretation of lattice-based (modal) logics as hyper-constructive logics of evidential reasoning. Conceptually, the present paper proposes graph-based frames as a formal framework suitable for generalizing Pawlak's rough set theory to a setting in which inherent limits to knowability need to be considered. Technically, the present paper establishes systematic connections between the first-order correspondents of Sahlqvist modal reduction principles on Kripke frames, and on the more general relational environments of graph-based and polarity-based frames. This work is part of a research line aiming at: (a) comparing and inter-relating the various (first-order) conditions corresponding to a given (modal) axiom in different relational semantics (b) recognizing when first-order sentences in the frame-correspondence languages of different relational structures encode the same modal content (c) meaningfully transferring relational properties across different semantic contexts. The present paper develops these results for the graph-based semantics, polarity-based semantics, and all Sahlqvist modal reduction principles. As an application, we study well known modal axioms in rough set theory on graph-based frames and show that, although these axioms correspond to different first-order conditions on graph-based frames, their intuitive meaning is retained.This allows us to introduce the notion of hyperconstructivist approximation spaces as the subclass of graph-based frames defined by the first-order conditions corresponding to the same modal axioms defining classical generalized approximation spaces, and to transfer the properties and the intuitive understanding of different approximation spaces to graph-based frames.

math.LO↗

arXiv2024

Obligations and permissions, algebraically

math.LO↗

arXiv2024

Obligations and permissions on selfextensional logics

We further develop the abstract algebraic logic approach to input/output logic initiated in \cite{wollic22}, where the family of selfextensional logics was proposed as a general background environment for input/output logics. In this paper, we introduce and discuss the generalizations of several types of permission (negative, dual negative, static, dynamic), as well as their interactions with normative systems, to various families of selfextensional logics, thereby proposing a systematic approach to the definition of normative and permission systems on nonclassical propositional bases.

math.LO↗

arXiv2024

Labelled calculi for lattice-based modal logics

We introduce labelled sequent calculi for the basic normal non-distributive modal logic L and 31 of its axiomatic extensions, where the labels are atomic formulas of a first order language which is interpreted on the canonical extensions of the algebras in the variety corresponding to the logic L. Modular proofs are presented that these calculi are all sound, complete and conservative w.r.t. L, and enjoy cut elimination and the subformula property. The introduction of these calculi showcases a general methodology for introducing labelled calculi for the class of LE-logics and their analytic axiomatic extensions in a principled and uniform way.

math.LO↗

arXiv2024

Labelled calculi for the logics of rough concepts

We introduce sound and complete labelled sequent calculi for the basic normal non-distributive modal logic L and some of its axiomatic extensions, where the labels are atomic formulas of the first order language of enriched formal contexts, i.e., relational structures based on formal contexts which provide complete semantics for these logics. We also extend these calculi to provide a proof system for the logic of rough formal contexts.

math.LO↗

arXiv2024

Algebraic proof theory for LE-logics

In this paper we extend the research programme in algebraic proof theory from axiomatic extensions of the full Lambek calculus to logics algebraically captured by certain varieties of normal lattice expansions (normal LE-logics). Specifically, we generalise the residuated frames in [34] to arbitrary signatures of normal lattice expansions (LE). Such a generalization provides a valuable tool for proving important properties of LE-logics in full uniformity. We prove semantic cut elimination for the display calculi D.LE associated with the basic normal LE-logics and their axiomatic extensions with analytic inductive axioms. We also prove the finite model property (FMP) for each such calculus D.LE, as well as for its extensions with analytic structural rules satisfying certain additional properties.

math.LO↗

arXiv2024

Generating proof systems for three-valued propositional logics

In general, providing an axiomatization for an arbitrary logic is a task that may require some ingenuity. In the case of logics defined by a finite logical matrix (three-valued logics being a particularly simple example), the generation of suitable finite axiomatizations can be completely automatized, essentially by expressing the matrix tables via inference rules. In this chapter we illustrate how two formalisms, the 3-labelled calculi of Baaz, Fermüller and Zach and the multiple-conclusion (or Set-Set) Hilbert-style calculi of Shoesmith and Smiley, may be uniformly employed to axiomatize logics defined by a three-valued logical matrix. The generating procedure common to both formalisms can be described as follows: first (i) convert the matrix semantics into rule form (we refer to this step as the generating subprocedure) and then (ii) simplify the set of rules thus obtained, essentially relying on the defining properties of any Tarskian consequence relation (we refer to this step as the streamlining subprocedure). We illustrate through some examples that, if a minimal expressiveness assumption is met (namely, if the matrix defining the logic is monadic), then it is straightforward to define effective translations guaranteeing the equivalence between the 3-labelled and the Set-Set approach.

math.LO↗