Showing 1–50 of 79 results for author: Oliva, P

Acceleration and radiation: Classical and quantum aspects

Authors: Felipe Ignacio Portales Oliva

Abstract: It has been known for some time that the classical concept of radiation is not covariant: for uniformly accelerated particles, it depends on the state of motion of the observer relative to the particle emitting it. Moreover, recent literature in the field of Quantum Field Theory in Curved Spacetimes suggests a deep connection between bremsstrahlung and the Unruh effect, where zero-Rindler energy p… ▽ More It has been known for some time that the classical concept of radiation is not covariant: for uniformly accelerated particles, it depends on the state of motion of the observer relative to the particle emitting it. Moreover, recent literature in the field of Quantum Field Theory in Curved Spacetimes suggests a deep connection between bremsstrahlung and the Unruh effect, where zero-Rindler energy particles have played a central role beyond constructing the radiation contents of systems; as this is an unfamiliar concept, it seems unsettling to deal with particles having no energy. This thesis studies such a connection in both the classical and quantum perspectives, showing how the quantum Unruh effect is responsible for the classical radiation detected for the electric and gravitational cases, and studies the role of zero-Rindler-energy particles and how they relate to the radiative field of uniformly accelerated particles. △ Less

Submitted 25 June, 2024; originally announced June 2024.

Comments: PhD thesis presented at Federal University of ABC (UFABC), Brazil; supervised by A. G. S. Landulfo. 119 pages, 5 figures, PDFLaTeX

Higher-order Games with Dependent Types

Authors: Martín Escardó, Paulo Oliva

Abstract: In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point.… ▽ More In previous work on higher-order games, we accounted for finite games of unbounded length by working with continuous outcome functions, which carry implicit game trees. In this work we make such trees explicit. We use concepts from dependent type theory to capture history-dependent games, where the set of available moves at a given position in the game depends on the moves played up to that point. In particular, games are modelled by a W-type, which is essentially the same type used by Aczel to model constructive Zermelo-Frankel set theory (CZF). We have also implemented all our definitions, constructions, results and proofs in the dependently-typed programming language Agda, which, in particular, allows us to run concrete examples of computations of optimal strategies, that is, strategies in subgame perfect equilibrium. △ Less

Submitted 7 July, 2023; v1 submitted 15 December, 2022; originally announced December 2022.

Comments: 20 pages

MSC Class: 91A40; 91A18; 03B15; 03F10 ACM Class: F.4.1

Towards fast weak adversarial training to solve high dimensional parabolic partial differential equations using XNODE-WAN

Authors: Paul Valsecchi Oliva, Yue Wu, Cuiyu He, Hao Ni

Abstract: Due to the curse of dimensionality, solving high dimensional parabolic partial differential equations (PDEs) has been a challenging problem for decades. Recently, a weak adversarial network (WAN) proposed in (Y.Zang et al., 2020) offered a flexible and computationally efficient approach to tackle this problem defined on arbitrary domains by leveraging the weak solution. WAN reformulates the PDE pr… ▽ More Due to the curse of dimensionality, solving high dimensional parabolic partial differential equations (PDEs) has been a challenging problem for decades. Recently, a weak adversarial network (WAN) proposed in (Y.Zang et al., 2020) offered a flexible and computationally efficient approach to tackle this problem defined on arbitrary domains by leveraging the weak solution. WAN reformulates the PDE problem as a generative adversarial network, where the weak solution (primal network) and the test function (adversarial network) are parameterized by the multi-layer deep neural networks (DNNs). However, it is not yet clear whether DNNs are the most effective model for the parabolic PDE solutions as they do not take into account the fundamentally different roles played by time and spatial variables in the solution. To reinforce the difference, we design a novel so-called XNODE model for the primal network, which is built on the neural ODE (NODE) model with additional spatial dependency to incorporate the a priori information of the PDEs and serve as a universal and effective approximation to the solution. The proposed hybrid method (XNODE-WAN), by integrating the XNODE model within the WAN framework, leads to significant improvement in the performance and efficiency of training. Numerical results show that our method can reduce the training time to a fraction of that of the WAN model. △ Less

Submitted 14 October, 2021; originally announced October 2021.

Comments: 35 pages, 7 figures

MSC Class: 65N99 65M99

Quantification of pulmonary involvement in COVID-19 pneumonia by means of a cascade oftwo U-nets: training and assessment on multipledatasets using different annotation criteria

Authors: Francesca Lizzi, Abramo Agosti, Francesca Brero, Raffaella Fiamma Cabini, Maria Evelina Fantacci, Silvia Figini, Alessandro Lascialfari, Francesco Laruina, Piernicola Oliva, Stefano Piffer, Ian Postuma, Lisa Rinaldi, Cinzia Talamonti, Alessandra Retico

Abstract: The automatic assignment of a severity score to the CT scans of patients affected by COVID-19 pneumonia could reduce the workload in radiology departments. This study aims at exploiting Artificial intelligence (AI) for the identification, segmentation and quantification of COVID-19 pulmonary lesions. We investigated the effects of using multiple datasets, heterogeneously populated and annotated ac… ▽ More The automatic assignment of a severity score to the CT scans of patients affected by COVID-19 pneumonia could reduce the workload in radiology departments. This study aims at exploiting Artificial intelligence (AI) for the identification, segmentation and quantification of COVID-19 pulmonary lesions. We investigated the effects of using multiple datasets, heterogeneously populated and annotated according to different criteria. We developed an automated analysis pipeline, the LungQuant system, based on a cascade of two U-nets. The first one (U-net_1) is devoted to the identification of the lung parenchyma, the second one (U-net_2) acts on a bounding box enclosing the segmented lungs to identify the areas affected by COVID-19 lesions. Different public datasets were used to train the U-nets and to evaluate their segmentation performances, which have been quantified in terms of the Dice index. The accuracy in predicting the CT-Severity Score (CT-SS) of the LungQuant system has been also evaluated. Both Dice and accuracy showed a dependency on the quality of annotations of the available data samples. On an independent and publicly available benchmark dataset, the Dice values measured between the masks predicted by LungQuant system and the reference ones were 0.95$\pm$0.01 and 0.66$\pm$0.13 for the segmentation of lungs and COVID-19 lesions, respectively. The accuracy of 90% in the identification of the CT-SS on this benchmark dataset was achieved. We analysed the impact of using data samples with different annotation criteria in training an AI-based quantification system for pulmonary involvement in COVID-19 pneumonia. In terms of the Dice index, the U-net segmentation quality strongly depends on the quality of the lesion annotations. Nevertheless, the CT-SS can be accurately predicted on independent validation sets, demonstrating the satisfactory generalization ability of the LungQuant. △ Less

Submitted 6 May, 2021; originally announced May 2021.

On the Borel-Cantelli Lemmas, the Erdős-Rényi Theorem, and the Kochen-Stone Theorem

Authors: Rob Arthan, Paulo Oliva

Abstract: In this paper we present a quantitative analysis of the first and second Borel-Cantelli Lemmas and of two of their generalisations: the Erdős-Rényi Theorem, and the Kochen-Stone Theorem. We will see that the first three results have direct quantitative formulations, giving an explicit relationship between quantitative formulations of the assumptions and the conclusion. For the Kochen-Stone theorem… ▽ More In this paper we present a quantitative analysis of the first and second Borel-Cantelli Lemmas and of two of their generalisations: the Erdős-Rényi Theorem, and the Kochen-Stone Theorem. We will see that the first three results have direct quantitative formulations, giving an explicit relationship between quantitative formulations of the assumptions and the conclusion. For the Kochen-Stone theorem, however, we can show that the numerical bounds of a direct quantitative formulation are not computable in general. Nonetheless, we obtain a quantitative formulation of the Kochen-Stone Theorem using Tao's notion of metastability. △ Less

Submitted 15 December, 2021; v1 submitted 17 December, 2020; originally announced December 2020.

Comments: 22 pages

MSC Class: 60A10; 60F20; 03F60

Parametrised Functional Interpretations

Authors: Bruno Dinis, Paulo Oliva

Abstract: This paper presents a general framework for unifying functional interpretations. It is based on families of parameters allowing for different degrees of freedom on the design of the interpretation. In this way we are able to generalise previous work on unifying functional interpretations, by including in the unification the more recent bounded and Herbrandized functional interpretations. This paper presents a general framework for unifying functional interpretations. It is based on families of parameters allowing for different degrees of freedom on the design of the interpretation. In this way we are able to generalise previous work on unifying functional interpretations, by including in the unification the more recent bounded and Herbrandized functional interpretations. △ Less

Submitted 12 May, 2020; originally announced May 2020.

MSC Class: 03F07 and 03F10 and 03F30 and 03F55

On the Herbrand Functional Interpretation

Authors: Paulo Oliva, Chuangjie Xu

Abstract: We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigatio… ▽ More We show that the types of the witnesses in the Herbrand functional interpretation can be simplified, avoiding the use of "sets of functionals" in the interpretation of implication and universal quantification. This is done by presenting an alternative formulation of the Herbrand functional interpretation, which we show to be equivalent to the original presentation. As a result of this investigation we also strengthen the monotonicity property of the original presentation, and prove a monotonicity property for our alternative definition. △ Less

Submitted 3 December, 2019; originally announced December 2019.

Comments: 9 pages

MSC Class: 26E35; 11U10; 03F25

Negative Translations for Affine and Lukasiewicz Logic

Authors: Rob Arthan, Paulo Oliva

Abstract: We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in affine logic the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend af… ▽ More We investigate four well-known negative translations of classical logic into intuitionistic logic within a substructural setting. We find that in affine logic the translation schemes due to Kolmogorov and Gödel both satisfy Troelstra's criteria for a negative translation. On the other hand, the schemes of Glivenko and Gentzen both fail for affine logic, but for different reasons: one can extend affine logic to make Glivenko work and Gentzen fail and vice versa. By contrast, in the setting of Lukasiewicz logic, we can prove a general result asserting that a wide class of formula translations including those of Kolmogorov, Gödel, Gentzen and Glivenko not only satisfy Troelstra's criteria with respect to a natural intuitionistic fragment of Lukasiewicz logic but are all equivalent. △ Less

Submitted 29 November, 2019; originally announced December 2019.

Comments: arXiv admin note: text overlap with arXiv:1404.0570

MSC Class: 03B47; 03B35; 03F03; 03F52 ACM Class: F.4.1

A charming ICECUBE discover?

Authors: D. Fargion, P. G. De Sanctis Lucentini, M. Yu. Khlopov, P. Oliva, F. La Monaca, P. Paggi

Abstract: Last two years high energy neutrino data are studied. The two recent tau neutrino double bang candidate are discussed within their detectability, noise and expected rate. The neutrino flavor distribution mainly favoring equal electron and muon presence, is reminded. The angular distribution of highest muon neutrino tracks is analyzed. Their horizontal strong anisotropy and their remarkable up-down… ▽ More Last two years high energy neutrino data are studied. The two recent tau neutrino double bang candidate are discussed within their detectability, noise and expected rate. The neutrino flavor distribution mainly favoring equal electron and muon presence, is reminded. The angular distribution of highest muon neutrino tracks is analyzed. Their horizontal strong anisotropy and their remarkable up-down asymmetry, with the absence of clustering, is noticed. The main persistent missing of astrophysical X,gamma sources (as GRB and AGN flaring source) and all the above signatures led us to suggest a dominance of prompt charmed (atmospheric) events able to pollute, to smear and to hide any minor astronomical presence. △ Less

Submitted 17 November, 2019; originally announced November 2019.

Comments: 15 pages, 4 figures, updated minimaized version, from earlier arxiv.longhoe.net/abs/1808.10493v4; Volume 331, Frontier Research in Astrophysics, III (FRAPWS2018)

Report number: PoS(FRAPWS2018)007

Journal ref: Proceeding of Science , 2019

Studying Algebraic Structures using Prover9 and Mace4

Authors: Rob Arthan, Paulo Oliva

Abstract: In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator in the investigation of a class of algebraic structures. We will see that these tools, when combined with human insight and traditional algebraic methods, help us to explore the problem space quickly and effectively. The… ▽ More In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator in the investigation of a class of algebraic structures. We will see that these tools, when combined with human insight and traditional algebraic methods, help us to explore the problem space quickly and effectively. The counter-example generator rapidly rules out many false conjectures, while the theorem prover is often much more efficient than a human being at verifying algebraic identities. The specific tools in our case study are Prover9 and Mace4; the algebraic structures are generalisations of Heyting algebras known as hoops. We will see how this approach helped us to discover new theorems and to find new or improved proofs of known results. We also make some suggestions for how one might deploy these tools to supplement a more conventional approach to teaching algebra. △ Less

Submitted 14 August, 2019; originally announced August 2019.

Comments: 21 pages, to appear as Chapter 5 in "Proof Technology in Mathematics Research and Teaching", Mathematics Education in the Digital Era 14, edited by G. Hanna et al. (eds.), published by Springer

Sorting and filtering as effective rational choice procedures

Authors: Paulo Oliva, Philipp Zahn

Abstract: Many online shops offer functionality that help their customers navigate the available alternatives. For instance, options to filter and to sort goods are wide-spread. In this paper we show that sorting and filtering can be used by rational consumers to find their most preferred choice -- quickly. We characterize the preferences which can be expressed through filtering and sorting and show that th… ▽ More Many online shops offer functionality that help their customers navigate the available alternatives. For instance, options to filter and to sort goods are wide-spread. In this paper we show that sorting and filtering can be used by rational consumers to find their most preferred choice -- quickly. We characterize the preferences which can be expressed through filtering and sorting and show that these preferences exhibit a simple and intuitive logical structure. △ Less

Submitted 9 September, 2021; v1 submitted 18 September, 2018; originally announced September 2018.

A Curry-Howard Correspondence for the Minimal Fragment of Łukasiewicz Logic

Authors: Rob Arthan, Paulo Oliva

Abstract: In this paper we introduce a term calculus ${\cal B}$ which adds to the affine $λ$-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between ${\cal B}$ and the sub-structural logical system which we call "minimal Łukasiewicz logic", also known in the literature as the logic of hoops (a generalisation of MV-algebras). This l… ▽ More In this paper we introduce a term calculus ${\cal B}$ which adds to the affine $λ$-calculus with pairing a new construct allowing for a restricted form of contraction. We obtain a Curry-Howard correspondence between ${\cal B}$ and the sub-structural logical system which we call "minimal Łukasiewicz logic", also known in the literature as the logic of hoops (a generalisation of MV-algebras). This logic lies strictly in between affine minimal logic and standard minimal logic. We prove that ${\cal B}$ is strongly normalising and has the Church-Rosser property. We also give examples of terms in ${\cal B}$ corresponding to some important derivations from our work and the literature. Finally, we discuss the relation between normalisation in ${\cal B}$ and cut-elimination for a Gentzen-style formulation of minimal Łukasiewicz logic. △ Less

Submitted 12 September, 2018; originally announced September 2018.

Comments: 17 pages

MSC Class: 03B15; 03B50; 03B40; 68N18; 03B47; 03F52; 03B20; 03B70

Solar neutrino flare, megaton neutrino detectors and human space journey

Authors: Daniele Fargion, Pietro Oliva, P. G. De Sanctis Lucentini, Silvia Pietroni, Fabio La Monaca, Paolo Paggi, Emanuele Habib, Maxim Yu. Khlopov

Abstract: The largest solar flare have been recorded in gamma flash and hard spectra up to tens GeV energy. The present building and upgrade of Hyper- Kamiokande (HK) in Japan and Korea, (as well as Deep Core, PINGU) Megatons neutrino detectors do offer a novel way to detectable trace of solar flares: their sudden anti-neutrino (or neutrino) imprint made by proton scattering and pion decays via Delta resona… ▽ More The largest solar flare have been recorded in gamma flash and hard spectra up to tens GeV energy. The present building and upgrade of Hyper- Kamiokande (HK) in Japan and Korea, (as well as Deep Core, PINGU) Megatons neutrino detectors do offer a novel way to detectable trace of solar flares: their sudden anti-neutrino (or neutrino) imprint made by proton scattering and pion decays via Delta resonance production on solar corona foot-point. These signals might be observable at largest flare by HK via soft spectra up to tens-hundred MeV energy and by IceCube-PINGU at higher, GeVs energies. We show the expected rate of signals for the most powerful solar flare occurred in recent decades extrapolated for future Megaton detectors. The neutrino solar flare detection with its prompt alarm system may alert astronauts on space journey allowing them to hide themselves into inner rocket container surrounded by fuel or water supply. These container walls are able to defend astronauts from the main lethal (the dominant soft component) radiation wind due to such largest solar flares. △ Less

Submitted 18 November, 2018; v1 submitted 6 September, 2018; originally announced September 2018.

Comments: 15 pages, 12 figures

No guaranteed neutrino astronomy without (enough) double bang tau and downward HESE muon tracks: An update version

Authors: D. Fargion, P. G. De Sanctis Lucentini, M. Yu. Khlopov, P. Oliva, F. La Monaca, P. Paggi

Abstract: IceCube Neutrino Astronomy is considered. The tau neutrino flavor paucity and the asymmetry for the tracks suggest a dominant atmospheric charm noise. The correlated cascades and tracks asymmetry with relevant statistics enforce the charm noise dominance in the data. The charm signal may explain at once the absence of correlation for the tracks data with the galactic plane and with known brightest… ▽ More IceCube Neutrino Astronomy is considered. The tau neutrino flavor paucity and the asymmetry for the tracks suggest a dominant atmospheric charm noise. The correlated cascades and tracks asymmetry with relevant statistics enforce the charm noise dominance in the data. The charm signal may explain at once the absence of correlation for the tracks data with the galactic plane and with known brightest gamma sources. △ Less

Submitted 28 October, 2019; v1 submitted 30 August, 2018; originally announced August 2018.

Comments: 16 pages, 4 figure , Questions and Discussion; new sections and new updated arguments

On Rational Choice and the Representation of Decision Problems

Authors: Paulo Oliva, Philipp Zahn

Abstract: In economic theory, an agent chooses from available alternatives -- modeled as a set. In decisions in the field or in the lab, however, agents do not have access to the set of alternatives at once. Instead, alternatives are represented by the outside world in a structured way. Online search results are lists of items, wine menus are often lists of lists (grouped by type or country), and online sho… ▽ More In economic theory, an agent chooses from available alternatives -- modeled as a set. In decisions in the field or in the lab, however, agents do not have access to the set of alternatives at once. Instead, alternatives are represented by the outside world in a structured way. Online search results are lists of items, wine menus are often lists of lists (grouped by type or country), and online shop** often involves filtering items which can be viewed as navigating a tree. Representations constrain how an agent can choose. At the same time, an agent can also leverage representations when choosing, simplifying his/her choice process. For instance, in the case of a list he or she can use the order in which alternatives are represented to make his/her choice. In this paper, we model representations and decision procedures operating on them. We show that choice procedures are related to classical choice functions by a canonical map**. Using this map**, we can ask whether properties of choice functions can be lifted onto the choice procedures which induce them. We focus on the obvious benchmark: rational choice. We fully characterize choice procedures which can be rationalized by a strict preference relation for general representations including lists, list of lists, trees and others. Our framework can thereby be used as the basis for new tests of rational behavior. Classical choice theory operates on very limited information, typically budgets or menus and final choices. This is in stark contrast to the vast amount of data that specifically web companies collect about their users' choice process. Our framework offers a way to integrate such data into economic choice models. △ Less

Submitted 8 November, 2021; v1 submitted 10 January, 2018; originally announced January 2018.

Could GRB170817A be really correlated to a NS-NS merging?

Authors: Daniele Fargion, Maxim Khlopov, Pietro Oliva

Abstract: The exciting development of gravitational wave (GW) astronomy in the correlation of LIGO and VIRGO detection of GW signals makes possible to expect registration of effects of not only Binary Black Hole (BH) coalescence, but also Binary Neutron Star (NS) merging accompanied by electromagnetic (GRB) signal. Here we consider the possibility that a Neutron Star (NS), merging in a NS-NS or NS-BH system… ▽ More The exciting development of gravitational wave (GW) astronomy in the correlation of LIGO and VIRGO detection of GW signals makes possible to expect registration of effects of not only Binary Black Hole (BH) coalescence, but also Binary Neutron Star (NS) merging accompanied by electromagnetic (GRB) signal. Here we consider the possibility that a Neutron Star (NS), merging in a NS-NS or NS-BH system might be (soon) observed in correlation with any LIGO-VIRGO Gravitational Waves detection. We analyze as an example the recent case of the short GRB 170817A observed by Fermi and Integral. The associated Optical transient OT source in NGC4993 imply a rare near source, a consequent averaged large rate of such events (almost) compatible with expected NS NS merging rate. However the expected beamed GRB (or Short GRB) may be mostly aligned to a different direction than our. Therefore even soft GRB photons, more spread than hard ones, might be hardly able to shower to us. Nevertheless a prompt spiraling electron turbine jet in largest magnetic fields, at the base of the NS-NS collapse, might shine by its tangential synchrotron radiation in spread way with its skimming photons shining in large open disk. The consequent solid angle for such soft disk gamma radiation may be large enough to be nevertheless often observed. △ Less

Submitted 13 October, 2017; originally announced October 2017.

Comments: 12 pages, 12 figures

Journal ref: Int. J. Mod. Phys. D, 4 December, 2017

Observing future Solar Flare Neutrino in Hyper-KamioKande in Japan, Korea and in IceCube

Authors: Daniele Fargion, Pietro Oliva

Abstract: The largest Solar flare have been recorded in gamma flash and hard spectra up to tens GeV energy. The present building and upgrade of Hyper-Kamiokande (HK) and IceCube (as well as Deep Core, PINGU) neutrino detectors do offer a novel way to largest trace of solar Flare: their sudden anti-neutrino (or neutrino) flare made by proton scattering and pion decays via Delta resonance production. These si… ▽ More The largest Solar flare have been recorded in gamma flash and hard spectra up to tens GeV energy. The present building and upgrade of Hyper-Kamiokande (HK) and IceCube (as well as Deep Core, PINGU) neutrino detectors do offer a novel way to largest trace of solar Flare: their sudden anti-neutrino (or neutrino) flare made by proton scattering and pion decays via Delta resonance production. These signals might be observable at largest flare by HK via soft spectra up to tens- hundred MeV energy and by IceCube-PINGU at higher, GeV up to hundred GeV, energies. We show the expected rate of signals for the most powerful solar flare occurred in recent decades. △ Less

Submitted 6 July, 2017; originally announced July 2017.

Comments: 5 pages, 4 figures, ICRC 2017

No Tau? No Astronomy!

Authors: Daniele Fargion, Pietro Oliva

Abstract: Since 2013 IceCube cascade showers sudden overabundance have shown a fast flavor change above 30-60 TeV up to PeV energy. This flavor change from dominant muon tracks at TeVs to shower events at higher energies, has been indebted to a new injection of a neutrino astronomy. However the recent published 54 neutrino HESE, high energy starting events, as well as the 38 external muon tracks made by tro… ▽ More Since 2013 IceCube cascade showers sudden overabundance have shown a fast flavor change above 30-60 TeV up to PeV energy. This flavor change from dominant muon tracks at TeVs to shower events at higher energies, has been indebted to a new injection of a neutrino astronomy. However the recent published 54 neutrino HESE, high energy starting events, as well as the 38 external muon tracks made by trough going muon formed around the IceCube, none of them are pointing to any expected X-gamma or radio sources: no one in connection to GRB, no toward active BL Lac, neither to AGN source in Fermi catalog. No clear correlation with nearby mass distribution (Local Group), nor to galactic plane. Moreover there have not been any record (among a dozen of 200 TeV energetic events) of the expected double bang due to the tau neutrino birth and decay. An amazing and surprising unfair distribution in flavor versus expected democratic one. Finally there is not a complete consistence of the internal HESE event spectra and the external crossing muon track ones. Moreover the apparent sudden astrophysical neutrino flux rise at 60 TeV might be probably also suddenly cut at a few PeV in order to hide the (unobserved , yet) Glashow resonance peak at 6.3 PeV. A more mondane prompt charmed atmospheric neutrino component may explain most of the IceCube puzzles. If this near future, 2017-2018, it does not shine tau neutrino signals somewhere (by tau airshowers in AUGER, TA, ASHRA or double bang in IceCube) there are a list of consequences to face. These missing correlations and in particular the tau signature absence force us to claim : No Tau? No neutrino Astronomy. △ Less

Submitted 13 July, 2017; v1 submitted 6 July, 2017; originally announced July 2017.

Comments: 7 pages, 4 figures, ICRC 2017; additional minor misprint corrections

Signals of HE atmospheric muon decay in flight around the Sun's albedo versus astrophysical muon and tau neutrino traces in the Moon's shadow

Authors: Daniele Fargion, Pietro Oliva, Pier Giorgio De Sanctis Lucentini, Maxim Yu. Khlopov

Abstract: The Sun albedo of cosmic rays at GeVs energy has been discovered recently by FERMI satellite. They are traces of atmospheric CR hitting solar atmosphere and reflecting skimming gamma photons. Even if relevant for astrophysics, as being trace of atmospheric solar Cosmic Ray noises they cannot offer any signal of neutrino astronomy. On the contrary the Moon, with no atmosphere, may become soon a nov… ▽ More The Sun albedo of cosmic rays at GeVs energy has been discovered recently by FERMI satellite. They are traces of atmospheric CR hitting solar atmosphere and reflecting skimming gamma photons. Even if relevant for astrophysics, as being trace of atmospheric solar Cosmic Ray noises they cannot offer any signal of neutrino astronomy. On the contrary the Moon, with no atmosphere, may become soon a novel filtering calorimeter and an amplifier of energetic muon astronomical neutrinos (at TeV up to hundred TeV energy); these lepton tracks leave an imprint in their beta decay while in flight to Earth. Their TeV electron air-shower are among the main signals. Also a more energetic, but more rare, PeV up to EeV tau lunar neutrino events may be esca** as a tau lepton from the Moon: PeVs secondaries may be shining on Earth atmosphere in lunar shadows in a surprising rich way. One or a few gamma air-shower event inside the Moon shadows may occur each year in near future CTA or LHAASO TeVs gamma array detector, assuming a non negligible astrophysical TeV up to hundred TeV neutrino component (respect to our terrestrial ruling atmospheric ones); these signals will open a new wonderful passepartout keyhole for neutrino been seen along the Moon. The lunar solid angle is small and the muon or tau expected rate is rare, but future largest tau radio array as GRAND one might well discover such neutrino imprint. △ Less

Submitted 1 November, 2017; v1 submitted 28 June, 2017; originally announced June 2017.

Comments: 15 pages, 2 figures

Uncorrelated far AGN flaring with their delayed UHECRs events

Authors: D. Fargion, P. Oliva, Pier Giorgio De Sanctis Lucentini

Abstract: The most distant AGN, within the allowed GZK cut-off radius, have been recently candidate by many authors as the best location for observed UHECR origination. Indeed, the apparent homogeneity and isotropy of recent UHECR signals seems to require a far cosmic isotropic and homogeneous scenario involving a proton UHECR courier: our galaxy or nearest local group or super galactic plane (ruled by Virg… ▽ More The most distant AGN, within the allowed GZK cut-off radius, have been recently candidate by many authors as the best location for observed UHECR origination. Indeed, the apparent homogeneity and isotropy of recent UHECR signals seems to require a far cosmic isotropic and homogeneous scenario involving a proton UHECR courier: our galaxy or nearest local group or super galactic plane (ruled by Virgo cluster) are too much near and apparently too much anisotropic in disagreement with PAO and TA almost homogeneous sample data. However, the few and mild observed UHECR clustering, the North and South Hot Spots, are smeared in wide solid angles. Their consequent random walk flight from most far GZK UHECR sources, nearly at 100 Mpc, must be delayed (with respect to a straight AGN photon gamma flaring arrival trajectory) at least by a million years. During this time, the AGN jet blazing signal, its probable axis deflection (such as the helical jet in Mrk501), its miss alignment or even its almost certain exhaust activity may lead to a complete misleading correlation between present UHECR events and a much earlier active AGN ejection. UHECR maps maybe anyway related to galactic or nearest (Cen A, M82) AGN extragalactic UHECR sources shining in twin Hot Spot. Therefore we defend our (quite different) scenarios where UHECR are mostly made by lightest UHECR nuclei originated by nearby AGN sources, or few galactic sources, whose delayed signals reach us within few thousand years in the observed smeared sky areas. △ Less

Submitted 7 May, 2017; v1 submitted 31 March, 2017; originally announced March 2017.

Comments: 13 pages, 10 figures, minor editorial corrections, in press, JPS Conference Proceedings Vol. 9 (published on April 6, 2016) JPS Conference Proceedings,Proceedings of International Symposium for Ultra-High Energy Cosmic Rays October 2016, (UHECR2016)

Report number: Proc. 2016 Int. Conf. Ultra-High Energy Cosmic Rays (UHECR2016)

2013-2016 review: HE Neutrino and UHECR Astronomy?

Authors: D. Fargion, P. Oliva

Abstract: The last few years, 2013-2016, the high energy neutrino events in ICECUBE and the last rich UHECR maps by AUGER and TA were hopefully opening a new High Energy astronomy age. Unfortunately the foreseen correlation between neutrino with best gamma X sources has not (yet) been found. The most celebrated GRB gamma sources do not correlate to any neutrino events. The expected Local Group anisotropy in… ▽ More The last few years, 2013-2016, the high energy neutrino events in ICECUBE and the last rich UHECR maps by AUGER and TA were hopefully opening a new High Energy astronomy age. Unfortunately the foreseen correlation between neutrino with best gamma X sources has not (yet) been found. The most celebrated GRB gamma sources do not correlate to any neutrino events. The expected Local Group anisotropy in UHECR within the nuleon GZK cut off, has just fade away. UHECR events from Virgo are almost absent. Above two hundred TeV energy tau neutrino might shine by double bang in detectable way in ICECUBE. Within a dozen of events no tau neutrino arised (yet) in ICECUBE. Finally GRBs Fireball models calling since decades for HE neutrinos correlated imprint at TeVs energy are not (yet) found. So many absences are making a huge question mark: is there a new reading key? △ Less

Submitted 31 January, 2017; originally announced February 2017.

UHECR narrow clustering correlating IceCube through-going muons

Authors: Daniele Fargion, Pietro Oliva, Pier Giorgio De Sanctis Lucentini, Daniele D Armiento, Paolo Paggi

Abstract: The recent UHECR events by AUGER and the Telescope Array (TA) suggested that wide clusterings as the North and South, named Hot Spot, are related to near AGNs such as the one in M82 and Cen A. In the same frame since 2008 we assumed that the UHECR are made by light and lightest nuclei to explain the otherwise embarrassing absence of the huge nearby Virgo cluster, absence due to the fragility and t… ▽ More The recent UHECR events by AUGER and the Telescope Array (TA) suggested that wide clusterings as the North and South, named Hot Spot, are related to near AGNs such as the one in M82 and Cen A. In the same frame since 2008 we assumed that the UHECR are made by light and lightest nuclei to explain the otherwise embarrassing absence of the huge nearby Virgo cluster, absence due to the fragility and the opacity of lightest nuclei by photo-dissociation from Virgo distances. Moreover UHECR map exhibits a few narrow clustering, some near the galactic plane, as toward SS 433 and on the opposite side of the plane at celestial horizons: we tagged them in 2014 suggesting possible near source active also as a UHE neutrino. Indeed since last year, 2015, highest IceCube trough-going muons, UHE up-going neutrino events at hundreds TeV energy, did show (by two cases over three tagged in North sky) the expected overlap** of UHE neutrinos signals with narrow crowding UHECR. New data with higher energy threshold somehow re-confirmed our preliminary proposal; new possible sources appear by a additional correlated UHE-neutrino versus UHE-neutrino and-or with narrow UHECR clustering events. A possible role of relic neutrino mass scattering by ZeV neutrino arised. △ Less

Submitted 31 October, 2016; originally announced November 2016.

Comments: 6 pages, 5 figures

Report number: Nuclear and Particle Physics Proceedings Volumes 291--293, Pages 195-200

Journal ref: Nuclear and Particle Physics Proceedings, 2017

Fast 3C 279 gamma flares by a merging medium size black hole jet aligned to the AGN one by tidal torque?

Authors: Daniele Fargion, Pietro Oliva

Abstract: The shorter-than-Schwarzschild 3C 279 variability flare on June 2015 is very puzzling. Its nature cannot be due to any NS merging nor to a medium sized (hundred million solar mass) BH collapse. Our preliminary model is based on the long-life (a third of a year) merging of a medium size BH (hundred of solar mass) jet spiralling toward the largest AGN one, (billion solar mass), that is dragging by t… ▽ More The shorter-than-Schwarzschild 3C 279 variability flare on June 2015 is very puzzling. Its nature cannot be due to any NS merging nor to a medium sized (hundred million solar mass) BH collapse. Our preliminary model is based on the long-life (a third of a year) merging of a medium size BH (hundred of solar mass) jet spiralling toward the largest AGN one, (billion solar mass), that is dragging by tidal torques the medium small size BH jet along the main AGN 3C 279 one. The tidal torque is aligning both jets toward Earth. The twin overlap** blazars may offer at once a long and a short scale variability consistent with the surprising Fermi discovers. △ Less

Submitted 22 January, 2017; v1 submitted 30 August, 2016; originally announced August 2016.

Comments: 7 pages, 1 figure, PoS

A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem

Authors: Paulo Oliva, Silvia Steila

Abstract: In 1979 Schwichtenberg showed that the System $\text{T}$ definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels $0$ and $1$. More precisely, if the functional $Y$ which controls the stop** condition of Spector's bar recursor is $\text{T}$-definable, then the corresponding bar recursion of type levels $0$ and $1$ is already $\text{T}$-definable. S… ▽ More In 1979 Schwichtenberg showed that the System $\text{T}$ definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels $0$ and $1$. More precisely, if the functional $Y$ which controls the stop** condition of Spector's bar recursor is $\text{T}$-definable, then the corresponding bar recursion of type levels $0$ and $1$ is already $\text{T}$-definable. Schwichtenberg's original proof, however, relies on a detour through Tait's infinitary terms and the correspondence between ordinal recursion for $α< \varepsilon_0$ and primitive recursion over finite types. This detour makes it hard to calculate on given concrete system $\text{T}$ input, what the corresponding system $\text{T}$ output would look like. In this paper we present an alternative (more direct) proof based on an explicit construction which we prove correct via a suitably defined logical relation. We show through an example how this gives a straightforward mechanism for converting bar recursive definitions into $\text{T}$-definitions under the conditions of Schwichtenberg's theorem. Finally, with the explicit construction we can also easily state a sharper result: if $Y$ is in the fragment $\text{T}_i$ then terms built from $\text{BR}^{\mathbb{N}, σ}$ for this particular $Y$ are definable in the fragment $\text{T}_{i + \max \{ 1, \text{level}σ \} + 2}$. △ Less

Submitted 15 August, 2017; v1 submitted 18 July, 2016; originally announced July 2016.

Comments: 12 pages

MSC Class: 03F07; 03F10

Solving the missing GRB neutrino and GRB-SN puzzles

Authors: Daniele Fargion, Pietro Oliva

Abstract: Every GRB model where the progenitor is assumed to be a highly relativistic hadronic jet whose pions, muons and electron pair secondaries are feeding the gamma jets engine, necessarily (except for very fine-tuned cases) leads to a high average neutrino over photon radiant exposure (radiance), a ratio well above unity, though the present observed average IceCube neutrino radiance is at most compara… ▽ More Every GRB model where the progenitor is assumed to be a highly relativistic hadronic jet whose pions, muons and electron pair secondaries are feeding the gamma jets engine, necessarily (except for very fine-tuned cases) leads to a high average neutrino over photon radiant exposure (radiance), a ratio well above unity, though the present observed average IceCube neutrino radiance is at most comparable to the gamma in the GRB one. Therefore no hadronic GRB, fireball or hadronic thin precessing jet, esca** exploding star in tunneled or penetrarting beam, can fit the actual observations. A new model is shown here, based on a purely electronic progenitor jet, fed by neutrons (and relics) stripped from a neutron star (NS) by tidal forces of a black hole or NS companion, showering into a gamma jet. Such thin precessing spinning jets explain unsolved puzzles such as the existence of the X-ray precursor in many GRBs. The present pure electron jet model, disentangling gamma and (absent) neutrinos, explains naturally why there is no gamma GRB correlates with any simultaneous TeV IceCube astrophysical neutrinos. Rare unstable NS companion stages while feeding the jet may lead to an explosion simulating a SN event. Recent IceCube-160731A highest energy muon neutrino event with absent X-gamma traces confirms the present model expectations. △ Less

Submitted 9 August, 2016; v1 submitted 30 April, 2016; originally announced May 2016.

Comments: 9 pages, 6 Figures

Report number: Volumes 297--299, April--June 2018, Pages 249-258

Journal ref: Nuclear and Particle Physics Proceedings 2018

May GWs signals by BH BH merging be associated with any gamma or neutrino burst? The case of a NS NS merging in GW GRB170817A

Authors: Daniele Fargion, Pier Giorgio De Sanctis Lucentini, Pietro Oliva, Maxim Yu. Khlopov

Abstract: The Gravitational Wave (GW) events GW150914, GW151226, GW170104 detected by LIGO were a record of Black Hole binary merging system (BH-BH) very probably in nearly empty or a vacuum space; such a kind of events will be mostly with no baryon mass (plasma or dense masses) and therefore mute or blind in any correlated gamma band. If the GWs events might be born inside a globular cluster, a star formin… ▽ More The Gravitational Wave (GW) events GW150914, GW151226, GW170104 detected by LIGO were a record of Black Hole binary merging system (BH-BH) very probably in nearly empty or a vacuum space; such a kind of events will be mostly with no baryon mass (plasma or dense masses) and therefore mute or blind in any correlated gamma band. If the GWs events might be born inside a globular cluster, a star forming region or along a spiral AGN accretion disk their additional accreting mass may be the needed baryon load to explode and shine: in those dense places. BH BH collapse may also offer an optical X and gamma afterglow via their baryon lightening and photon tracks. Only very nearby (tens Mpc) BH Neutron Star (NS) or NS NS cannibal merging might be guaranteed and associated also with a desired, visible and correlated spherical NS explosion (kilonova one); they require much lower threshold or just nearer distances. Indeed such a very exceptional GW170817 GRB170817a event occurred last August 2017; it took place and it was related to a very first NS NS collapse in a SN kilonova spherical explosion. The GRB170817a gamma, X, radio signature it was exceptional in many features . Its unique values (softer, weaker, the most near and long life one) made GRB170817a very possibly an off-axis jet detection. However there are solid arguments that suggest that such a GRB are not just blazing within a collimated beam jet but that they are also shining in a wider spread gamma equatorial disk blazing, orthogonal to the jet itself. In a few words we were observing the event not along its jet but mostly orthogonal to it. This GRB170817a geometry may better explain the otherwise unexpected beamed to us event. In this paper therefore we summarize the astrophysical and the cosmological signature of such a long desired multiple astronomy. △ Less

Submitted 12 April, 2018; v1 submitted 31 March, 2016; originally announced March 2016.

Comments: 18 pages, 3 figures; updated text to recent data as GW 170817 and GRB 170817a

Tau Now

Authors: Daniele Fargion, Pietro Oliva

Abstract: UHECR and UHE neutrino map correlation seem to most inconclusive. We show here that a few peculiar UHECR narrow clustering might be connected to a first UHE muon neutrino tracks. Moreover we discuss the best filtered and amplified UHE neutrino astronomy painted by up-going tau airshower. Their discover by new projects could be reached soon. UHECR and UHE neutrino map correlation seem to most inconclusive. We show here that a few peculiar UHECR narrow clustering might be connected to a first UHE muon neutrino tracks. Moreover we discuss the best filtered and amplified UHE neutrino astronomy painted by up-going tau airshower. Their discover by new projects could be reached soon. △ Less

Submitted 10 February, 2016; originally announced February 2016.

Comments: 8 pages, 7 figure

Journal ref: Nuclear and Particle Physics Proceedings, Volumes 279--281, Pages 198--205, 2016

Why not any tau double bang in Icecube, yet?

Authors: D. Fargion, P. Oliva, G. Ucci

Abstract: High Energy Neutrino Astronomy has been revealed by a sudden change in the flavor composition around maximal energies since three years of recording in ice km detector. However these discover didn' t led to any clear promised Neutrino Astronomy land yet. No correlation with hard gamma sources was found. Moreover the astrophysical spectra expected at Fermi value, seem to converge to a softer value,… ▽ More High Energy Neutrino Astronomy has been revealed by a sudden change in the flavor composition around maximal energies since three years of recording in ice km detector. However these discover didn' t led to any clear promised Neutrino Astronomy land yet. No correlation with hard gamma sources was found. Moreover the astrophysical spectra expected at Fermi value, seem to converge to a softer value, also required to avoid any Glashow resonant neutrino signal. We suggest a main solution within a composite flux ruled by prompt atmospheric neutrinos. Nevertheless the recent discover of twentyone crossing muons at hundreds TeVs had shown a first narrow overlapped doublet and a correlated track with a peculiar hard UHECR event clustering pointing to a well known microjet in bynary precession; these first connections hint for a non negligible astrophysical component making neutrino astronomy anyway already more than a hope. △ Less

Submitted 7 January, 2016; v1 submitted 29 December, 2015; originally announced December 2015.

Comments: 11 pages, 3 figures

Report number: C14-05-26.7

Journal ref: PoS FRAPWS2014 (2016) 028, ISSN: 18248039

Higher-Order Decision Theory

Authors: Jules Hedges, Paulo Oliva, Evguenia Sprits, Viktor Winschel, Philipp Zahn

Abstract: Classical decision theory models behaviour in terms of utility maximisation where utilities represent rational preference relations over outcomes. However, empirical evidence and theoretical considerations suggest that we need to go beyond this framework. We propose to represent goals by higher-order functions or operators that take other functions as arguments where the max and argmax operators a… ▽ More Classical decision theory models behaviour in terms of utility maximisation where utilities represent rational preference relations over outcomes. However, empirical evidence and theoretical considerations suggest that we need to go beyond this framework. We propose to represent goals by higher-order functions or operators that take other functions as arguments where the max and argmax operators are special cases. Our higher-order functions take a context function as their argument where a context represents a process from actions to outcomes. By that we can define goals being dependent on the actions and the process in addition to outcomes only. This formulation generalises outcome based preferences to context-dependent goals. We show how to uniformly represent within our higher-order framework classical utility maximisation but also various other extensions that have been debated in economics. △ Less

Submitted 3 June, 2015; v1 submitted 2 June, 2015; originally announced June 2015.

Comments: arXiv admin note: text overlap with arXiv:1409.7411

Higher-Order Game Theory

Authors: Jules Hedges, Paulo Oliva, Evguenia Sprits, Viktor Winschel, Philipp Zahn

Abstract: In applied game theory the motivation of players is a key element. It is encoded in the payoffs of the game form and often based on utility functions. But there are cases were formal descriptions in the form of a utility function do not exist. In this paper we introduce a representation of games where players' goals are modeled based on so-called higher-order functions. Our representation provides… ▽ More In applied game theory the motivation of players is a key element. It is encoded in the payoffs of the game form and often based on utility functions. But there are cases were formal descriptions in the form of a utility function do not exist. In this paper we introduce a representation of games where players' goals are modeled based on so-called higher-order functions. Our representation provides a general and powerful way to mathematically summarize players' intentions. In our framework utility functions as well as preference relations are special cases to describe players' goals. We show that in higher-order functions formal descriptions of players may still exist where utility functions do not using a classical example, a variant of Keynes' beauty contest. We also show that equilibrium conditions based on Nash can be easily adapted to our framework. Lastly, this framework serves as a step** stone to powerful tools from computer science that can be usefully applied to economic game theory in the future such as computational and computability aspects. △ Less

Submitted 3 June, 2015; v1 submitted 2 June, 2015; originally announced June 2015.

Comments: arXiv admin note: substantial text overlap with arXiv:1409.7411

The meaning of the UHECR Hot Spots: A Light Nuclei Nearby Astronomy

Authors: Daniele Fargion, Graziano Ucci, Pietro Oliva, Pier Giorgio De Sanctis Lucentini

Abstract: In this paper we review all the up-to-date Ultra High Energy Cosmic Rays (UHECR) events reported by AUGER, by Telescope Array (TA) and by AGASA in common coordinate maps. We also confirm our earliest (2008-2013) model, where UHECR are mostly made by light nuclei (namely He, Be, B), which explains the Virgo absence and confirms M82 as the main source for North TA Hot Spot. Many more sources, such a… ▽ More In this paper we review all the up-to-date Ultra High Energy Cosmic Rays (UHECR) events reported by AUGER, by Telescope Array (TA) and by AGASA in common coordinate maps. We also confirm our earliest (2008-2013) model, where UHECR are mostly made by light nuclei (namely He, Be, B), which explains the Virgo absence and confirms M82 as the main source for North TA Hot Spot. Many more sources, such as NGC253 and several galactic ones, are possible candidates for most of the 376 UHECR events. Several correlated map, already considered in recent years, are then reported to show all the events, with their statistical correlation values. △ Less

Submitted 5 May, 2015; v1 submitted 4 December, 2014; originally announced December 2014.

Comments: 7 pages, 15 figures. Final version in epj Web Conference

Journal ref: EPJ Web Conf. 99 (2015) 08002; Conference: C14-08-18.1 Proceedings

Spector bar recursion over finite partial functions

Authors: Paulo Oliva, Thomas Powell

Abstract: We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recu… ▽ More We introduce a new, demand-driven variant of Spector's bar recursion in the spirit of the Berardi-Bezem-Coquand functional. The recursion takes place over finite partial functions $u$, where the control parameter $\varphi$, used in Spector's bar recursion to terminate the computation at sequences $s$ satisfying $\varphi(\hat{s})<|s|$, now acts as a guide for deciding exactly where to make bar recursive updates, terminating the computation whenever $\varphi(\hat{u})\in\mbox{dom}(u)$. We begin by exploring theoretical aspects of this new form of recursion, then in the main part of the paper we show that demand-driven bar recursion can be directly used to give an alternative functional interpretation of classical countable choice. We provide a short case study as an illustration, in which we extract a new bar recursive program from the proof that there is no injection from $\mathbb{N}\to\mathbb{N}$ to $\mathbb{N}$, and compare this to the program that would be obtained using Spector's original variant. We conclude by formally establishing that our new bar recursor is primitive recursively equivalent to the original Spector bar recursion, and thus defines the same class of functionals when added to Gödel's system $\sf T$. △ Less

Submitted 17 August, 2015; v1 submitted 23 October, 2014; originally announced October 2014.

Comments: 28 pages

MSC Class: 03D65; 03F03; 03F10; 03F25

Unifying Functional Interpretations: Past and Future

Authors: Paulo Oliva

Abstract: This article surveys work done in the last six years on the unification of various functional interpretations including Gödel's dialectica interpretation, its Diller-Nahm variant, Kreisel modified realizability, Stein's family of functional interpretations, functional interpretations "with truth", and bounded functional interpretations. Our goal in the present paper is twofold: (1) to look back an… ▽ More This article surveys work done in the last six years on the unification of various functional interpretations including Gödel's dialectica interpretation, its Diller-Nahm variant, Kreisel modified realizability, Stein's family of functional interpretations, functional interpretations "with truth", and bounded functional interpretations. Our goal in the present paper is twofold: (1) to look back and single out the main lessons learnt so far, and (2) to look forward and list several open questions and possible directions for further research. △ Less

Submitted 16 October, 2014; originally announced October 2014.

Comments: 18 pages

MSC Class: 03B47; 03F25

The Herbrand Functional Interpretation of the Double Negation Shift

Authors: Martin Escardo, Paulo Oliva

Abstract: This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $T$-selection… ▽ More This paper considers a generalisation of selection functions over an arbitrary strong monad $T$, as functionals of type $J^T_R X = (X \to R) \to T X$. It is assumed throughout that $R$ is a $T$-algebra. We show that $J^T_R$ is also a strong monad, and that it embeds into the continuation monad $K_R X = (X \to R) \to R$. We use this to derive that the explicitly controlled product of $T$-selection functions is definable from the explicitly controlled product of quantifiers, and hence from Spector's bar recursion. We then prove several properties of this product in the special case when $T$ is the finite power set monad ${\mathcal P}(\cdot)$. These are used to show that when $T X = {\mathcal P}(X)$ the explicitly controlled product of $T$-selection functions calculates a witness to the Herbrand functional interpretation of the double negation shift. △ Less

Submitted 19 October, 2015; v1 submitted 16 October, 2014; originally announced October 2014.

Comments: 18 pages

MSC Class: 03E25; 03F10; 03F25

A Higher-order Framework for Decision Problems and Games

Authors: Jules Hedges, Paulo Oliva, Evguenia Winschel, Viktor Winschel, Philipp Zahn

Abstract: We introduce a new unified framework for modelling both decision problems and finite games based on quantifiers and selection functions. We show that the canonical utility maximisation is one special case of a quantifier and that our more abstract framework provides several additional degrees of freedom in modelling. In particular, incomplete preferences, non-maximising heuristics, and context-dep… ▽ More We introduce a new unified framework for modelling both decision problems and finite games based on quantifiers and selection functions. We show that the canonical utility maximisation is one special case of a quantifier and that our more abstract framework provides several additional degrees of freedom in modelling. In particular, incomplete preferences, non-maximising heuristics, and context-dependent motives can be taken into account when describing an agent's goal. We introduce a suitable generalisation of Nash equilibrium for games in terms of quantifiers and selection functions. Moreover, we introduce a refinement of Nash that captures context-dependency of goals. Modelling in our framework is compositional as the parts of the game are modular and can be easily exchanged. We provide an extended example where we illustrate concepts and highlight the benefits of our alternative modelling approach. △ Less

Submitted 25 September, 2014; originally announced September 2014.

Comments: 45 pages

Proceedings Fifth International Workshop on Classical Logic and Computation

Authors: Paulo Oliva

Abstract: Classical Logic and Computation (CL&C) 2014 is the fifth edition of this workshop series. The workshop series intends to cover all work aiming to explore computational aspects of classical logic and mathematics. Its focus is on the exploration of the computational content of mathematical and logical principles, aiming to bring together researchers from both fields and exchange ideas. In this fifth… ▽ More Classical Logic and Computation (CL&C) 2014 is the fifth edition of this workshop series. The workshop series intends to cover all work aiming to explore computational aspects of classical logic and mathematics. Its focus is on the exploration of the computational content of mathematical and logical principles, aiming to bring together researchers from both fields and exchange ideas. In this fifth edition we received 18 submissions of both short and full papers. Fourteen (14) of these were selected to present at the meeting in Vienna, and six (6) full papers were accepted to appear at this ETPCS special volume. Topics covered by this years submissions included: translations of classical to intuitionistic proofs, witness extraction from classical proofs, confluence properties for classical systems, linear logic, constructive semantics for classical logic (game semantics, realizability), and the study of calculi based on classical logic (lambda-mu-calculus, continuation calculus). △ Less

Submitted 9 September, 2014; originally announced September 2014.

ACM Class: F.4.1

Journal ref: EPTCS 164, 2014

Bar Recursion and Products of Selection Functions

Authors: Martin Escardo, Paulo Oliva

Abstract: We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector's bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown t… ▽ More We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector's bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of "skewed" selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to be T-equivalent to the iteration of the simple products. △ Less

Submitted 14 August, 2014; v1 submitted 25 July, 2014; originally announced July 2014.

Comments: 28 pages, 1 figure

MSC Class: 03F10; 03F35; 03F25 ACM Class: F.4.1

Proving termination with transition invariants of height omega

Authors: Stefano Berardi, Paulo Oliva, Silvia Steila

Abstract: The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a… ▽ More The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a "disjunctively well-founded transition invariant". From this result the same authors and Byron Cook designed an algorithm checking a sufficient condition for termination for a while-if program. The algorithm looks for a disjunctively well-founded transition invariant, made of well-founded relations of height omega, and if it finds it, it deduces the termination for the while-if program using the Termination Theorem. This raises an interesting question: What is the status of reduction relations having a disjunctively well-founded transition invariant where each relation has height omega? An answer to this question can lead to a characterization of the set of while-if programs which the termination algorithm can prove to be terminating. The goal of this work is to prove that they are exactly the set of reduction relations having height omega^n for some n < omega. Besides, if all the relations in the transition invariant are primitive recursive and the reduction relation is the graph of the restriction to some primitive recursive set of a primitive recursive map, then a final state is computable by some primitive recursive map in the initial state. As a corollary we derive that the set of functions, having at least one implementation in Podelski Rybalchenko while-if language with a well-founded disjunctively transition invariant where each relation has height omega, is exactly the set of primitive recursive functions. △ Less

Submitted 17 July, 2014; originally announced July 2014.

Crossing muons in Icecube at highest energy: Cornerstone to neutrino astronomy

Authors: D. Fargion, P. Oliva

Abstract: Highest energy neutrino events (contained) in cubic km ICECUBE detector resulted in last three years to be as many as $37-2=35$ signals (two of those having been recently discharged); these tens-hundred TeV (32 energetic events) up to rarest (only 3) PeV cascade showers, proved to have an extraterrestrial origin. The UHE neutrino flavor transition from a $ν_μ$ atmospheric dominance (over $ν_{e}$ s… ▽ More Highest energy neutrino events (contained) in cubic km ICECUBE detector resulted in last three years to be as many as $37-2=35$ signals (two of those having been recently discharged); these tens-hundred TeV (32 energetic events) up to rarest (only 3) PeV cascade showers, proved to have an extraterrestrial origin. The UHE neutrino flavor transition from a $ν_μ$ atmospheric dominance (over $ν_{e}$ showers at TeV energy), toward a higher energy shower cascade ($ν_{e}$, $ν_τ$) events at few tens TeV up to PeV energy is a hint of such a fast extraterrestrial injection. The majority (28 out of 35) of all these events are spherical cascade; their consequent smeared map is inconclusive. The additional rarest $9-2=7$ muon tracks, while being sharp in arrival directions, did not offer any correlated clustering nor any overlap** within known sources. We recently suggested that the highest energy (tens-TeV) crossing muon along the ICECUBE, mostly at horizons or upcoming, are the ideal tool able to reveal soon such clustering or even any narrow angle pointing to known (IR, X, Radio or $γ$) sources or self-correlation in rare doublet or triplet: a last hope for a meaningful and short-time $ν$ Astronomy. Any crossing muons clustering along galactic sources or within UHECR arrivals might also probe rarest UHECR event made by nuclei or neutrons. Within three years of ICECUBE data all the non-contained crossing highest energy muons above few tens TeV may be several dozens, possibly around $54$ (27 for upward ones), mostly enhanced along horizontal edges, painting known sources and/or self-correlating in doublets or rarest triplet (if steady or transient nearby source are at sight). Recent preliminary ICECUBE presentation on crossing muons are consistent with present preliminary muon rate estimate. △ Less

Submitted 9 September, 2014; v1 submitted 23 April, 2014; originally announced April 2014.

Comments: 5 pages, 2 figure, Nucl.B macro

Report number: NUPHBP15139 PII

Journal ref: Nuclear Physics B,(Proc.Suppl.) 256-257( 2014)-2013-217

On Pocrims and Hoops

Authors: Rob Arthan, Paulo Oliva

Abstract: Pocrims and suitable specialisations thereof are structures that provide the natural algebraic semantics for a minimal affine logic and its extensions. Hoops comprise a special class of pocrims that provide algebraic semantics for what we view as an intuitionistic analogue of the classical multi-valued Łukasiewicz logic. We present some contributions to the theory of these algebraic structures. We… ▽ More Pocrims and suitable specialisations thereof are structures that provide the natural algebraic semantics for a minimal affine logic and its extensions. Hoops comprise a special class of pocrims that provide algebraic semantics for what we view as an intuitionistic analogue of the classical multi-valued Łukasiewicz logic. We present some contributions to the theory of these algebraic structures. We give a new proof that the class of hoops is a variety. We use a new indirect method to establish several important identities in the theory of hoops: in particular, we prove that the double negation map** in a hoop is a homormorphism. This leads to an investigation of algebraic analogues of the various double negation translations that are well-known from proof theory. We give an algebraic framework for studying the semantics of double negation translations and use it to prove new results about the applicability of the double negation translations due to Gentzen and Glivenko. △ Less

Submitted 16 October, 2014; v1 submitted 3 April, 2014; originally announced April 2014.

Comments: 37 pages

MSC Class: 03G25; 06D35; 03B47

On Affine Logic and Łukasiewicz Logic

Authors: Rob Arthan, Paulo Oliva

Abstract: The multi-valued logic of Łukasiewicz is a substructural logic that has been widely studied and has many interesting properties. It is classical, in the sense that it admits the axiom schema of double negation, [DNE]. However, our understanding of Łukasiewicz logic can be improved by separating its classical and intuitionistic aspects. The intuitionistic aspect of Łukasiewicz logic is captured in… ▽ More The multi-valued logic of Łukasiewicz is a substructural logic that has been widely studied and has many interesting properties. It is classical, in the sense that it admits the axiom schema of double negation, [DNE]. However, our understanding of Łukasiewicz logic can be improved by separating its classical and intuitionistic aspects. The intuitionistic aspect of Łukasiewicz logic is captured in an axiom schema, [CWC], which asserts the commutativity of a weak form of conjunction. This is equivalent to a very restricted form of contraction. We show how Łukasiewicz Logic can be viewed both as an extension of classical affine logic with [CWC], or as an extension of what we call \emph{intuitionistic} Łukasiewicz logic with [DNE], intuitionistic Łukasiewicz logic being the extension of intuitionistic affine logic by the schema [CWC]. At first glance, intuitionistic affine logic seems very weak, but, in fact, [CWC] is surprisingly powerful, implying results such as intuitionistic analogues of De Morgan's laws. However the proofs can be very intricate. We present these results using derived connectives to clarify and motivate the proofs and give several applications. We give an analysis of the applicability to these logics of the well-known methods that use negation to translate classical logic into intuitionistic logic. The usual proofs of correctness for these translations make much use of contraction. Nonetheless, we show that all the usual negative translations are already correct for intuitionistic Łukasiewicz logic, where only the limited amount of contraction given by [CWC] is allowed. This is in contrast with affine logic for which we show, by appeal to results on semantics proved in a companion paper, that both the Gentzen and the Glivenko translations fail. △ Less

Submitted 14 August, 2014; v1 submitted 2 April, 2014; originally announced April 2014.

Comments: 28 pages

MSC Class: 03B47; 03B35; 03F03; 03F52 ACM Class: F.4.1

Hoops, Coops and the Algebraic Semantics of Continuous Logic

Authors: Rob Arthan, Paulo Oliva

Abstract: Büchi and Owen studied algebraic structures called hoops. Hoops provide a natural algebraic semantics for a class of substructural logics that we think of as intuitionistic analogues of the widely studied Łukasiewicz logics. Ben Yaacov extended Łukasiewicz logic to get what is called continuous logic by adding a halving operator. In this paper, we define the notion of continuous hoop, or coop for… ▽ More Büchi and Owen studied algebraic structures called hoops. Hoops provide a natural algebraic semantics for a class of substructural logics that we think of as intuitionistic analogues of the widely studied Łukasiewicz logics. Ben Yaacov extended Łukasiewicz logic to get what is called continuous logic by adding a halving operator. In this paper, we define the notion of continuous hoop, or coop for short, and show that coops provide a natural algebraic semantics for continuous logic. We characterise the simple and subdirectly irreducible coops and investigate the decision problem for various theories of coops. In passing, we give a new proof that hoops form a variety by giving an algorithm that converts a proof in intuitionistic Łukaseiwicz logic into a chain of equations. △ Less

Submitted 12 December, 2012; originally announced December 2012.

Comments: 33 pages, 3 figures

MSC Class: 03G25 03B50

Project G.N.O.S.I.S.: Geographical Network Of Synoptic Information System

Authors: Pietro Oliva

Abstract: Everybody knows how much synoptic maps are useful today. An excellent example above all is Google Earth: its simplicity and friendly interface allows every user to have the Earth maps ready in just one simple layout; nevertheless a crucial dimension is missing in Google Earth: the time. This doesn't mean we simply aim to add history to Google Earth (though it could be already a nice goal): the mai… ▽ More Everybody knows how much synoptic maps are useful today. An excellent example above all is Google Earth: its simplicity and friendly interface allows every user to have the Earth maps ready in just one simple layout; nevertheless a crucial dimension is missing in Google Earth: the time. This doesn't mean we simply aim to add history to Google Earth (though it could be already a nice goal): the main idea behind GNOSIS project is to produce applications to "dress up" the Globe with a set of skin-maps representing the most various different kind of histories like the evolution of geology, genetics, agriculture, ethnology, linguistics, musicology, metallurgy and so forth, in time. It may be interesting in the near future to have such a possibility to watch on the map the positions and movements of the armies during the battles of Waterloo or Thermopylae, the spreading of the cultivation of corn in time, the rise and fall of Roman Empire or the diffusion of Smallpox together with the spread of a religion, a specific dialect, the early pottery techniques or the natural resources available to pre-Columbian civilizations on a Google-Earth-map-like, that is to say to have at one's hand the ultimate didactic-enciclopedic tool. To do so we foresee the use of a general-purpose intermediate/high level programming language, possibly object-oriented such C++ or Java. △ Less

Submitted 3 November, 2012; originally announced November 2012.

Comments: 3 pages, Proposal for future project

A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions

Authors: Paulo Oliva, Thomas Powell

Abstract: We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics. We use Gödel's Dialectica interpretation to produce a computational version of the well known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics. △ Less

Submitted 1 June, 2012; v1 submitted 25 April, 2012; originally announced April 2012.

A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis

Authors: Paulo Oliva, Thomas Powell

Abstract: It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the prod… ▽ More It has been shown that a functional interpretation of proofs in mathematical analysis can be given by the product of selection functions, a mode of recursion that has an intuitive reading in terms of the computation of optimal strategies in sequential games. We argue that this result has genuine practical value by interpreting some well-known theorems of mathematics and demonstrating that the product gives these theorems a natural computational interpretation that can be clearly understood in game theoretic terms. △ Less

Submitted 23 April, 2012; originally announced April 2012.

(Dual) Hoops Have Unique Halving

Authors: Rob Arthan, Paulo Oliva

Abstract: Continuous logic extends the multi-valued Lukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The semantics of these logics can be given using specialisations of algebraic structures known as hoops. As part of an investigation into the metatheory of propositional continuous logic, we were ind… ▽ More Continuous logic extends the multi-valued Lukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The semantics of these logics can be given using specialisations of algebraic structures known as hoops. As part of an investigation into the metatheory of propositional continuous logic, we were indebted to Prover9 for finding a proof of an important algebraic law. △ Less

Submitted 14 October, 2013; v1 submitted 2 March, 2012; originally announced March 2012.

Comments: 17 pages, 5 figures, published as a chapter in the Bill McCune Memorial Festschrift

MSC Class: 03G25; 03B50

The effect of the geomagnetic field on cosmic ray energy estimates and large scale anisotropy searches on data from the Pierre Auger Observatory

Authors: P. Abreu, M. Aglietta, E. J. Ahn, I. F. M. Albuquerque, D. Allard, I. Allekotte, J. Allen, P. Allison, J. Alvarez Castillo, J. Alvarez-Muñiz, M. Ambrosio, A. Aminaei, L. Anchordoqui, S. Andringa, T. Antičić, A. Anzalone, C. Aramo, E. Arganda, F. Arqueros, H. Asorey, P. Assis, J. Aublin, M. Ave, M. Avenier, G. Avila , et al. (473 additional authors not shown)

Abstract: We present a comprehensive study of the influence of the geomagnetic field on the energy estimation of extensive air showers with a zenith angle smaller than $60^\circ$, detected at the Pierre Auger Observatory. The geomagnetic field induces an azimuthal modulation of the estimated energy of cosmic rays up to the ~2% level at large zenith angles. We present a method to account for this modulation… ▽ More We present a comprehensive study of the influence of the geomagnetic field on the energy estimation of extensive air showers with a zenith angle smaller than $60^\circ$, detected at the Pierre Auger Observatory. The geomagnetic field induces an azimuthal modulation of the estimated energy of cosmic rays up to the ~2% level at large zenith angles. We present a method to account for this modulation of the reconstructed energy. We analyse the effect of the modulation on large scale anisotropy searches in the arrival direction distributions of cosmic rays. At a given energy, the geomagnetic effect is shown to induce a pseudo-dipolar pattern at the percent level in the declination distribution that needs to be accounted for. △ Less

Submitted 30 November, 2011; originally announced November 2011.

Comments: 20 pages, 14 figures

Journal ref: JCAP11 (2011) 022

Trigger and Aperture of the Surface Detector Array of the Pierre Auger Observatory

Authors: J. Abraham, P. Abreu, M. Aglietta, C. Aguirre, E. J. Ahn, D. Allard, I. Allekotte, J. Allen, J. Alvarez-Muñiz, M. Ambrosio, L. Anchordoqui, S. Andringa, A. Anzalone, C. Aramo, E. Arganda, S. Argirò, K. Arisaka, F. Arneodo, F. Arqueros, T. Asch, H. Asorey, P. Assis, J. Aublin, M. Ave, G. Avila , et al. (447 additional authors not shown)

Abstract: The surface detector array of the Pierre Auger Observatory consists of 1600 water-Cherenkov detectors, for the study of extensive air showers (EAS) generated by ultra-high-energy cosmic rays. We describe the trigger hierarchy, from the identification of candidate showers at the level of a single detector, amongst a large background (mainly random single cosmic ray muons), up to the selection of re… ▽ More The surface detector array of the Pierre Auger Observatory consists of 1600 water-Cherenkov detectors, for the study of extensive air showers (EAS) generated by ultra-high-energy cosmic rays. We describe the trigger hierarchy, from the identification of candidate showers at the level of a single detector, amongst a large background (mainly random single cosmic ray muons), up to the selection of real events and the rejection of random coincidences. Such trigger makes the surface detector array fully efficient for the detection of EAS with energy above $3\times 10^{18}$ eV, for all zenith angles between 0$^\circ$ and 60$^\circ$, independently of the position of the impact point and of the mass of the primary particle. In these range of energies and angles, the exposure of the surface array can be determined purely on the basis of the geometrical acceptance. △ Less

Submitted 29 November, 2011; originally announced November 2011.

Comments: 29 pages, 12 figures

Journal ref: Nucl. Instrum. Methods A 613 (2010) 29-39

The Lateral Trigger Probability function for the Ultra-High Energy Cosmic Ray Showers detected by the Pierre Auger Observatory

Authors: The Pierre Auger Collaboration, P. Abreu, M. Aglietta, E. J. Ahn, I. F. M. Albuquerque, D. Allard, I. Allekotte, J. Allen, P. Allison, J. Alvarez Castillo, J. Alvarez-Muñiz, M. Ambrosio, A. Aminaei, L. Anchordoqui, S. Andringa, T. Antičić, A. Anzalone, C. Aramo, E. Arganda, F. Arqueros, H. Asorey, P. Assis, J. Aublin, M. Ave, M. Avenier , et al. (473 additional authors not shown)

Abstract: In this paper we introduce the concept of Lateral Trigger Probability (LTP) function, i.e., the probability for an extensive air shower (EAS) to trigger an individual detector of a ground based array as a function of distance to the shower axis, taking into account energy, mass and direction of the primary cosmic ray. We apply this concept to the surface array of the Pierre Auger Observatory consi… ▽ More In this paper we introduce the concept of Lateral Trigger Probability (LTP) function, i.e., the probability for an extensive air shower (EAS) to trigger an individual detector of a ground based array as a function of distance to the shower axis, taking into account energy, mass and direction of the primary cosmic ray. We apply this concept to the surface array of the Pierre Auger Observatory consisting of a 1.5 km spaced grid of about 1600 water Cherenkov stations. Using Monte Carlo simulations of ultra-high energy showers the LTP functions are derived for energies in the range between 10^{17} and 10^{19} eV and zenith angles up to 65 degs. A parametrization combining a step function with an exponential is found to reproduce them very well in the considered range of energies and zenith angles. The LTP functions can also be obtained from data using events simultaneously observed by the fluorescence and the surface detector of the Pierre Auger Observatory (hybrid events). We validate the Monte-Carlo results showing how LTP functions from data are in good agreement with simulations. △ Less

Submitted 28 November, 2011; originally announced November 2011.

Comments: 22 pages, 8 figures. Published in Astroparticle Physics

Journal ref: Astroparticle Physics 35 (2011) 266-276

Search for signatures of magnetically-induced alignment in the arrival directions measured by the Pierre Auger Observatory

Authors: The Pierre Auger Collaboration, P. Abreu, M. Aglietta, E. J. Ahn, I. F. M. Albuquerque, D. Allard, I. Allekotte, J. Allen, P. Allison, J. Alvarez Castillo, J. Alvarez-Muñiz, M. Ambrosio, A. Aminaei, L. Anchordoqui, S. Andringa, T. Antičić, A. Anzalone, C. Aramo, E. Arganda, F. Arqueros, H. Asorey, P. Assis, J. Aublin, M. Ave, M. Avenier , et al. (474 additional authors not shown)

Abstract: We present the results of an analysis of data recorded at the Pierre Auger Observatory in which we search for groups of directionally-aligned events (or `multiplets') which exhibit a correlation between arrival direction and the inverse of the energy. These signatures are expected from sets of events coming from the same source after having been deflected by intervening coherent magnetic fields. T… ▽ More We present the results of an analysis of data recorded at the Pierre Auger Observatory in which we search for groups of directionally-aligned events (or `multiplets') which exhibit a correlation between arrival direction and the inverse of the energy. These signatures are expected from sets of events coming from the same source after having been deflected by intervening coherent magnetic fields. The observation of several events from the same source would open the possibility to accurately reconstruct the position of the source and also measure the integral of the component of the magnetic field orthogonal to the trajectory of the cosmic rays. We describe the largest multiplets found and compute the probability that they appeared by chance from an isotropic distribution. We find no statistically significant evidence for the presence of multiplets arising from magnetic deflections in the present data. △ Less

Submitted 10 November, 2011; originally announced November 2011.

Comments: Accepted for publication in Astroparticle Physics