Showing 1–50 of 50 results for author: Marcos, J

EUSO-SPB1 Mission and Science

Authors: JEM-EUSO Collaboration, :, G. Abdellaoui, S. Abe, J. H. Adams. Jr., D. Allard, G. Alonso, L. Anchordoqui, A. Anzalone, E. Arnone, K. Asano, R. Attallah, H. Attoui, M. Ave Pernas, R. Bachmann, S. Bacholle, M. Bagheri, M. Bakiri, J. Baláz, D. Barghini, S. Bartocci, M. Battisti, J. Bayer, B. Beldjilali, T. Belenguer , et al. (271 additional authors not shown)

Abstract: The Extreme Universe Space Observatory on a Super Pressure Balloon 1 (EUSO-SPB1) was launched in 2017 April from Wanaka, New Zealand. The plan of this mission of opportunity on a NASA super pressure balloon test flight was to circle the southern hemisphere. The primary scientific goal was to make the first observations of ultra-high-energy cosmic-ray extensive air showers (EASs) by looking down on… ▽ More The Extreme Universe Space Observatory on a Super Pressure Balloon 1 (EUSO-SPB1) was launched in 2017 April from Wanaka, New Zealand. The plan of this mission of opportunity on a NASA super pressure balloon test flight was to circle the southern hemisphere. The primary scientific goal was to make the first observations of ultra-high-energy cosmic-ray extensive air showers (EASs) by looking down on the atmosphere with an ultraviolet (UV) fluorescence telescope from suborbital altitude (33~km). After 12~days and 4~hours aloft, the flight was terminated prematurely in the Pacific Ocean. Before the flight, the instrument was tested extensively in the West Desert of Utah, USA, with UV point sources and lasers. The test results indicated that the instrument had sensitivity to EASs of approximately 3 EeV. Simulations of the telescope system, telescope on time, and realized flight trajectory predicted an observation of about 1 event assuming clear sky conditions. The effects of high clouds were estimated to reduce this value by approximately a factor of 2. A manual search and a machine-learning-based search did not find any EAS signals in these data. Here we review the EUSO-SPB1 instrument and flight and the EAS search. △ Less

Submitted 12 January, 2024; originally announced January 2024.

Comments: 18 pages, 19 figures

Journal ref: Astropart Phys 154 (2024) 102891

High-Resolution Building and Road Detection from Sentinel-2

Authors: Wojciech Sirko, Emmanuel Asiedu Brempong, Juliana T. C. Marcos, Abigail Annkah, Abel Korme, Mohammed Alewi Hassen, Krishna Sapkota, Tomer Shekel, Abdoulaye Diack, Sella Nevo, Jason Hickey, John Quinn

Abstract: Map** buildings and roads automatically with remote sensing typically requires high-resolution imagery, which is expensive to obtain and often sparsely available. In this work we demonstrate how multiple 10 m resolution Sentinel-2 images can be used to generate 50 cm resolution building and road segmentation masks. This is done by training a `student' model with access to Sentinel-2 images to re… ▽ More Map** buildings and roads automatically with remote sensing typically requires high-resolution imagery, which is expensive to obtain and often sparsely available. In this work we demonstrate how multiple 10 m resolution Sentinel-2 images can be used to generate 50 cm resolution building and road segmentation masks. This is done by training a `student' model with access to Sentinel-2 images to reproduce the predictions of a `teacher' model which has access to corresponding high-resolution imagery. While the predictions do not have all the fine detail of the teacher model, we find that we are able to retain much of the performance: for building segmentation we achieve 78.3% mIoU, compared to the high-resolution teacher model accuracy of 85.3% mIoU. We also describe a related method for counting individual buildings in a Sentinel-2 patch which achieves R^2 = 0.91 against true counts. This work opens up new possibilities for using freely available Sentinel-2 imagery for a range of tasks that previously could only be done with high-resolution satellite imagery. △ Less

Submitted 20 June, 2024; v1 submitted 17 October, 2023; originally announced October 2023.

Adding an Implication to Logics of Perfect Paradefinite Algebras

Authors: Vitor Greati, Sérgio Marcelino, João Marcos, Umberto Rivieccio

Abstract: Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal… ▽ More Perfect paradefinite algebras are De Morgan algebras expanded with an operation that allows for the full behavior of classical negation to be restored. They form a variety that is term-equivalent to the variety of involutive Stone algebras. Their associated multiple-conclusion (Set-Set) and single-conclusion (Set-Fmla) order-preserving logics are non-algebraizable self-extensional logics of formal inconsistency and undeterminedness determined by a six-valued matrix, studied in depth by Gomes et al. (2022) from both the algebraic and the proof-theoretical perspectives. In the present paper, we continue that study by investigating directions for conservatively expanding these logics with an implication connective (essentially, one that admits the deduction-detachment theorem). We first consider logics given by very simple and manageable non-deterministic semantics whose implication (in isolation) is classical. These, nevertheless, fail to be self-extensional. We then consider the implication realized by the relative pseudo-complement over the six-valued perfect paradefinite algebra. Our strategy is to expand the language of the latter algebra with this connective and study the (self-extensional) Set-Set and Set-Fmla order-preserving and top-assertional logics of the variety induced by the resulting algebra. We provide axiomatizations for such new variety and for such logics, drawing parallels with the class of symmetric Heyting algebras and with Moisil's 'symmetric modal logic'. For the Set-Set logic, in particular, the axiomatization we obtain is analytic. We close by studying interpolation properties for these logics and concluding that the new variety has the Maehara amalgamation property. △ Less

Submitted 6 April, 2024; v1 submitted 13 September, 2023; originally announced September 2023.

Comments: New version after a round of peer reviewing, no critical changes

MSC Class: 03G10 (Primary) 03C05; 03B50; 03B70; 03B53; 03B22; 03B35; 03C40 (Secondary) ACM Class: F.4.1

The Greenland Telescope: Construction, Commissioning, and Operations in Pituffik

Authors: Ming-Tang Chen, Keiichi Asada, Satoki Matsushita, Philippe Raffin, Makoto Inoue, Paul T. P. Ho, Chih-Chiang Han, Derek Kubo, Timothy Norton, Nimesh A. Patel, George Nystrom, Chih-Wei L. Huang, Pierre Martin-Cocher, Jun Yi Koay, Cristina Romero-Cañizales, Ching-Tang Liu, Teddy Huang, Kuan-Yu Liu, Tashun Wei, Shu-Hao Chang, Ryan Chilson, Peter Oshiro, Homin Jiang, Chao-Te Li, Geoffrey Bower , et al. (29 additional authors not shown)

Abstract: In 2018, the Greenland Telescope (GLT) started scientific observation in Greenland. Since then, we have completed several significant improvements and added new capabilities to the telescope system. This paper presents a full review of the GLT system, a summary of our observation activities since 2018, the lessons learned from the operations in the Arctic regions, and the prospect of the telescope… ▽ More In 2018, the Greenland Telescope (GLT) started scientific observation in Greenland. Since then, we have completed several significant improvements and added new capabilities to the telescope system. This paper presents a full review of the GLT system, a summary of our observation activities since 2018, the lessons learned from the operations in the Arctic regions, and the prospect of the telescope. △ Less

Submitted 19 July, 2023; originally announced July 2023.

Comments: 26 pages, 11 figures, and 8 tables. This is the version of the article before publication editing, as submitted by an author to Publications of the Astronomical Society of the Pacific. IOP Publishing Ltd is not responsible for any errors or omissions in this version of the manuscript or any version derived from it. The Version of Record will be added when it becomes available

Proceedings 11th International Workshop on Theorem Proving Components for Educational Software

Authors: Pedro Quaresma, João Marcos, Walther Neuper

Abstract: The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise. The 11th International Wor… ▽ More The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. What follows is a brief description of how the present volume contributes to this enterprise. The 11th International Workshop on Theorem Proving Components for Educational Software (ThEdu'22), was a satellite event of the 8th Federated Logic Conference (FLoC 2022), July 31-August 12, 2022, Haifa, Israel ThEdu'22 was a vibrant workshop, with two invited talk by Thierry Dana-Picard (Jerusalem College of Technology, Jerusalem, Israel) and Yoni Zohar (Bar Ilan University, Tel Aviv, Israel) and four contributions. An open call for papers was then issued, and attracted seven submissions. Those submissions have been accepted by our reviewers, who jointly produced at least three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. The contributions in this volume are a faithful representation of the wide spectrum of ThEdu, ranging from those more focused on the automated deduction research, not losing track of the possible applications in an educational setting, to those focused on the applications, in educational settings, of automated deduction tools and methods. We, the volume editors, hope that this collection of papers will further promote the development of theorem-proving based software, and that it will allow to improve the mutual understanding between computer scientists, mathematicians and stakeholders in education. While this volume goes to press, the next edition of the ThEdu workshop is being prepared: ThEdu'23 will be a satellite event of the 29th international Conference on Automated Deduction (CADE 2023), July 1-4, 2023, Rome, Italy. △ Less

Submitted 9 March, 2023; originally announced March 2023.

Journal ref: EPTCS 375, 2023

Self-solidifying active droplets showing memory-induced chirality

Authors: Kai Feng, José Carlos Ureña Marcos, Aritra K. Mukhopadhyay, Ran Niu, Qiang Zhao, **** Qu, Benno Liebchen

Abstract: Most synthetic microswimmers do not reach the autonomy of their biological counterparts in terms of energy supply and diversity of motion. Here we report the first all-aqueous droplet swimmer powered by self-generated polyelectrolyte gradients, which shows memory-induced chirality while self-solidifying. An aqueous solution of surface tension-lowering polyelectrolytes self-solidifies on the surfac… ▽ More Most synthetic microswimmers do not reach the autonomy of their biological counterparts in terms of energy supply and diversity of motion. Here we report the first all-aqueous droplet swimmer powered by self-generated polyelectrolyte gradients, which shows memory-induced chirality while self-solidifying. An aqueous solution of surface tension-lowering polyelectrolytes self-solidifies on the surface of acidic water, during which polyelectrolytes are gradually emitted into the surrounding water and induce linear self-propulsion via spontaneous symmetry breaking. The low diffusion coefficient of the polyelectrolytes leads to long-lived chemical trails which cause memory effects that drive a transition from linear to chiral motion without requiring any imposed symmetry breaking. The droplet swimmer is capable of highly efficient removal (up to 85%) of uranium from aqueous solutions within 90 min, benefiting from self-propulsion and flow-induced mixing. Our results provide a route to fueling self-propelled agents which can autonomously perform chiral motion and collect toxins. △ Less

Submitted 24 October, 2023; v1 submitted 8 February, 2023; originally announced February 2023.

Inverted Sedimentation of Active Particles in Unbiased ac Fields

Authors: José Carlos Ureña Marcos, Benno Liebchen

Abstract: Gaining control over the motion of active particles is crucial for applications ranging from targeted cargo delivery to nanomedicine. While much progress has been made recently to control active motion based on external forces, flows or gradients in concentration or light intensity, which all have a well-defined direction or bias, little is known about how to steer active particles in situations w… ▽ More Gaining control over the motion of active particles is crucial for applications ranging from targeted cargo delivery to nanomedicine. While much progress has been made recently to control active motion based on external forces, flows or gradients in concentration or light intensity, which all have a well-defined direction or bias, little is known about how to steer active particles in situations where no permanent bias can be realized. Here, we show that ac fields with a vanishing time average provide an alternative route to steering active particles. We exemplify this route for inertial active particles in a gravitational field, observing that a substantial fraction of them persistently travels in the upward direction upon switching on the ac field, resulting in an inverted sedimentation profile at the top wall of a confining container. Our results offer a generic control principle which could be used in the future to steer active motion, to direct collective behaviors and to purify mixtures. △ Less

Submitted 28 November, 2022; v1 submitted 24 November, 2022; originally announced November 2022.

Gaia Data Release 3: Summary of the content and survey properties

Authors: Gaia Collaboration, A. Vallenari, A. G. A. Brown, T. Prusti, J. H. J. de Bruijne, F. Arenou, C. Babusiaux, M. Biermann, O. L. Creevey, C. Ducourant, D. W. Evans, L. Eyer, R. Guerra, A. Hutton, C. Jordi, S. A. Klioner, U. L. Lammers, L. Lindegren, X. Luri, F. Mignard, C. Panem, D. Pourbaix, S. Randich, P. Sartoretti, C. Soubiran , et al. (431 additional authors not shown)

Abstract: We present the third data release of the European Space Agency's Gaia mission, GDR3. The GDR3 catalogue is the outcome of the processing of raw data collected with the Gaia instruments during the first 34 months of the mission by the Gaia Data Processing and Analysis Consortium. The GDR3 catalogue contains the same source list, celestial positions, proper motions, parallaxes, and broad band photom… ▽ More We present the third data release of the European Space Agency's Gaia mission, GDR3. The GDR3 catalogue is the outcome of the processing of raw data collected with the Gaia instruments during the first 34 months of the mission by the Gaia Data Processing and Analysis Consortium. The GDR3 catalogue contains the same source list, celestial positions, proper motions, parallaxes, and broad band photometry in the G, G$_{BP}$, and G$_{RP}$ pass-bands already present in the Early Third Data Release. GDR3 introduces an impressive wealth of new data products. More than 33 million objects in the ranges $G_{rvs} < 14$ and $3100 <T_{eff} <14500 $, have new determinations of their mean radial velocities based on data collected by Gaia. We provide G$_{rvs}$ magnitudes for most sources with radial velocities, and a line broadening parameter is listed for a subset of these. Mean Gaia spectra are made available to the community. The GDR3 catalogue includes about 1 million mean spectra from the radial velocity spectrometer, and about 220 million low-resolution blue and red prism photometer BPRP mean spectra. The results of the analysis of epoch photometry are provided for some 10 million sources across 24 variability types. GDR3 includes astrophysical parameters and source class probabilities for about 470 million and 1500 million sources, respectively, including stars, galaxies, and quasars. Orbital elements and trend parameters are provided for some $800\,000$ astrometric, spectroscopic and eclipsing binaries. More than $150\,000$ Solar System objects, including new discoveries, with preliminary orbital solutions and individual epoch observations are part of this release. Reflectance spectra derived from the epoch BPRP spectral data are published for about 60\,000 asteroids. Finally, an additional data set is provided, namely the Gaia Andromeda Photometric Survey (abridged) △ Less

Submitted 30 July, 2022; originally announced August 2022.

Comments: 23 pages, 2 figures

Gaia Data Release 3: Reflectance spectra of Solar System small bodies

Authors: Gaia Collaboration, L. Galluccio, M. Delbo, F. De Angeli, T. Pauwels, P. Tanga, F. Mignard, A. Cellino, A. G. A. Brown, K. Muinonen, A. Penttila, S. Jordan, A. Vallenari, T. Prusti, J. H. J. de Bruijne, F. Arenou, C. Babusiaux, M. Biermann, O. L. Creevey, C. Ducourant, D. W. Evans, L. Eyer, R. Guerra, A. Hutton, C. Jordi , et al. (422 additional authors not shown)

Abstract: The Gaia mission of the European Space Agency (ESA) has been routinely observing Solar System objects (SSOs) since the beginning of its operations in August 2014. The Gaia data release three (DR3) includes, for the first time, the mean reflectance spectra of a selected sample of 60 518 SSOs, primarily asteroids, observed between August 5, 2014, and May 28, 2017. Each reflectance spectrum was deriv… ▽ More The Gaia mission of the European Space Agency (ESA) has been routinely observing Solar System objects (SSOs) since the beginning of its operations in August 2014. The Gaia data release three (DR3) includes, for the first time, the mean reflectance spectra of a selected sample of 60 518 SSOs, primarily asteroids, observed between August 5, 2014, and May 28, 2017. Each reflectance spectrum was derived from measurements obtained by means of the Blue and Red photometers (BP/RP), which were binned in 16 discrete wavelength bands. We describe the processing of the Gaia spectral data of SSOs, explaining both the criteria used to select the subset of asteroid spectra published in Gaia DR3, and the different steps of our internal validation procedures. In order to further assess the quality of Gaia SSO reflectance spectra, we carried out external validation against SSO reflectance spectra obtained from ground-based and space-borne telescopes and available in the literature. For each selected SSO, an epoch reflectance was computed by dividing the calibrated spectrum observed by the BP/RP at each transit on the focal plane by the mean spectrum of a solar analogue. The latter was obtained by averaging the Gaia spectral measurements of a selected sample of stars known to have very similar spectra to that of the Sun. Finally, a mean of the epoch reflectance spectra was calculated in 16 spectral bands for each SSO. The agreement between Gaia mean reflectance spectra and those available in the literature is good for bright SSOs, regardless of their taxonomic spectral class. We identify an increase in the spectral slope of S-type SSOs with increasing phase angle. Moreover, we show that the spectral slope increases and the depth of the 1 um absorption band decreases for increasing ages of S-type asteroid families. △ Less

Submitted 24 June, 2022; originally announced June 2022.

Comments: 30 pages, 26 figures

Gaia Data Release 3: Map** the asymmetric disc of the Milky Way

Authors: Gaia Collaboration, R. Drimmel, M. Romero-Gomez, L. Chemin, P. Ramos, E. Poggio, V. Ripepi, R. Andrae, R. Blomme, T. Cantat-Gaudin, A. Castro-Ginard, G. Clementini, F. Figueras, M. Fouesneau, Y. Fremat, K. Jardine, S. Khanna, A. Lobel, D. J. Marshall, T. Muraveva, A. G. A. Brown, A. Vallenari, T. Prusti, J. H. J. de Bruijne, F. Arenou , et al. (431 additional authors not shown)

Abstract: With the most recent Gaia data release the number of sources with complete 6D phase space information (position and velocity) has increased to well over 33 million stars, while stellar astrophysical parameters are provided for more than 470 million sources, in addition to the identification of over 11 million variable stars. Using the astrophysical parameters and variability classifications provid… ▽ More With the most recent Gaia data release the number of sources with complete 6D phase space information (position and velocity) has increased to well over 33 million stars, while stellar astrophysical parameters are provided for more than 470 million sources, in addition to the identification of over 11 million variable stars. Using the astrophysical parameters and variability classifications provided in Gaia DR3, we select various stellar populations to explore and identify non-axisymmetric features in the disc of the Milky Way in both configuration and velocity space. Using more about 580 thousand sources identified as hot OB stars, together with 988 known open clusters younger than 100 million years, we map the spiral structure associated with star formation 4-5 kpc from the Sun. We select over 2800 Classical Cepheids younger than 200 million years, which show spiral features extending as far as 10 kpc from the Sun in the outer disc. We also identify more than 8.7 million sources on the red giant branch (RGB), of which 5.7 million have line-of-sight velocities, allowing the velocity field of the Milky Way to be mapped as far as 8 kpc from the Sun, including the inner disc. The spiral structure revealed by the young populations is consistent with recent results using Gaia EDR3 astrometry and source lists based on near infrared photometry, showing the Local (Orion) arm to be at least 8 kpc long, and an outer arm consistent with what is seen in HI surveys, which seems to be a continuation of the Perseus arm into the third quadrant. Meanwhile, the subset of RGB stars with velocities clearly reveals the large scale kinematic signature of the bar in the inner disc, as well as evidence of streaming motions in the outer disc that might be associated with spiral arms or bar resonances. (abridged) △ Less

Submitted 5 August, 2022; v1 submitted 13 June, 2022; originally announced June 2022.

Comments: 35 pages, 27 figures, accepted for publication in A&A special Gaia DR3 issue. V2: abstract completed. V3: complete author list and link to data: https://drive.google.com/drive/u/1/folders/1yOJPjYmM7QK5XVsqaiSOTuwDQNti2LlZ

Journal ref: A&A 674, A37 (2023)

Gaia Data Release 3: Pulsations in main sequence OBAF-type stars

Authors: Gaia Collaboration, J. De Ridder, V. Ripepi, C. Aerts, L. Palaversa, L. Eyer, B. Holl, M. Audard, L. Rimoldini, A. G. A. Brown, A. Vallenari, T. Prusti, J. H. J. de Bruijne, F. Arenou, C. Babusiaux, M. Biermann, O. L. Creevey, C. Ducourant, D. W. Evans, R. Guerra, A. Hutton, C. Jordi, S. A. Klioner, U. L. Lammers, L. Lindegren , et al. (423 additional authors not shown)

Abstract: The third Gaia data release provides photometric time series covering 34 months for about 10 million stars. For many of those stars, a characterisation in Fourier space and their variability classification are also provided. This paper focuses on intermediate- to high-mass (IHM) main sequence pulsators M >= 1.3 Msun) of spectral types O, B, A, or F, known as beta Cep, slowly pulsating B (SPB), del… ▽ More The third Gaia data release provides photometric time series covering 34 months for about 10 million stars. For many of those stars, a characterisation in Fourier space and their variability classification are also provided. This paper focuses on intermediate- to high-mass (IHM) main sequence pulsators M >= 1.3 Msun) of spectral types O, B, A, or F, known as beta Cep, slowly pulsating B (SPB), delta Sct, and gamma Dor stars. These stars are often multi-periodic and display low amplitudes, making them challenging targets to analyse with sparse time series. All datasets used in this analysis are part of the Gaia DR3 data release. The photometric time series were used to perform a Fourier analysis, while the global astrophysical parameters necessary for the empirical instability strips were taken from the Gaia DR3 gspphot tables, and the vsini data were taken from the Gaia DR3 esphs tables. We show that for nearby OBAF-type pulsators, the Gaia DR3 data are precise and accurate enough to pinpoint them in the Hertzsprung-Russell diagram. We find empirical instability strips covering broader regions than theoretically predicted. In particular, our study reveals the presence of fast rotating gravity-mode pulsators outside the strips, as well as the co-existence of rotationally modulated variables inside the strips as reported before in the literature. We derive an extensive period-luminosity relation for delta Sct stars and provide evidence that the relation features different regimes depending on the oscillation period. Finally, we demonstrate how stellar rotation attenuates the amplitude of the dominant oscillation mode of delta Sct stars. △ Less

Submitted 16 August, 2022; v1 submitted 13 June, 2022; originally announced June 2022.

Journal ref: A&A 674, A36 (2023)

Gaia Data Release 3: A Golden Sample of Astrophysical Parameters

Authors: Gaia Collaboration, O. L. Creevey, L. M. Sarro, A. Lobel, E. Pancino, R. Andrae, R. L. Smart, G. Clementini, U. Heiter, A. J. Korn, M. Fouesneau, Y. Frémat, F. De Angeli, A. Vallenari, D. L. Harrison, F. Thévenin, C. Reylé, R. Sordo, A. Garofalo, A. G. A. Brown, L. Eyer, T. Prusti, J. H. J. de Bruijne, F. Arenou, C. Babusiaux , et al. (423 additional authors not shown)

Abstract: Gaia Data Release 3 (DR3) provides a wealth of new data products for the astronomical community to exploit, including astrophysical parameters for a half billion stars. In this work we demonstrate the high quality of these data products and illustrate their use in different astrophysical contexts. We query the astrophysical parameter tables along with other tables in Gaia DR3 to derive the samples… ▽ More Gaia Data Release 3 (DR3) provides a wealth of new data products for the astronomical community to exploit, including astrophysical parameters for a half billion stars. In this work we demonstrate the high quality of these data products and illustrate their use in different astrophysical contexts. We query the astrophysical parameter tables along with other tables in Gaia DR3 to derive the samples of the stars of interest. We validate our results by using the Gaia catalogue itself and by comparison with external data. We have produced six homogeneous samples of stars with high quality astrophysical parameters across the HR diagram for the community to exploit. We first focus on three samples that span a large parameter space: young massive disk stars (~3M), FGKM spectral type stars (~3M), and UCDs (~20K). We provide these sources along with additional information (either a flag or complementary parameters) as tables that are made available in the Gaia archive. We furthermore identify 15740 bone fide carbon stars, 5863 solar-analogues, and provide the first homogeneous set of stellar parameters of the Spectro Photometric Standard Stars. We use a subset of the OBA sample to illustrate its usefulness to analyse the Milky Way rotation curve. We then use the properties of the FGKM stars to analyse known exoplanet systems. We also analyse the ages of some unseen UCD-companions to the FGKM stars. We additionally predict the colours of the Sun in various passbands (Gaia, 2MASS, WISE) using the solar-analogue sample. △ Less

Submitted 12 June, 2022; originally announced June 2022.

Comments: 35 pages, (incl 6 pages references, acknowledgements, affiliations), 37 figures, A&A accepted

Journal ref: A&A 674, A39 (2023)

Gaia Data Release 3: The extragalactic content

Authors: Gaia Collaboration, C. A. L. Bailer-Jones, D. Teyssier, L. Delchambre, C. Ducourant, D. Garabato, D. Hatzidimitriou, S. A. Klioner, L. Rimoldini, I. Bellas-Velidis, R. Carballo, M. I. Carnerero, C. Diener, M. Fouesneau, L. Galluccio, P. Gavras, A. Krone-Martins, C. M. Raiteri, R. Teixeira, A. G. A. Brown, A. Vallenari, T. Prusti, J. H. J. de Bruijne, F. Arenou, C. Babusiaux , et al. (422 additional authors not shown)

Abstract: The Gaia Galactic survey mission is designed and optimized to obtain astrometry, photometry, and spectroscopy of nearly two billion stars in our Galaxy. Yet as an all-sky multi-epoch survey, Gaia also observes several million extragalactic objects down to a magnitude of G~21 mag. Due to the nature of the Gaia onboard selection algorithms, these are mostly point-source-like objects. Using data prov… ▽ More The Gaia Galactic survey mission is designed and optimized to obtain astrometry, photometry, and spectroscopy of nearly two billion stars in our Galaxy. Yet as an all-sky multi-epoch survey, Gaia also observes several million extragalactic objects down to a magnitude of G~21 mag. Due to the nature of the Gaia onboard selection algorithms, these are mostly point-source-like objects. Using data provided by the satellite, we have identified quasar and galaxy candidates via supervised machine learning methods, and estimate their redshifts using the low resolution BP/RP spectra. We further characterise the surface brightness profiles of host galaxies of quasars and of galaxies from pre-defined input lists. Here we give an overview of the processing of extragalactic objects, describe the data products in Gaia DR3, and analyse their properties. Two integrated tables contain the main results for a high completeness, but low purity (50-70%), set of 6.6 million candidate quasars and 4.8 million candidate galaxies. We provide queries that select purer sub-samples of these containing 1.9 million probable quasars and 2.9 million probable galaxies (both 95% purity). We also use high quality BP/RP spectra of 43 thousand high probability quasars over the redshift range 0.05-4.36 to construct a composite quasar spectrum spanning restframe wavelengths from 72-100 nm. △ Less

Submitted 12 June, 2022; originally announced June 2022.

Comments: Accepted to A&A

Gaia Data Release 3: Stellar multiplicity, a teaser for the hidden treasure

Authors: Gaia Collaboration, F. Arenou, C. Babusiaux, M. A. Barstow, S. Faigler, A. Jorissen, P. Kervella, T. Mazeh, N. Mowlavi, P. Panuzzo, J. Sahlmann, S. Shahaf, A. Sozzetti, N. Bauchet, Y. Damerdji, P. Gavras, P. Giacobbe, E. Gosset, J. -L. Halbwachs, B. Holl, M. G. Lattanzi, N. Leclerc, T. Morel, D. Pourbaix, P. Re Fiorentin , et al. (425 additional authors not shown)

Abstract: The Gaia DR3 Catalogue contains for the first time about eight hundred thousand solutions with either orbital elements or trend parameters for astrometric, spectroscopic and eclipsing binaries, and combinations of them. This paper aims to illustrate the huge potential of this large non-single star catalogue. Using the orbital solutions together with models of the binaries, a catalogue of tens of t… ▽ More The Gaia DR3 Catalogue contains for the first time about eight hundred thousand solutions with either orbital elements or trend parameters for astrometric, spectroscopic and eclipsing binaries, and combinations of them. This paper aims to illustrate the huge potential of this large non-single star catalogue. Using the orbital solutions together with models of the binaries, a catalogue of tens of thousands of stellar masses, or lower limits, partly together with consistent flux ratios, has been built. Properties concerning the completeness of the binary catalogues are discussed, statistical features of the orbital elements are explained and a comparison with other catalogues is performed. Illustrative applications are proposed for binaries across the H-R diagram. The binarity is studied in the RGB/AGB and a search for genuine SB1 among long-period variables is performed. The discovery of new EL CVn systems illustrates the potential of combining variability and binarity catalogues. Potential compact object companions are presented, mainly white dwarf companions or double degenerates, but one candidate neutron star is also presented. Towards the bottom of the main sequence, the orbits of previously-suspected binary ultracool dwarfs are determined and new candidate binaries are discovered. The long awaited contribution of Gaia to the analysis of the substellar regime shows the brown dwarf desert around solar-type stars using true, rather than minimum, masses, and provides new important constraints on the occurrence rates of substellar companions to M dwarfs. Several dozen new exoplanets are proposed, including two with validated orbital solutions and one super-Jupiter orbiting a white dwarf, all being candidates requiring confirmation. Beside binarity, higher order multiple systems are also found. △ Less

Submitted 11 June, 2022; originally announced June 2022.

Comments: 60 pages, 60 figures. Accepted for publication in Astronomy & Astrophysics (2022-06-09). The catalogue of binary masses is available for download from the ESA Gaia DR3 Archive and will be available from the CDS/VizieR service

Journal ref: A&A 674, A34 (2023)

Gaia Data Release 3: Chemical cartography of the Milky Way

Authors: Gaia Collaboration, A. Recio-Blanco, G. Kordopatis, P. de Laverny, P. A. Palicio, A. Spagna, L. Spina, D. Katz, P. Re Fiorentin, E. Poggio, P. J. McMillan, A. Vallenari, M. G. Lattanzi, G. M. Seabroke, L. Casamiquela, A. Bragaglia, T. Antoja, C. A. L. Bailer-Jones, R. Andrae, M. Fouesneau, M. Cropper, T. Cantat-Gaudin, U. Heiter, A. Bijaoui, A. G. A. Brown , et al. (425 additional authors not shown)

Abstract: Gaia DR3 opens a new era of all-sky spectral analysis of stellar populations thanks to the nearly 5.6 million stars observed by the RVS and parametrised by the GSP-spec module. The all-sky Gaia chemical cartography allows a powerful and precise chemo-dynamical view of the Milky Way with unprecedented spatial coverage and statistical robustness. First, it reveals the strong vertical symmetry of the… ▽ More Gaia DR3 opens a new era of all-sky spectral analysis of stellar populations thanks to the nearly 5.6 million stars observed by the RVS and parametrised by the GSP-spec module. The all-sky Gaia chemical cartography allows a powerful and precise chemo-dynamical view of the Milky Way with unprecedented spatial coverage and statistical robustness. First, it reveals the strong vertical symmetry of the Galaxy and the flared structure of the disc. Second, the observed kinematic disturbances of the disc -- seen as phase space correlations -- and kinematic or orbital substructures are associated with chemical patterns that favour stars with enhanced metallicities and lower [alpha/Fe] abundance ratios compared to the median values in the radial distributions. This is detected both for young objects that trace the spiral arms and older populations. Several alpha, iron-peak elements and at least one heavy element trace the thin and thick disc properties in the solar cylinder. Third, young disc stars show a recent chemical impoverishment in several elements. Fourth, the largest chemo-dynamical sample of open clusters analysed so far shows a steepening of the radial metallicity gradient with age, which is also observed in the young field population. Finally, the Gaia chemical data have the required coverage and precision to unveil galaxy accretion debris and heated disc stars on halo orbits through their [alpha/Fe] ratio, and to allow the study of the chemo-dynamical properties of globular clusters. Gaia DR3 chemo-dynamical diagnostics open new horizons before the era of ground-based wide-field spectroscopic surveys. They unveil a complex Milky Way that is the outcome of an eventful evolution, sha** it to the present day (abridged). △ Less

Submitted 11 June, 2022; originally announced June 2022.

Comments: Astronomy and Astrophysics (accepted, in press)

Journal ref: A&A 674, A38 (2023)

Finite two-dimensional proof systems for non-finitely axiomatizable logics

Authors: Vitor Greati, João Marcos

Abstract: The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional)… ▽ More The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional) logics determined by (non-deterministic) logical matrices are known to be axiomatizable by analytic and possibly finite proof systems as soon as they turn out to satisfy a certain constraint of sufficient expressiveness. In this paper we introduce a recipe for cooking up a two-dimensional logical matrix (or B-matrix) by the combination of two (possibly partial) non-deterministic logical matrices. We will show that such a combination may result in B-matrices satisfying the property of sufficient expressiveness, even when the input matrices are not sufficiently expressive in isolation, and we will use this result to show that one-dimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics, becoming, thus, finitely axiomatizable by the addition of an extra dimension. We will illustrate the said construction using a well-known logic of formal inconsistency called mCi. We will first prove that this logic is not finitely axiomatizable by a one-dimensional (generalized) Hilbert-style system. Then, taking advantage of a known 5-valued non-deterministic logical matrix for this logic, we will combine it with another one, conveniently chosen so as to give rise to a B-matrix that is axiomatized by a two-dimensional Hilbert-style system that is both finite and analytic. △ Less

Submitted 18 May, 2022; originally announced May 2022.

MSC Class: 03B50; 03B22; 03A05; 03B35; 03B25 ACM Class: F.4.1; I.1.2

Gaia Early Data Release 3: The celestial reference frame (Gaia-CRF3)

Authors: Gaia Collaboration, S. A. Klioner, L. Lindegren, F. Mignard, J. Hernández, M. Ramos-Lerate, U. Bastian, M. Biermann, A. Bombrun, A. de Torres, E. Gerlach, R. Geyer, T. Hilger, D. Hobbs, U. L. Lammers, P. J. McMillan, H. Steidelmüller, D. Teyssier, C. M. Raiteri, S. Bartolomé, M. Bernet, J. Castañeda, M. Clotet, M. Davidson, C. Fabricius , et al. (426 additional authors not shown)

Abstract: Gaia-CRF3 is the celestial reference frame for positions and proper motions in the third release of data from the Gaia mission, Gaia DR3 (and for the early third release, Gaia EDR3, which contains identical astrometric results). The reference frame is defined by the positions and proper motions at epoch 2016.0 for a specific set of extragalactic sources in the (E)DR3 catalogue. We describe the c… ▽ More Gaia-CRF3 is the celestial reference frame for positions and proper motions in the third release of data from the Gaia mission, Gaia DR3 (and for the early third release, Gaia EDR3, which contains identical astrometric results). The reference frame is defined by the positions and proper motions at epoch 2016.0 for a specific set of extragalactic sources in the (E)DR3 catalogue. We describe the construction of Gaia-CRF3, and its properties in terms of the distributions in magnitude, colour, and astrometric quality. Compact extragalactic sources in Gaia DR3 were identified by positional cross-matching with 17 external catalogues of quasars (QSO) and active galactic nuclei (AGN), followed by astrometric filtering designed to remove stellar contaminants. Selecting a clean sample was favoured over including a higher number of extragalactic sources. For the final sample, the random and systematic errors in the proper motions are analysed, as well as the radio-optical offsets in position for sources in the third realisation of the International Celestial Reference Frame (ICRF3). The Gaia-CRF3 comprises about 1.6 million QSO-like sources, of which 1.2 million have five-parameter astrometric solutions in Gaia DR3 and 0.4 million have six-parameter solutions. The sources span the magnitude range G = 13 to 21 with a peak density at 20.6 mag, at which the typical positional uncertainty is about 1 mas. The proper motions show systematic errors on the level of 12 $μ$as yr${}^{-1}$ on angular scales greater than 15 deg. For the 3142 optical counterparts of ICRF3 sources in the S/X frequency bands, the median offset from the radio positions is about 0.5 mas, but exceeds 4 mas in either coordinate for 127 sources. We outline the future of the Gaia-CRF in the next Gaia data releases. △ Less

Submitted 30 October, 2022; v1 submitted 26 April, 2022; originally announced April 2022.

Journal ref: A&A 667, A148 (2022)

Spreading fronts of wetting liquid droplets: microscopic simulations and universal fluctuations

Authors: J. M. Marcos, P. Rodríguez-López, J. J. Melendez, R. Cuerno, J. J. Ruiz-Lorenzo

Abstract: We have used kinetic Monte Carlo (kMC) simulations of a lattice gas to study front fluctuations in the spreading of a non-volatile liquid droplet onto a solid substrate. Our results are consistent with a diffusive growth law for the radius of the precursor layer, $R \sim t^δ$, with $δ\approx 1/2$ in all the conditions considered for temperature and substrate wettability, in good agreement with pre… ▽ More We have used kinetic Monte Carlo (kMC) simulations of a lattice gas to study front fluctuations in the spreading of a non-volatile liquid droplet onto a solid substrate. Our results are consistent with a diffusive growth law for the radius of the precursor layer, $R \sim t^δ$, with $δ\approx 1/2$ in all the conditions considered for temperature and substrate wettability, in good agreement with previous studies. The fluctuations of the front exhibit kinetic roughening properties with exponent values which depend on temperature $T$, but become $T$-independent for sufficiently high $T$. Moreover, strong evidences of intrinsic anomalous scaling have been found, characterized by different values of the roughness exponent at short and large length scales. Although such a behavior differs from the scaling properties of the one-dimensional Kardar-Parisi-Zhang (KPZ) universality class, the front covariance and the probability distribution function of front fluctuations found in our kMC simulations do display KPZ behavior, agreeing with simulations of a continuum height equation proposed in this context. However, this equation does not feature intrinsic anomalous scaling, at variance with the discrete model. △ Less

Submitted 22 April, 2022; originally announced April 2022.

Comments: 15 pages and 14 figures. To be published in PRE

Journal ref: Physical Review E 105, 054801 (2022)

Improving position resolution of neutron detectors with ultra-thin B4C foils

Authors: N. F. V. Duarte, J. S. Marcos, A. Antognini, C. Klauser, S. A. Felix, C. M. B. Monteiro, F. D. Amaro

Abstract: A new technique for detection of slow neutrons with gaseous detectors using ultra-thin layers with 10B atoms is presented. The reaction between a thermal neutron and a 10B atom releases 2 secondary particles, namely a 7Li ion and an alpha particle, which due to momentum conservation are emitted in opposite directions, along the same line (back to back). Current boron coated neutron detectors are e… ▽ More A new technique for detection of slow neutrons with gaseous detectors using ultra-thin layers with 10B atoms is presented. The reaction between a thermal neutron and a 10B atom releases 2 secondary particles, namely a 7Li ion and an alpha particle, which due to momentum conservation are emitted in opposite directions, along the same line (back to back). Current boron coated neutron detectors are equipped with 10B films with thicknesses of several micrometers, deposited on very thick substrate plates. However, since the ranges of the 7Li ion and the alpha particle are of few micrometeres in most materials, one of these particles is always lost in the 10B layer or substrate. As such, these detectors lose the ability to reconstruct the reaction line of action and to precisely determine the neutron position, as only one of the two secondary particles track can be measured. With the technique now presented, the sum of the 10B layer and the substrate thicknesses is small enough to allow for both secondary particles to escape and ionize the gas in opposite sides of the 10B converter foil. Independent readout structures, one on each side of the 10B converter foil, detect each secondary particle and determine its track centroid and the deposited energy. Since the two secondary particles are emitted back to back, the neutron position can be obtained by combining the information recorded by the two readout structures. Through GEANT4 simulations, we verified that the spatial resolution can be significantly improved: our results show that, by using a B4C layer with a thickness of 1 micron on a 0.9 micron Mylar substrate, the spatial resolution can by improved by a factor of 8, compared to conventional detectors with thick 10B detection layers. △ Less

Submitted 26 February, 2022; originally announced February 2022.

Proceedings 10th International Workshop on Theorem Proving Components for Educational Software

Authors: João Marcos, Walther Neuper, Pedro Quaresma

Abstract: This EPTCS volume contains the proceedings of the ThEdu'21 workshop, promoted on 11 July 2021, as a satellite event of CADE-28. Due to the COVID-19 pandemic, CADE-28 and all its co-located events happened as virtual events. ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration. After the workshop an open call for pape… ▽ More This EPTCS volume contains the proceedings of the ThEdu'21 workshop, promoted on 11 July 2021, as a satellite event of CADE-28. Due to the COVID-19 pandemic, CADE-28 and all its co-located events happened as virtual events. ThEdu'21 was a vibrant workshop, with an invited talk by Gilles Dowek (ENS Paris-Saclay), eleven contributions, and one demonstration. After the workshop an open call for papers was issued and attracted 10 submissions, 7 of which have been accepted by the reviewers, and collected in the present post-proceedings volume. The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favouring software support for this transition by exploiting the power of theorem-proving technologies. The volume editors hope that this collection of papers will further promote the development of theorem-proving based software, and that it will collaborate on improving mutual understanding between computer scientists, mathematicians and stakeholders in education. △ Less

Submitted 2 February, 2022; originally announced February 2022.

Journal ref: EPTCS 354, 2022

JEM-EUSO Collaboration contributions to the 37th International Cosmic Ray Conference

Authors: G. Abdellaoui, S. Abe, J. H. Adams Jr., D. Allard, G. Alonso, L. Anchordoqui, A. Anzalone, E. Arnone, K. Asano, R. Attallah, H. Attoui, M. Ave Pernas, M. Bagheri, J. Baláz, M. Bakiri, D. Barghini, S. Bartocci, M. Battisti, J. Bayer, B. Beldjilali, T. Belenguer, N. Belkhalfa, R. Bellotti, A. A. Belov, K. Benmessai , et al. (267 additional authors not shown)

Abstract: Compilation of papers presented by the JEM-EUSO Collaboration at the 37th International Cosmic Ray Conference (ICRC), held on July 12-23, 2021 (online) in Berlin, Germany. Compilation of papers presented by the JEM-EUSO Collaboration at the 37th International Cosmic Ray Conference (ICRC), held on July 12-23, 2021 (online) in Berlin, Germany. △ Less

Submitted 28 January, 2022; originally announced January 2022.

Comments: html page with links to the JEM-EUSO Collaboration papers presented at ICRC-2021, Berlin, Germany

Proof Search on Bilateralist Judgments over Non-deterministic Semantics

Authors: Vitor Greati, Sérgio Marcelino, João Marcos

Abstract: The bilateralist approach to logical consequence maintains that judgments of different qualities should be taken into account in determining what-follows-from-what. We argue that such an approach may be actualized by a two-dimensional notion of entailment induced by semantic structures that also accommodate non-deterministic and partial interpretations, and propose a proof-theoretical apparatus to… ▽ More The bilateralist approach to logical consequence maintains that judgments of different qualities should be taken into account in determining what-follows-from-what. We argue that such an approach may be actualized by a two-dimensional notion of entailment induced by semantic structures that also accommodate non-deterministic and partial interpretations, and propose a proof-theoretical apparatus to reason over bilateralist judgments using symmetrical two-dimensional analytical Hilbert-style calculi. We also provide a proof-search algorithm for finite analytic calculi that runs in at most exponential time, in general, and in polynomial time when only rules having at most one formula in the succedent are present in the concerned calculus. △ Less

Submitted 17 July, 2021; originally announced July 2021.

MSC Class: 03B50 (Primary); 03B22 (Primary); 03A05 (Primary); 03B35 (Primary); 03B25 ACM Class: F.4.1; I.1.2

On Logics of Perfect Paradefinite Algebras

Authors: Joel Gomes, Vitor Greati, Sérgio Marcelino, João Marcos, Umberto Rivieccio

Abstract: The present study shows how to enrich De Morgan algebras with a perfection operator that allows one to express the Boolean properties of negation-consistency and negation-determinedness. The variety of perfect paradefinite algebras thus obtained (PP-algebras) is shown to be term-equivalent to the variety of involutive Stone algebras, introduced by R. Cignoli and M. Sagastume, and more recently stu… ▽ More The present study shows how to enrich De Morgan algebras with a perfection operator that allows one to express the Boolean properties of negation-consistency and negation-determinedness. The variety of perfect paradefinite algebras thus obtained (PP-algebras) is shown to be term-equivalent to the variety of involutive Stone algebras, introduced by R. Cignoli and M. Sagastume, and more recently studied from a logical perspective by M. Figallo-L. Cantú and by S. Marcelino-U. Rivieccio. This equivalence plays an important role in the investigation of the 1-assertional logic and of the order-preserving logic associated to PP-algebras. The latter logic (here called PP<=) is characterized by a single 6-valued matrix and is shown to be a Logic of Formal Inconsistency and Formal Undeterminedness. We axiomatize PP<= by means of an analytic finite Hilbert-style calculus, and we present an axiomatization procedure that covers the logics corresponding to other classes of De Morgan algebras enriched by a perfection operator. △ Less

Submitted 8 April, 2022; v1 submitted 17 June, 2021; originally announced June 2021.

Comments: In Proceedings LSFA 2021, arXiv:2204.03415

Journal ref: EPTCS 357, 2022, pp. 56-76

Proceedings 9th International Workshop on Theorem Proving Components for Educational Software

Authors: Pedro Quaresma, Walther Neuper, João Marcos

Abstract: The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu'20) was scheduled to happen on June 29 as a satellite of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking… ▽ More The 9th International Workshop on Theorem-Proving Components for Educational Software (ThEdu'20) was scheduled to happen on June 29 as a satellite of the IJCAR-FSCD 2020 joint meeting, in Paris. The COVID-19 pandemic came by surprise, though, and the main conference was virtualised. Fearing that an online meeting would not allow our community to fully reproduce the usual face-to-face networking opportunities of the ThEdu initiative, the Steering Committee of ThEdu decided to cancel our workshop. Given that many of us had already planned and worked for that moment, we decided that ThEdu'20 could still live in the form of an EPTCS volume. The EPTCS concurred with us, recognising this very singular situation, and accepted our proposal of organising a special issue with papers submitted to ThEdu'20. An open call for papers was then issued, and attracted five submissions, all of which have been accepted by our reviewers, who produced three careful reports on each of the contributions. The resulting revised papers are collected in the present volume. We, the volume editors, hope that this collection of papers will help further promoting the development of theorem-proving-based software, and that it will collaborate to improve the mutual understanding between computer mathematicians and stakeholders in education. With some luck, we would actually expect that the very special circumstances set up by the worst sanitary crisis in a century will happen to reinforce the need for the application of certified components and of verification methods for the production of educational software that would be available even when the traditional on-site learning experiences turn out not to be recommendable. △ Less

Submitted 27 October, 2020; originally announced October 2020.

Journal ref: EPTCS 328, 2020

Proceedings 8th International Workshop on Theorem Proving Components for Educational Software

Authors: Pedro Quaresma, Walther Neuper, João Marcos

Abstract: This EPTCS volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. After the workshop an open call f… ▽ More This EPTCS volume contains the proceedings of the ThEdu'19 workshop, promoted on August 25, 2019, as a satellite event of CADE-27, in Natal, Brazil. Representing the eighth installment of the ThEdu series, ThEdu'19 was a vibrant workshop, with an invited talk by Sarah Winkler, four contributions, and the first edition of a Geometry Automated Provers Competition. After the workshop an open call for papers was issued and attracted seven submissions, six of which have been accepted by the reviewers, and collected in the present post-proceedings volume. The ThEdu series pursues the smooth transition from an intuitive way of doing mathematics at secondary school to a more formal approach to the subject in STEM education, while favoring software support for this transition by exploiting the power of theorem-proving technologies. The volume editors hope that this collection of papers will further promote the development of theorem-proving-based software, and that it will collaborate on improving mutual understanding between computer mathematicians and stakeholders in education. △ Less

Submitted 26 February, 2020; originally announced February 2020.

Journal ref: EPTCS 313, 2020

Contributions to the 36th International Cosmic Ray Conference (ICRC 2019) of the JEM-EUSO Collaboration

Authors: G. Abdellaoui, S. Abe, J. H. Adams Jr., A. Ahriche, D. Allard, L. Allen, G. Alonso, L. Anchordoqui, A. Anzalone, Y. Arai, K. Asano, R. Attallah, H. Attoui, M. Ave Pernas, S. Bacholle, M. Bakiri, P. Baragatti, P. Barrillon, S. Bartocci, J. Bayer, B. Beldjilali, T. Belenguer, N. Belkhalfa, R. Bellotti, A. Belov , et al. (287 additional authors not shown)

Abstract: Compilation of papers presented by the JEM-EUSO Collaboration at the 36th International Cosmic Ray Conference (ICRC), held July 24 through August 1, 2019 in Madison, Wisconsin. Compilation of papers presented by the JEM-EUSO Collaboration at the 36th International Cosmic Ray Conference (ICRC), held July 24 through August 1, 2019 in Madison, Wisconsin. △ Less

Submitted 18 December, 2019; originally announced December 2019.

Comments: links to the 24 papers published in arXiv

Journal ref: all published in PoS(ICRC2019)

What is a logical theory? On theories containing assertions and denials

Authors: Carolina Blasio, Carlos Caleiro, João Marcos

Abstract: The standard notion of formal theory, in Logic, is in general biased exclusively towards assertion: it commonly refers only to collections of assertions that any agent who accepts the generating axioms of the theory should also be committed to accept. In reviewing the main abstract approaches to the study of logical consequence, we point out why this notion of theory is unsatisfactory at multiple… ▽ More The standard notion of formal theory, in Logic, is in general biased exclusively towards assertion: it commonly refers only to collections of assertions that any agent who accepts the generating axioms of the theory should also be committed to accept. In reviewing the main abstract approaches to the study of logical consequence, we point out why this notion of theory is unsatisfactory at multiple levels, and introduce a novel notion of theory that attacks the shortcomings of the received notion by allowing one to take both assertions and denials on a par. This novel notion of theory is based on a bilateralist approach to consequence operators, which we hereby introduce, and whose main properties we investigate in the present paper. △ Less

Submitted 3 April, 2019; v1 submitted 6 March, 2019; originally announced March 2019.

MSC Class: 03Bxx

SiPM-based neutron Anger camera with auto-calibration capabilities

Authors: A. Morozov, J. Marcos, L. Margato, D. Roulier, V. Solovov

Abstract: We present characterization results of a neutron Anger camera based on a lithium-6 loaded cerium activated silicate glass scintillator (33.3 x 33.3 x 1 mm3) and an array of 64 silicon photomultipliers. Reconstruction of the scintillation events is performed with a statistical method, implemented on a graphics processing unit (GPU). We demonstrate that the light response model of the detector can b… ▽ More We present characterization results of a neutron Anger camera based on a lithium-6 loaded cerium activated silicate glass scintillator (33.3 x 33.3 x 1 mm3) and an array of 64 silicon photomultipliers. Reconstruction of the scintillation events is performed with a statistical method, implemented on a graphics processing unit (GPU). We demonstrate that the light response model of the detector can be obtained from flood irradiation calibration data using an unsupervised iterative procedure. The useful field of view is 28 x 28 mm2. The spatial resolution measured at 2.5 A neutron beam is better than 0.6 mm FWHM and the energy resolution at the neutron peak is 11%. △ Less

Submitted 12 February, 2019; originally announced February 2019.

Combining fragments of classical logic: When are interaction principles needed?

Authors: Carlos Caleiro, Sérgio Marcelino, João Marcos

Abstract: We investigate the combination of fragments of classical logic as a way of conservatively extending a given Boolean logic by the addition of new connectives, and we precisely characterize the circumstances in which such a combination produces the corresponding fragment of classical logic over the signature containing connectives from both fragments given as input. If the thereby produced combined… ▽ More We investigate the combination of fragments of classical logic as a way of conservatively extending a given Boolean logic by the addition of new connectives, and we precisely characterize the circumstances in which such a combination produces the corresponding fragment of classical logic over the signature containing connectives from both fragments given as input. If the thereby produced combined fragment is only incompletely characterized by the components given as input, this means that connectives from one component need to interact with connectives from the other component, giving rise to interaction principles. The main contributions strongly rely on the (well-known) description of the 2-valued clones made by Post, on the (not so well-known) axiomatization procedures for 2-valued matrices laid out by Rautenberg, and on Avron's non-deterministic matrices, which have (recently) been used to produce a significant advance on the understanding of the semantics of fibring. △ Less

Submitted 16 October, 2018; v1 submitted 13 October, 2018; originally announced October 2018.

Comments: Authors' affiliations and funding information added

MSC Class: 03B20; 03B50; 03B62

First observations of speed of light tracks by a fluorescence detector looking down on the atmosphere

Authors: G. Abdellaoui, S. Abe, J. H. Adams Jr., A. Ahriche, D. Allard, L. Allen, G. Alonso, L. Anchordoqui, A. Anzalone, Y. Arai, K. Asano, R. Attallah, H. Attoui, M. Ave Pernas, S. Bacholle, M. Bakiri, P. Baragatti, P. Barrillon, S. Bartocci, J. Bayer, B. Beldjilali, T. Belenguer, N. Belkhalfa, R. Bellotti, A. Belov , et al. (289 additional authors not shown)

Abstract: EUSO-Balloon is a pathfinder mission for the Extreme Universe Space Observatory onboard the Japanese Experiment Module (JEM-EUSO). It was launched on the moonless night of the 25$^{th}$ of August 2014 from Timmins, Canada. The flight ended successfully after maintaining the target altitude of 38 km for five hours. One part of the mission was a 2.5 hour underflight using a helicopter equipped with… ▽ More EUSO-Balloon is a pathfinder mission for the Extreme Universe Space Observatory onboard the Japanese Experiment Module (JEM-EUSO). It was launched on the moonless night of the 25$^{th}$ of August 2014 from Timmins, Canada. The flight ended successfully after maintaining the target altitude of 38 km for five hours. One part of the mission was a 2.5 hour underflight using a helicopter equipped with three UV light sources (LED, xenon flasher and laser) to perform an inflight calibration and examine the detectors capability to measure tracks moving at the speed of light. We describe the helicopter laser system and details of the underflight as well as how the laser tracks were recorded and found in the data. These are the first recorded laser tracks measured from a fluorescence detector looking down on the atmosphere. Finally, we present a first reconstruction of the direction of the laser tracks relative to the detector. △ Less

Submitted 7 August, 2018; originally announced August 2018.

Comments: 18 pages, 14 figures

Journal ref: 2018 JINST 13 P05023

Nelson's Logic S

Authors: Thiago Nascimento, Umberto Rivieccio, Joao Marcos, Matthew Spinks

Abstract: Besides the better-known Nelson logic (N3) and paraconsistent logic (N4), in 1959 David Nelson introduced, with motivations of realizability and constructibility, a logic called S. The logic S was originally presented by means of a calculus (crucially lacking the contraction rule) with infinitely many rule schemata and no semantics (other than the intended interpretation into Arithmetic.) We look… ▽ More Besides the better-known Nelson logic (N3) and paraconsistent logic (N4), in 1959 David Nelson introduced, with motivations of realizability and constructibility, a logic called S. The logic S was originally presented by means of a calculus (crucially lacking the contraction rule) with infinitely many rule schemata and no semantics (other than the intended interpretation into Arithmetic.) We look here at the propositional fragment of S, showing that it is algebraizable (in fact, implicative), in the sense of Blok and Pigozzi, with respect to a variety of three-potent involutive residuated lattices. We thus introduce the first known algebraic semantics for S as well as a finite Hilbert-style calculus equivalent to Nelson's presentation; this also allows us to clarify the relation between S and the other two Nelson logics N3 and N4. △ Less

Submitted 21 September, 2019; v1 submitted 28 March, 2018; originally announced March 2018.

Comments: 20 pages, 1 figure

Algebraic Semantics for Nelson's Logic S

Authors: Thiago Nascimento, Umberto Rivieccio, João Marcos, Matthew Spinks

Abstract: Besides the better-known Nelson's Logic and Paraconsistent Nelson's Logic, in "Negation and separation of concepts in constructive systems" (1959), David Nelson introduced a logic called S with the aim of analyzing the constructive content of provable negation statements in mathematics. Motivated by results from Kleene, in "On the Interpretation of Intuitionistic Number Theory" (1945), Nelson inve… ▽ More Besides the better-known Nelson's Logic and Paraconsistent Nelson's Logic, in "Negation and separation of concepts in constructive systems" (1959), David Nelson introduced a logic called S with the aim of analyzing the constructive content of provable negation statements in mathematics. Motivated by results from Kleene, in "On the Interpretation of Intuitionistic Number Theory" (1945), Nelson investigated a more symmetric recursive definition of truth, according to which a formula could be either primitively verified or refuted. The logic S was defined by means of a calculus lacking the contraction rule and having infinitely many schematic rules, and no semantics was provided. This system received little attention from researchers and it even remained unnoticed that on its original presentation it was inconsistent. Fortunately, the inconsistency was caused by typos and by a rule whose hypothesis and conclusion were swapped.We investigate in the present study a corrected version of the logic S, and focus at its propositional fragment, showing that it is algebraizable (in fact, implicative) with respect to a certain special class of involutive residuated lattices. We thus introduce the first (algebraic) semantics for S as well as a finite Hilbert-style calculus equivalent to Nelson's presentation. We also compare S with the other two above-mentioned logics of the Nelson family. △ Less

Submitted 10 June, 2018; v1 submitted 28 March, 2018; originally announced March 2018.

Comments: 16 pages

Semi-BCI Algebras

Authors: Regivan H. N. Santiago, Benjamin Bedregal, João Marcos, Carlos Caleiro, Jocivania Pinheiro

Abstract: The notion of semi-BCI algebras is introduced and some of its properties are investigated. This algebra is another generalization for BCI-algebras. It arises from the "intervalization" of BCI algebras. Semi-BCI have a similar structure to Pseudo-BCI algebras however they are not the same. In this paper we also provide an investigation on the similarity between these classes of algebras by showing… ▽ More The notion of semi-BCI algebras is introduced and some of its properties are investigated. This algebra is another generalization for BCI-algebras. It arises from the "intervalization" of BCI algebras. Semi-BCI have a similar structure to Pseudo-BCI algebras however they are not the same. In this paper we also provide an investigation on the similarity between these classes of algebras by showing how they relate to the process of intervalization. △ Less

Submitted 13 March, 2018; originally announced March 2018.

Comments: 30 pages, 1 figure

Merging fragments of classical logic

Authors: Carlos Caleiro, Sérgio Marcelino, João Marcos

Abstract: We investigate the possibility of extending the non-functionally complete logic of a collection of Boolean connectives by the addition of further Boolean connectives that make the resulting set of connectives functionally complete. More precisely, we will be interested in checking whether an axiomatization for Classical Propositional Logic may be produced by merging Hilbert-style calculi for two d… ▽ More We investigate the possibility of extending the non-functionally complete logic of a collection of Boolean connectives by the addition of further Boolean connectives that make the resulting set of connectives functionally complete. More precisely, we will be interested in checking whether an axiomatization for Classical Propositional Logic may be produced by merging Hilbert-style calculi for two disjoint incomplete fragments of it. We will prove that the answer to that problem is a negative one, unless one of the components includes only top-like connectives. △ Less

Submitted 27 June, 2017; originally announced June 2017.

Comments: submitted to FroCoS 2017

MSC Class: 03B05 (Primary); 03B20; 03C05 (Secondary) ACM Class: F.4.1; I.2.3

Sequent systems for negative modalities

Authors: Ori Lahav, João Marcos, Yoni Zohar

Abstract: Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate semantics and proof systems, whose philosophical interpretations and computational properties are found wanting. In this paper we investigate congruential non-… ▽ More Non-classical negations may fail to be contradictory-forming operators in more than one way, and they often fail also to respect fundamental meta-logical properties such as the replacement property. Such drawbacks are witnessed by intricate semantics and proof systems, whose philosophical interpretations and computational properties are found wanting. In this paper we investigate congruential non-classical negations that live inside very natural systems of normal modal logics over complete distributive lattices; these logics are further enriched by adjustment connectives that may be used for handling reasoning under uncertainty caused by inconsistency or undeterminedness. Using such straightforward semantics, we study the classes of frames characterized by seriality, reflexivity, functionality, symmetry, transitivity, and some combinations thereof, and discuss what they reveal about sub-classical properties of negation. To the logics thereby characterized we apply a general mechanism that allows one to endow them with analytic ordinary sequent systems, most of which are even cut-free. We also investigate the exact circumstances that allow for classical negation to be explicitly defined inside our logics. △ Less

Submitted 25 July, 2017; v1 submitted 15 June, 2017; originally announced June 2017.

Comments: 37 pages, preliminary version, to appear in Logica Universalis. arXiv admin note: substantial text overlap with arXiv:1606.04006

MSC Class: 03B45 ACM Class: F.4.1

Iterative reconstruction of SiPM light response functions in a square-shaped compact gamma camera

Authors: A. Morozov, F. Alves, J. Marcos, R. Martins, L. Pereira, V. Solovov, V. Chepel

Abstract: Compact gamma cameras with a square-shaped monolithic scintillator crystal and an array of silicon photomultipliers (SiPMs) are actively being developed for applications in areas such as small animal imaging, cancer diagnostics and radiotracer guided surgery. Statistical methods of position reconstruction, which are potentially superior to the traditional centroid method, require accurate knowledg… ▽ More Compact gamma cameras with a square-shaped monolithic scintillator crystal and an array of silicon photomultipliers (SiPMs) are actively being developed for applications in areas such as small animal imaging, cancer diagnostics and radiotracer guided surgery. Statistical methods of position reconstruction, which are potentially superior to the traditional centroid method, require accurate knowledge of the spatial response of each photomultiplier. Using both Monte Carlo simulations and experimental data obtained with a camera prototype, we show that the spatial response of all photomultipliers (light response functions) can be parameterized with axially symmetric functions obtained iteratively from flood field irradiation data. The study was performed with a camera prototype equipped with a 30 x 30 x 2 mm3 LYSO crystal and an 8 x 8 array of SiPMs for 140 keV gamma rays. The simulations demonstrate that the images, reconstructed with the maximum likelihood method using the response obtained with the iterative approach, exhibit only minor distortions: the average difference between the reconstructed and the true positions in X and Y directions does not exceed 0.2 mm in the central area of 22 x 22 mm2 and 0.4 mm at the periphery of the camera. A similar level of image distortions is shown experimentally with the camera prototype. △ Less

Submitted 9 October, 2016; originally announced October 2016.

It ain't necessarily so: Basic sequent systems for negative modalities

Authors: Ori Lahav, João Marcos, Yoni Zohar

Abstract: We look at non-classical negations and their corresponding adjustment connectives from a modal viewpoint, over complete distributive lattices, and apply a very general mechanism in order to offer adequate analytic proof systems to logics that are based on them. Defining non-classical negations within usual modal semantics automatically allows one to treat equivalent formulas as synonymous, and to… ▽ More We look at non-classical negations and their corresponding adjustment connectives from a modal viewpoint, over complete distributive lattices, and apply a very general mechanism in order to offer adequate analytic proof systems to logics that are based on them. Defining non-classical negations within usual modal semantics automatically allows one to treat equivalent formulas as synonymous, and to have a natural justification for a global version of the contraposition rule. From that perspective, our study offers a particularly useful environment in which negative modalities and their companions may be used for dealing with inconsistency and indeterminacy. After investigating modal logics based on arbitrary frames, we extend the results to serial frames, reflexive frames, functional frames, and symmetric frames. In each case we also investigate when and how classical negation may thereby be defined. △ Less

Submitted 23 June, 2016; v1 submitted 13 June, 2016; originally announced June 2016.

Comments: 20 pages, to appear in Advances in Modal Logic Vol 11 (a few typos corrected)

MSC Class: 03B45 ACM Class: F.4.1

Cultural Anthropology through the Lens of Wikipedia: Historical Leader Networks, Gender Bias, and News-based Sentiment

Authors: Peter A. Gloor, Joao Marcos, Patrick M. de Boer, Hauke Fuehres, Wei Lo, Keiichi Nemoto

Abstract: In this paper we study the differences in historical World View between Western and Eastern cultures, represented through the English, the Chinese, Japanese, and German Wikipedia. In particular, we analyze the historical networks of the World's leaders since the beginning of written history, comparing them in the different Wikipedias and assessing cultural chauvinism. We also identify the most inf… ▽ More In this paper we study the differences in historical World View between Western and Eastern cultures, represented through the English, the Chinese, Japanese, and German Wikipedia. In particular, we analyze the historical networks of the World's leaders since the beginning of written history, comparing them in the different Wikipedias and assessing cultural chauvinism. We also identify the most influential female leaders of all times in the English, German, Spanish, and Portuguese Wikipedia. As an additional lens into the soul of a culture we compare top terms, sentiment, emotionality, and complexity of the English, Portuguese, Spanish, and German Wikinews. △ Less

Submitted 31 July, 2015; originally announced August 2015.

TryLogic tutorial: an approach to Learning Logic by proving and refuting

Authors: Patrick Terrematte, João Marcos

Abstract: Aiming to offer a framework for blended learning to the teaching of proof theory, the present paper describes an interactive tutorial, called \textsc{TryLogic}, teaching how to solve logical conjectures either by proofs or refutations. The paper also describes the integration of our infrastructure with the Virtual Learning Environment \texttt{Moodle} through the IMS Learning Tools Interoperability… ▽ More Aiming to offer a framework for blended learning to the teaching of proof theory, the present paper describes an interactive tutorial, called \textsc{TryLogic}, teaching how to solve logical conjectures either by proofs or refutations. The paper also describes the integration of our infrastructure with the Virtual Learning Environment \texttt{Moodle} through the IMS Learning Tools Interoperability specification, and evaluates the tool we have developed. △ Less

Submitted 13 July, 2015; originally announced July 2015.

Comments: Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, João Marcos, María Manzano, Sophie Pinchinat, François Schwarzentruber

ACM Class: K.3.1; F.4.1

Fail better: What formalized math can teach us about learning

Authors: João Marcos

Abstract: Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in as much detail as our need for eliminating risk might require. For those who do not happen to have direct access to the realm of mathematical truths, the moder… ▽ More Real-life conjectures do not come with instructions saying whether they they should be proven or, instead, refuted. Yet, as we now know, in either case the final argument produced had better be not just convincing but actually verifiable in as much detail as our need for eliminating risk might require. For those who do not happen to have direct access to the realm of mathematical truths, the modern field of formalized mathematics has quite a few lessons to contribute, and one might pay heed to what it has to say, for instance, about: the importance of employing proof strategies; the fine control of automation in unraveling the structure of a certain proof object; reasoning forward from the givens and backward from the goals, in develo** proof scripts; knowing when and how definitions and identities apply in a helpful way, and when they do not apply; seeing proofs [and refutations] as dynamical objects, not reflected by the static derivation trees that Proof Theory wants them to be. I believe that the great challenge for teachers and learners resides currently less on the availability of suitable generic tools than in combining them wisely in view of their preferred education paradigms and introducing them in a way that best fits their specific aims, possibly with the help of intelligent online interactive tutoring systems. As a proof of concept, a computerized proof assistant that makes use of several successful tools already freely available on the market and that takes into account some of the above findings about teaching and learning Logic is hereby introduced. To fully account for our informed intuitions on the subject it would seem that a little bit extra technology would still be inviting, but no major breakthrough is really needed: We are talking about tools that are already within our reach to develop, as the fruits of collaborative effort. △ Less

Submitted 17 July, 2015; v1 submitted 13 July, 2015; originally announced July 2015.

Comments: Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, João Marcos, María Manzano, Sophie Pinchinat, François Schwarzentruber

ACM Class: K.3.1; F.4.1

Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics

Authors: Carlos Caleiro, João Marcos, Marco Volpe

Abstract: The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent… ▽ More The paper is a contribution both to the theoretical foundations and to the actual construction of efficient automatizable proof procedures for non-classical logics. We focus here on the case of finite-valued logics, and exhibit: (i) a mechanism for producing a classic-like description of them in terms of an effective variety of bivalent semantics; (ii) a mechanism for extracting, from the bivalent semantics so obtained, uniform (classically-labeled) cut-free standard analytic tableaux with possibly branching invertible rules and paired with proof strategies designed to guarantee termination of the associated proof procedure; (iii) a mechanism to also provide, for the same logics, uniform cut-based tableau systems with linear rules. The latter tableau systems are shown to be adequate even when restricted to analytic cuts, and they are also shown to polynomially simulate truth-tables, a feature that is not enjoyed by the former standard type of tableau systems (not even in the 2-valued case). The results are based on useful generalizations of the notions of analyticity and compositionality, and illustrate a theory that applies to many other classes of non-classical logics. △ Less

Submitted 16 August, 2014; originally announced August 2014.

MSC Class: 03B50 (Primary); 03B35 (Secondary)

Clausal Resolution for Modal Logics of Confluence

Authors: Cláudia Nalon, João Marcos, Clare Dixon

Abstract: We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms th… ▽ More We present a clausal resolution-based method for normal multimodal logics of confluence, whose Kripke semantics are based on frames characterised by appropriate instances of the Church-Rosser property. Here we restrict attention to eight families of such logics. We show how the inference rules related to the normal logics of confluence can be systematically obtained from the parametrised axioms that characterise such systems. We discuss soundness, completeness, and termination of the method. In particular, completeness can be modularly proved by showing that the conclusions of each newly added inference rule ensures that the corresponding conditions on frames hold. Some examples are given in order to illustrate the use of the method. △ Less

Submitted 1 May, 2014; originally announced May 2014.

Comments: 15 pages, 1 figure. Preprint of the paper accepted to IJCAR 2014

On Achievable Rates of the Two-user Symmetric Gaussian Interference Channel

Authors: Omar Mehanna, John Marcos, Nihar **dal

Abstract: We study the Han-Kobayashi (HK) achievable sum rate for the two-user symmetric Gaussian interference channel. We find the optimal power split ratio between the common and private messages (assuming no time-sharing), and derive a closed form expression for the corresponding sum rate. This provides a finer understanding of the achievable HK sum rate, and allows for precise comparisons between this s… ▽ More We study the Han-Kobayashi (HK) achievable sum rate for the two-user symmetric Gaussian interference channel. We find the optimal power split ratio between the common and private messages (assuming no time-sharing), and derive a closed form expression for the corresponding sum rate. This provides a finer understanding of the achievable HK sum rate, and allows for precise comparisons between this sum rate and that of orthogonal signaling. One surprising finding is that despite the fact that the channel is symmetric, allowing for asymmetric power split ratio at both users (i.e., asymmetric rates) can improve the sum rate significantly. Considering the high SNR regime, we specify the interference channel value above which the sum rate achieved using asymmetric power splitting outperforms the symmetric case. △ Less

Submitted 12 October, 2010; originally announced October 2010.

Comments: 7 pages, to appear in Allerton 2010

Automatic Generation of Proof Tactics for Finite-Valued Logics

Authors: João Marcos

Abstract: A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful systems resides in their responsiveness to extensibility of their reasoning capabilities, being designed over rule-based programming languages that allow the us… ▽ More A number of flexible tactic-based logical frameworks are nowadays available that can implement a wide range of mathematical theories using a common higher-order metalanguage. Used as proof assistants, one of the advantages of such powerful systems resides in their responsiveness to extensibility of their reasoning capabilities, being designed over rule-based programming languages that allow the user to build her own `programs to construct proofs' - the so-called proof tactics. The present contribution discusses the implementation of an algorithm that generates sound and complete tableau systems for a very inclusive class of sufficiently expressive finite-valued propositional logics, and then illustrates some of the challenges and difficulties related to the algorithmic formation of automated theorem proving tactics for such logics. The procedure on whose implementation we will report is based on a generalized notion of analyticity of proof systems that is intended to guarantee termination of the corresponding automated tactics on what concerns theoremhood in our targeted logics. △ Less

Submitted 25 March, 2010; originally announced March 2010.

Journal ref: EPTCS 21, 2010, pp. 91-98

Specific permutation polynomials over finite fields

Authors: Jose E. Marcos

Abstract: We present new classes of permutation polynomials over finite fields. We present new classes of permutation polynomials over finite fields. △ Less

Submitted 9 June, 2010; v1 submitted 15 October, 2008; originally announced October 2008.

Comments: Withdrawn by the author [conflict of copyright]

MSC Class: 11T06

Acoustic emission across the magnetostructural transition of the giant magnetocaloric Gd5Si2Ge2 compound

Authors: Francisco-Jose Perez-Reche, Felix Casanova, Eduard Vives, Lluis Manosa, Antoni Planes, Jordi Marcos, Xavier Batlle, Amilcar Labarta

Abstract: We report on the existence of acoustic emission during the paramagnetic-monoclinic to ferromagnetic-orthorhombic magnetostructural phase transition in the giant magnetocaloric Gd5Si2Ge2 compound. The transition kinetics have been analyzed from the detected acoustic signals. It is shown that this transition proceeds by avalanches between metastable states. We report on the existence of acoustic emission during the paramagnetic-monoclinic to ferromagnetic-orthorhombic magnetostructural phase transition in the giant magnetocaloric Gd5Si2Ge2 compound. The transition kinetics have been analyzed from the detected acoustic signals. It is shown that this transition proceeds by avalanches between metastable states. △ Less

Submitted 14 December, 2005; originally announced December 2005.

Comments: 5 pages, 4 figures

Disorder induced critical phenomena in magnetically glassy Cu-Al-Mn alloys

Authors: Jordi Marcos, Eduard Vives, Lluis Manosa, Mehmet Acet, Eyup Duman, Michel Morin, Vaclav Novak, Antoni Planes

Abstract: Measurements of magnetic hysteresis loops in Cu-Al-Mn alloys of different Mn content at low temperatures are presented. The loops are smooth and continuous above a certain temperature, but exhibit a magnetization discontinuity below that temperature. Scaling analysis suggest that this system displays a disorder induced phase transition line. Measurements allow to determine the critical exponents… ▽ More Measurements of magnetic hysteresis loops in Cu-Al-Mn alloys of different Mn content at low temperatures are presented. The loops are smooth and continuous above a certain temperature, but exhibit a magnetization discontinuity below that temperature. Scaling analysis suggest that this system displays a disorder induced phase transition line. Measurements allow to determine the critical exponents $β=0.03\pm 0.01$ and $βδ= 0.4 \pm 0.1$ in agreement with those reported recently [Berger et al., Phys. Rev. Lett. {\bf 85}, 4176 (2000)] △ Less

Submitted 13 September, 2002; originally announced September 2002.

Comments: 4 pages, 5 figures

Martensitic transition and magnetoresistance in a Cu-Al-Mn shape memory alloy. Influence of aging

Authors: Jordi Marcos, Antoni Planes, Lluís Mañosa, Amílcar Labarta, Bart Jan Hattink

Abstract: We have studied the effect of ageing within the miscibility gap on the electric, magnetic and thermodynamic properties of a non-stoichiometric Heusler Cu-Al-Mn shape-memory alloy, which undergoes a martensitic transition from a $bcc$-based ($β$-phase) towards a close-packed structure ($M$-phase). Negative magnetoresistance which shows an almost linear dependence on the square of magnetization wi… ▽ More We have studied the effect of ageing within the miscibility gap on the electric, magnetic and thermodynamic properties of a non-stoichiometric Heusler Cu-Al-Mn shape-memory alloy, which undergoes a martensitic transition from a $bcc$-based ($β$-phase) towards a close-packed structure ($M$-phase). Negative magnetoresistance which shows an almost linear dependence on the square of magnetization with different slopes in the $M$- and $β$-phases, was observed. This magnetoresistive effect has been associated with the existence of Mn-rich clusters with the Cu$_2$AlMn-structure. The effect of an applied magnetic field on the martensitic transition has also been studied. The entropy change between the $β$- and $M$-phases shows negligible dependence on the magnetic field but it decreases significantly with annealing time within the miscibility gap. Such a decrease is due to the increasing amount of Cu$_2$MnAl-rich domains that do not transform martensitically. △ Less

Submitted 10 July, 2002; originally announced July 2002.

Comments: 9 pages, 9 figures, accepted for publication in PRB

A Taxonomy of C-systems

Authors: W. A. Carnielli, J. Marcos

Abstract: A thorough investigation of the foundations of paraconsistent logics. Relations between logical principles are formally studied, a novel notion of consistency is introduced, the logics of formal inconsistency, and the subclasses of C-systems and dC-systems are defined and studied. An enormous variety of paraconsistent logics in the literature is shown to constitute C-systems. A thorough investigation of the foundations of paraconsistent logics. Relations between logical principles are formally studied, a novel notion of consistency is introduced, the logics of formal inconsistency, and the subclasses of C-systems and dC-systems are defined and studied. An enormous variety of paraconsistent logics in the literature is shown to constitute C-systems. △ Less

Submitted 6 August, 2001; originally announced August 2001.

Comments: 94 pages. This file was produced by Word, if you have trouble reading it contact <[email protected]>

MSC Class: 03B53 (Primary) 03B22 (Secondary)

Journal ref: In: "Paraconsistency: The Logical Way to the Inconsistent", Proceedings of the II World Congress on Paraconsistency (WCP'2000), Marcel Dekker, 2001

Magnetic phase separation in ordered alloys

Authors: Jordi Marcos, Eduard Vives, Teresa Castan

Abstract: We present a lattice model to study the equilibrium phase diagram of ordered alloys with one magnetic component that exhibits a low temperature phase separation between paramagnetic and ferromagnetic phases. The model is constructed from the experimental facts observed in Cu$_{3-x}$AlMn$_{x}$ and it includes coupling between configurational and magnetic degrees of freedom which are appropriated… ▽ More We present a lattice model to study the equilibrium phase diagram of ordered alloys with one magnetic component that exhibits a low temperature phase separation between paramagnetic and ferromagnetic phases. The model is constructed from the experimental facts observed in Cu$_{3-x}$AlMn$_{x}$ and it includes coupling between configurational and magnetic degrees of freedom which are appropriated for reproducing the low temperature miscibility gap. The essential ingredient for the occurrence of such a coexistence region is the development of ferromagnetic order induced by the long-range atomic order of the magnetic component. A comparative study of both mean-field and Monte Carlo solutions is presented. Moreover, the model may enable the study of the structure of the ferromagnetic domains embedded in the non-magnetic matrix. This is relevant in relation to phenomena such as magnetoresistance and paramagnetism. △ Less

Submitted 3 May, 2001; originally announced May 2001.

Comments: 12 pages, 11 figures, accepted in Phys. Rev. B