arXiv ScienceSearch

arXiv subjects

Giuseppe Greco

Publications and source records attributed to Giuseppe Greco.

At least 19 recordsLinked to original sources

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

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

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

Probing Cosmic Expansion and Early Universe with Einstein Telescope

Over the next two decades, gravitational-wave (GW) observations are expected to evolve from a discovery-driven endeavour into a precision tool for astrophysics, cosmology, and fundamental physics. Current second-generation ground-based detectors have established the existence of compact-binary mergers and enabled GW multi-messenger astronomy, but they remain limited in sensitivity, redshift reach, frequency coverage, and duty cycle. These limitations prevent them from addressing many fundamental open questions in cosmology. By the 2040s, wide-field electromagnetic surveys will have mapped the luminous Universe with unprecedented depth and accuracy. Nevertheless, key problems including the nature of dark matter, the physical origin of cosmic acceleration, the properties of gravity on cosmological scales, and the physical conditions of the earliest moments after the Big Bang will remain only partially constrained by electromagnetic observations alone. Progress on these fronts requires access to physical processes and epochs that do not emit light. Gravitational waves provide a unique and complementary observational channel: they propagate over cosmological distances largely unaffected by intervening matter, probe extreme astrophysical environments, and respond directly to the geometry of spacetime. In this context, next-generation GW observatories such as the Einstein Telescope (ET) will be transformative for European astronomy. Operating at sensitivities and frequencies beyond existing detectors, ET will observe binary black holes and neutron stars out to previously inaccessible redshifts, enable continuous high signal-to-noise monitoring of compact sources, and detect gravitational-wave backgrounds of astrophysical and cosmological origin. Together with space-based detectors, ET will play a central role in advancing our understanding of cosmic evolution and fundamental physics.

astro-ph.CO

Encapsulating Textual Contents into a MOC data Structure for Advanced Applications

Context. The Multi-Order Coverage map (MOC) is a widely adopted standard promoted by the International Virtual Observatory Alliance (IVOA) to support data sharing and interoperability within the Virtual Observatory (VO) ecosystem. This hierarchical data structure efficiently encodes and visualizes irregularly shaped regions of the sky, enabling applications such as cross-matching large astronomical catalogs. Aims. This study aims to explore potential enhancements to the MOC data structure by encapsulating textual descriptions and semantic embeddings into sky regions. Specifically, we introduce "Textual MOCs", in which textual content is encapsulated, and "Semantic MOCs" that transform textual content into semantic embeddings. These enhancements are designed to enable advanced operations such as similarity searches and complex queries and to integrate with generative artificial intelligence (GenAI) tools. Method. We experimented with Textual MOCs by annotating detailed descriptions directly into the MOC sky regions, enriching the maps with contextual information suitable for interactive learning tools. For Semantic MOCs, we converted the textual content into semantic embeddings, numerical representations capturing textual meanings in multidimensional spaces, and stored them in high-dimensional vector databases optimized for efficient retrieval. Results. The implementation of Textual MOCs enhances user engagement by providing meaningful descriptions within sky regions. Semantic MOCs enable sophisticated query capabilities, such as similarity-based searches and context-aware data retrieval. Integration with multimodal generative AI systems allows for more accurate and contextually relevant interactions supporting both spatial, semantic and visual operations for advancing astronomical data analysis capabilities.

astro-ph.IM

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

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

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

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

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

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

Current transport in Ni Schottky barrier on GaN epilayer grown on free standing substrates

In this paper, the Ni Schottky barrier on GaN epilayer grown on free standing substrates has been characterized. First, transmission electrical microscopy (TEM) images and nanoscale electrical analysis by conductive atomic force microscopy (C-AFM) of the bare material allowed visualizing structural defects in the crystal, as well as local inhomogeneities of the current conduction. The forward current-voltage (I-V) characteristics of Ni/GaN vertical Schottky diodes fabricated on the epilayer gave average values of the Schottky barrier height of 0.79 eV and ideality factor of 1.14. A statistical analysis over a set of diodes, combined with temperature dependence measurements, confirmed the formation of an inhomogeneous Schottky barrier in this material. From a plot of FB versus n, an ideal homogeneous barrier close to 0.9 eV was estimated, similar to that extrapolated by capacitance-voltage (C-V) analysis. Local I-V curves, acquired by means of C-AFM, displayed the inhomogeneous distribution of the onset of current conduction, which in turn resembles the one observed in the macroscopic Schottky diodes. Finally, the reverse characteristic of the diodes fabricated in the defects-free region have been acquired at different temperature and its behaviour has been described by the thermionic field emission (TFE) model.

cond-mat.mtrl-sci

Threshold voltage instability by charge trapping effects in the gate region of p-GaN HEMTs

In this work, the threshold voltage instability of normally-off p-GaN high electron mobility transistors (HEMTs) has been investigated by monitoring the gate current density during device on-state. The origin of the gate current variations under stress has been ascribed to charge trapping occurring at the different interfaces in the metal/p-GaN/AlGaN/GaN system. In particular, depending on the stress bias level, electrons (VG < 6 V) or holes (VG > 6 V) are trapped, causing a positive or negative threshold voltage shift {DVTH, respectively. By monitoring the gate current variations at different temperatures, the activation energies associated to the electrons and holes trapping could be determined and correlated with the presence of nitrogen (electron traps) or gallium (hole traps) vacancies. Moreover, the electrical measurements suggested the generation of a new electron-trap upon long-time bias stress, associated to the creation of crystallographic dislocation-like defects extending across the different interfaces (p-GaN/AlGaN/GaN) of the gate stack.

physics.app-ph

Unified inverse correspondence for DLE-Logics

By exploiting the algebraic and order theoretic mechanisms behind Sahlqvist correspondence, the theory of unified correspondence provides powerful tools for correspondence and canonicity across different semantics and signatures, covering all the logics whose algebraic semantics are given by normal (distributive) lattice expansions (referred to as (D)LEs). In particular, the algorithm ALBA, parametric in each (D)LE, effectively computes the first order correspondents of (D)LE-inductive formulas. We present an algorithm that makes use of ALBA's rules and algebraic language to invert its steps in the DLE setting; therefore effectively computing an inductive formula starting from its first order correspondent.

math.LO

Multi Order Coverage data structure to plan multi-messenger observations

We describe the use of Multi Order Coverage (MOC) maps as a practical way to manage complex regions of the sky for the planning of multi-messenger observations. MOC maps are a data structure that provides a multi-resolution representation of irregularly shaped and fragmentary regions over the sky based on the HEALPix (Hierarchical Equal Area isoLatitude Pixelization) tessellation. We present a new application of MOC, in combination with the \texttt{astroplan} observation planning package, to enable the efficient computation of sky regions and the visibility of these regions from a specific location on the Earth at a particular time. Using the example of the low-latency gravitational-wave alerts, and a simulated observational campaign with three observatories, we show that the use of MOC maps allows a high level of interoperability to support observing schedule plans. Gravitational-wave detections have an associated credible region localization on the sky. We demonstrate that these localizations can be encoded as MOC maps, and how they can be used in visualisation tools, and processed (filtered, combined) and also their utility for access to Virtual Observatory services which can be queried 'by MOC' for data within the region of interest. The ease of generating the MOC maps and the fast access to data means that the whole system can be very efficient, so that any updates on the gravitational-wave sky localization can be quickly taken into account and the corresponding adjustments to observing schedule plans can be rapidly implemented. We provide example python code as a practical example of these methods. In addition, a video demonstration of the entire workflow is available.

astro-ph.IM

First order logic properly displayed

We introduce a proper display calculus for first-order logic, of which we prove soundness, completeness, conservativity, subformula property and cut elimination via a Belnap-style metatheorem. All inference rules are closed under uniform substitution and are without side conditions.

math.LO

Neighbourhood semantics for graded modal logic

We introduce a class of neighbourhood frames for graded modal logic embedding Kripke frames into neighbourhood frames. This class of neighbourhood frames is shown to be first-order definable but not modally definable. We also obtain a new definition of graded bisimulation with respect to Kripke frames by modifying the definition of monotonic bisimulation.

math.LO

Vector spaces as Kripke frames

In recent years, the compositional distributional approach in computational linguistics has opened the way for an integration of the \emph{lexical} aspects of meaning into Lambek's type-logical grammar program. This approach is based on the observation that a sound semantics for the associative, commutative and unital Lambek calculus can be based on vector spaces by interpreting fusion as the tensor product of vector spaces. In this paper, we build on this observation and extend it to a `vector space semantics' for the \emph{general} Lambek calculus, based on \emph{algebras over a field} $\mathbb{K}$ (or $\mathbb{K}$-algebras), i.e. vector spaces endowed with a bilinear binary product. Such structures are well known in algebraic geometry and algebraic topology, since they are important instances of Lie algebras and Hopf algebras. Applying results and insights from duality and representation theory for the algebraic semantics of nonclassical logics, we regard $\mathbb{K}$-algebras as `Kripke frames' the complex algebras of which are complete residuated lattices. This perspective makes it possible to establish a systematic connection between vector space semantics and the standard Routley-Meyer semantics of (modal) substructural logics.

cs.LO