arXiv subjects
Publications and source records attributed to Giuseppe Greco.
We introduce a multi-type display calculus for Propositional Dynamic Logic (PDL). This calculus is complete w.r.t. PDL, and enjoys Belnap-style cut-elimination and subformula property.
We introduce the logic LRC, designed to describe and reason about agents' abilities and capabilities in using resources. The proposed framework bridges two - up to now - mutually independent strands of literature: the one on logics of abilities and capabilities, developed within the theory of agency, and the one on logics of resources, motivated by program semantics. The logic LRC is suitable to describe and reason about key aspects of social behaviour in organizations. We prove a number of properties enjoyed by LRC (soundness, completeness, canonicity, disjunction property) and its associated analytic calculus (conservativity, cut elimination and subformula property). These results lay at the intersection of the algebraic theory of unified correspondence and the theory of multi-type calculi in structural proof theory. Case studies are discussed which showcase several ways in which this framework can be extended and enriched while retaining its basic properties, so as to model an array of issues, both practically and theoretically relevant, spanning from planning problems to the logical foundations of the theory of organizations.
With the detection of a binary neutron star system and its corresponding electromagnetic counterparts, a new window of transient astronomy has opened. Due to the size of the error regions, which can span hundreds to thousands of square degrees, there are significant benefits to optimizing tilings for these large sky areas. The rich science promised by gravitational-wave astronomy has led to the proposal for a variety of tiling and time allocation schemes, and for the first time, we make a systematic comparison of some of these methods. We find that differences of a factor of 2 or more in efficiency are possible, depending on the algorithm employed. For this reason, for future surveys searching for electromagnetic counterparts, care should be taken when selecting tiling, time allocation, and scheduling algorithms to maximize the probability of counterpart detection.
We introduce a proper multi-type display calculus for bilattice logic (with conflation) for which we prove soundness, completeness, conservativity, standard subformula property and cut-elimination. Our proposal builds on the product representation of bilattices and applies the guidelines of the multi-type methodology in the design of display calculi.
We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and sub-formula property. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest Belnap-style proof of cut-elimination. Our proposal builds on an algebraic and order-theoretic analysis of the semantic environment of lattice logic, and applies the guidelines of the multi-type methodology in the design of display calculi.
We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut-elimination and subformula property. Based on the same design, we introduce a variant of Lambek calculus with exponentials, aimed at capturing the controlled application of exchange and associativity. Properness (i.e. closure under uniform substitution of all parametric parts in rules) is the main interest and added value of the present proposal, and allows for the smoothest proof of cut-elimination. Our proposal builds on an algebraic and order-theoretic analysis of linear logic, and applies the guidelines of the multi-type methodology in the design of display calculi.
Display calculi are generalized sequent calculi which enjoy a `canonical' cut elimination strategy. That is, their cut elimination is uniformly obtained by verifying the assumptions of a meta-theorem, and is preserved by adding or removing structural rules. In the present paper, we discuss a proof-theoretic setting, inspired both to Belnap's Display Logic and to Sambin's Basic Logic, which generalises these calculi in two directions: by explicitly allowing different types, and by weakening the so-called display and visibility properties. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth proof-theoretic treatment of multi-modal and dynamic logics. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit connectives which are neither adjoints nor residuals, or logics that are not closed under uniform substitution. In the present paper, we give a general overview of the calculi which we refer to as multi-type calculi, and we discuss their canonical cut elimination meta-theorem.
In this paper, we define a multi-type calculus for inquisitive logic, which is sound, complete and enjoys Belnap-style cut-elimination and subformula property. Inquisitive logic is the logic of inquisitive semantics, a semantic framework developed by Groenendijk, Roelofsen and Ciardelli which captures both assertions and questions in natural language. Inquisitive logic is sound and complete w.r.t. the so-called state semantics (also known as team semantics). The Hilbert-style presentation of inquisitive logic is not closed under uniform substitution; indeed, some occurrences of formulas are restricted to a certain subclass of formulas, called flat formulas. This and other features make the quest for analytic calculi for this logic not straightforward. We develop a certain algebraic and order-theoretic analysis of the team semantics, which provides the guidelines for the design of a multi-type environment which accounts for two domains of interpretation, for flat and for general formulas, as well as for their interaction. This multi-type environment in its turn provides the semantic environment for the multi-type calculus for inquisitive logic we introduce in this paper.
The present paper aims at establishing formal connections between correspondence phenomena, well known from the area of modal logic, and the theory of display calculi, originated by Belnap. These connections have been seminally observed and exploited by Marcus Kracht, in the context of his characterization of the modal axioms (which he calls primitive formulas) which can be effectively transformed into `analytic' structural rules of display calculi. In this context, a rule is `analytic' if adding it to a display calculus preserves Belnap's cut-elimination theorem. In recent years, the state-of-the-art in correspondence theory has been uniformly extended from classical modal logic to diverse families of nonclassical logics, ranging from (bi-)intuitionistic (modal) logics, linear, relevant and other substructural logics, to hybrid logics and mu-calculi. This generalization has given rise to a theory called unified correspondence, the most important technical tools of which are the algorithm ALBA, and the syntactic characterization of Sahlqvist-type classes of formulas and inequalities which is uniform in the setting of normal DLE-logics (logics the algebraic semantics of which is based on bounded distributive lattices). We apply unified correspondence theory, with its tools and insights, to extend Kracht's results and prove his claims in the setting of DLE-logics. The results of the present paper characterize the space of properly displayable DLE-logics.
We present a tool for reasoning in and about propositional sequent calculi. One aim is to support reasoning in calculi that contain a hundred rules or more, so that even relatively small pen and paper derivations become tedious and error prone. As an example, we implement the display calculus D.EAK of dynamic epistemic logic. Second, we provide embeddings of the calculus in the theorem prover Isabelle for formalising proofs about D.EAK. As a case study we show that the solution of the muddy children puzzle is derivable for any number of muddy children. Third, there is a set of meta-tools, that allows us to adapt the tool for a wide variety of user defined calculi.
We present the statistical analysis of the properties of gamma-ray bursts with measured host galaxy redshifts and peaked optical light curves in proper frames of reference. The optical transients are classified by comparing the time lag of the optical peak relative to the GRB trigger with the duration of the gamma-ray emission itself. The results of the correlation analysis of all possible pairs of energy, spectral, and temporal characteristics of both gamma-ray and optical emissions are given. We specify the pairs of the parameters with correlation coefficients greater than 50 % at significance levels better than 1 %. The following empirical relations, obtained for the first time, are specifically discussed: a correlation between the peak optical afterglow $R$ band luminosity and redshift $L_{R} \propto (z+1)^{5.39 \pm 0.74}$ and a correlation between the peak luminosity of the prompt optical emissions and the time of the peak $L_{R} \propto T_{\rm peak}^{-3.85 \pm 1.22}$. We also analyze the similarity of the relationships between the peak optical luminosity and the isotropic equivalent of the total energy of gamma-ray bursts for afterglows ($L_{R} \propto E_{\rm iso}^{1.06 \pm 0.22}$) and for prompt optical emissions ($L_{R} \propto E_{\rm iso}^{1.59 \pm 0.21}$).
We report on multi-wavelength observations, ranging from the X-ray to radio wave bands, of the IPN-localized gamma-ray burst GRB 070125. Spectroscopic observations reveal the presence of absorption lines due to O I, Si II, and C IV, implying a likely redshift of z = 1.547. The well-sampled light curves, in particular from 0.5 to 4 days after the burst, suggest a jet break at 3.7 days, corresponding to a jet opening angle of ~7.0 degrees, and implying an intrinsic GRB energy in the 1 - 10,000 keV band of around E = (6.3 - 6.9)x 10^(51) erg (based on the fluences measured by the gamma-ray detectors of the IPN network). GRB 070125 is among the brightest afterglows observed to date. The spectral energy distribution implies a host extinction of Av < 0.9 mag. Two rebrightening episodes are observed, one with excellent time coverage, showing an increase in flux of 56% in ~8000 seconds. The evolution of the afterglow light curve is achromatic at all times. Late-time observations of the afterglow do not show evidence for emission from an underlying host galaxy or supernova. Any host galaxy would be subluminous, consistent with current GRB host-galaxy samples. Evidence for strong Mg II absorption features is not found, which is perhaps surprising in view of the relatively high redshift of this burst and the high likelihood for such features along GRB-selected lines of sight.