Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
781
datasets available to search
ShareScore release 0.9.0
Dataset results
781 results for “proofs”
Virtual Reality Dataset used for Proof of Concept in the Validation of the Conflict Detection and Resolution Use Case (ARTIMATION)
<p>This dataset contains the <strong>dataset </strong>used in the Virtual Reality POC for the validation of the Conflict Detection and Resolution (CD&R) use case.</p> <p>This dataset represent a extract of different (using K-means) candidate solution, either good or bad ones.</p>
Embodied Spatial Navigation Training in Mild Cognitive Impairment: A Proof-of-Concept Trial
<p>Raw data of included cognitive test and VR data Starting Grant Ricerca Finalizzata, code: SG-2018-12368175</p>
2023 HYDRAS Proof of concept experiment with soybean genotypes
<h2>Description</h2> <p>This data sets contains metadata and data of the <strong>2023_POC experiment in the HYDRAS facility</strong>.</p> <p> The 2023 proof-of-concept study in hydras tested all standard field-phenotyping measurement types available in the infrastructure with 3 contrasting varieties of soybean + a control and a drought treatment using rain-out shelters. Start date: 23/5/2023, End dat: 4/10/2023. Location: Melle, Belgium. </p> <p>Data set contains: UAV sensor data, Electrical Resistivity Tomography data, soil point sensor data (water content, water potential and temperature), weather data, yield data and associated experimental information. </p> <h2>Content</h2> <ul> <li>2023_POC_metadata.xlsx contains all information about the experiment (goal, design, sensors, treatments, biological material, ...) and about the associated data files.</li> <li>Subfolder SPATIAL_INFO contains all spatial information about the experimental layout (location of field, plots, sensors, transects, ...) in GEOJSON files</li> <li>Other subfolders contain the actual data from various sources as .csv files. </li> </ul>
Supplement to "Proof of concept for Bayesian inference of dynamic rating curve uncertainty" (v3)
<div>This deposit contains part of the updated supplement to “Proof of concept for Bayesian inference of dynamic rating curve uncertainty” (<a href="https://www.tandfonline.com/doi/full/10.1080/02626667.2024.2401094" target="_blank" rel="noopener">Cornelio et al. 2024, HSJ</a>). This version, in particular, contains two files in which the following changes were made from the earlier version (v2.0.1):</div> <div> <ul> <li><strong><em>250117_Lbn_RC_new.R</em></strong> is the updated R code. The argument for the random number generator (RNG) kind is defined for the set.seed() functions used in the script. </li> <li><strong><em>Lbn-DMs-csv0.csv</em></strong> is the updated input file containing the stage-discharge gaugings. The column for the stage values has been renamed to "H_rec" (instead of "H_m" as in the original CSV) to be consistent with the attribute name used throughout the R code.</li> </ul> <p>Except for the above files, all the input and output files in <a href="https://zenodo.org/records/12792513" target="_blank" rel="noopener">v2.0.1</a><span> remain unchanged. </span></p> </div> <p><u> </u></p>
SMTLIB2.6 translation of proof obligations from the B formal method
<p>These files have been produced from the <a href="https://doi.org/10.5281/zenodo.7050797">POG files</a> using the program ppTransSmt, distributed with Atelier B.</p> <p>The source code of this version of ppTransSmt correspond to git commit `abb8ad04003803ea3683d8069363681e92308ebf` (in the private repository<br> of Atelier B).<br> </p>
Proof obligations from the B formal method
<p>Proof obligations generated with Atelier B, an IDE for the B method and Event-B.</p> <p>The files are in the POG format.</p>
Selective Oxidation of 5-Hydroxymethylfurfural to 2,5-Diformylfuran in Biphasic Media using Immobilized Galactose Oxidase: Proof of Concept and Limitations
<p>The oxidation of 5-hydroxymethylfurfural (HMF) to 2,5-diformylfuran (DFF) is a key reaction in valorizing biomass. DFF is hardly soluble in water, while HMF is often obtained from biorefineries in crude wet organic fractions. Thus, the reaction is challenging for both biocatalysis performed in aqueous media, and for chemocatalysis where the presence of water often results in catalyst poisoning. Galactose oxidase (GalOx) can selectively oxidize HMF to DFF and displays promising activity in aqueous-organic media. In this study, GalOx was immobilized on ten carriers, assessing the immobilization yield, activity, and stability. Covalently immobilized GalOx catalyzed the oxidation of HMF to DFF in neat and water-saturated EtOAc, and in biphasic systems of various water contents. At 50 % v/v H<sub>2</sub>O, the reaction was conducted at a semi-preparative scale (50 mL) with no adverse effect on DFF yield. Some limitations arise, such as enzyme deactivation, and adsorption of DFF to the support, particularly in the aqueous fraction. Future options to upgrade the route may include designed stable enzymes under the presence of HMF/DFF, and the setup of microaqueous systems where DFF adsorption is minimized. The use of wet EtOAc media would be a promising approach in future biorefineries employing inexpensive crude wet organic fractions.</p>
Proof-of-Concept Measurement for "Radar Band Fusion Using Frame-Based Compressed Sensing"
<p>This data set was created for a proof-of-concept test of the method described in "Radar Band Fusion Using Frame-Based Compressed Sensing". It consists of a measurment against a metal plate.</p> <p> </p>
Identification of grapevine clones via high-throughput amplicon sequencing: a proof-of-concept study VCF files
<p>VCF files used and cited in the article: Identification of grapevine clones via high-throughput amplicon sequencing: a proof-of-concept study</p>
Dataset of the article "A new and almost perfectly accurate approximation of the eigenvalue effective population size of a dioecious population: comparisons with other estimates and detailed proofs"
<p>Dataset of the article "A new and almost perfectly accurate approximation of the eigenvalue effective population size of a dioecious population: comparisons with other estimates and detailed proofs" (https://doi.org/10.5281/zenodo.7927968), recommended by PCI Evol Biol (https://evolbiol.peercommunityin.org/articles/rec?id=651)</p>
Proof-of-concept AO telemetry data using the AOT standard format
<p>Dataset containing a demonstration of AO telemetry data using the AOT standard format. Contains data from 5 different systems (CIAO, ERIS, GALACSI, NAOMI and PAPYRUS).</p> <p>The data is as follows:</p> <ul> <li>4 CIAO files "CIAO#_*.fits" where # indicates the AT where the data was produced.</li> <li>2 ERIS files, one in LGS (LTAO) mode and another in NGS (SCAO) mode.</li> <li>1 GALACSI file.</li> <li>4 NAOMI files "NAOMI#_*.fits" where # indicates the AT where the data was produced.</li> <li>2 PAPYRUS files, one using a Shack-Hartmann wavefront sensor (SHWFS) and another using a Pyramid wavefront sensor (PWFS).</li> </ul> <p>GALACSI, CIAO, NAOMI and ERIS data were gathered under ESO's program IDs 60.A-9278(B), 60.A-9278(C), 60.A-9278(D) and 60.A-9278(E) respectively. The data was translated via the functions provided in the Python package <em>aotpy</em> (<a href="https://doi.org/10.5281/zenodo.8187230">10.5281/zenodo.8187230</a>).</p> <p>This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No. 101004719 (OPTICON–RadioNet Pilot).</p>
Simple Dataset for Proof Method Recommendation in Isabelle/HOL
<p>Recently, a growing number of researchers have applied machine learning to assist users of interactive theorem provers.</p> <p>However, the expressive nature of underlying logics and esoteric structures of proof documents impede machine learning practitioners, who often do not have much expertise in formal logic, let alone Isabelle/HOL, from applying their tools and expertise to theorem proving.</p> <p>In this data description, we present a simple dataset that contains data on over 400k proof method applications in the Archive of Formal Proofs along with over 100 extracted features for each in a format that can be processed easily without any knowledge about formal logic.</p> <p>Our simple data format allows machine learning practitioners to try machine learning tools to predict proof methods in Isabelle/HOL, even if they are unfamiliar with theorem proving.</p>
Comparative Analysis of Anthraquinone and Chalcone Derivatives-Based Virtual Combinatorial Library. A Cheminformatics "Proof-of-Concept" Study
<p>This computational “proof-of-concept” study illustrated the combinatorial approach used to explain how the selected natural products' structures undergo molecular diversity analysis. A virtual combinatorial library (1.6M) based on 20 anthraquinones and 24 chalcones were enumerated. The resulting compounds were optimized to the near drug-likeness properties and the physicochemical descriptors were calculated for all datasets including FDA, Non-FDA, and natural products (NPs) datasets from ZINC 15. UMAP and principal component analysis (PCA) were applied to compare and represent the chemical space coverage of each dataset. Subsequently, the Laplacian score, and Gini coefficient, were applied to delineate feature selection, and selectivity among properties respectively. Finally, we demonstrated the diversity between the datasets by employing Murcko’s, and central scaffolds systems, calculated three fingerprint descriptors, and analyzed their diversity by PCA and self-organizing maps (SOM). The optimized enumeration resulted in 1,610,268 compounds with NP-Likeness, and synthetic feasibility mean scores close to FDA, Non-FDA, and NPs datasets. The overlap between the chemical space of 1.6M was more prominent with NPs. Laplacian score has prioritized NP-likeness and hydrogen bond acceptor properties (1.0 and 0.923) respectively, while the Gini coefficient showed that all properties have selective effects on datasets (0.81 to 0.93). Scaffold and fingerprint diversity indicated that the descending order for the tested datasets was FDA, Non-FDA, NPs, 1.6M. Virtual combinatorial libraries based on NPs can be considered as a source of the combinatorial compound with NP-likeness properties. Furthermore, measuring molecular diversity is supposed to be performed by different methods to allow for comparison and better judgment. </p> <p>This link provides an illustration of the whole virtual combinatorial library using the TMAP algorithm in addition to the complete dataset. TMAP is a recent algorithm applied to visualize ultra-large high-dimensional chemical libraries for structures and physicochemical properties (Probst & Reymond, 2020). This approach creates and distributes intuitive tree representations of big data sets with arbitrary dimensionality in the order of 10<sup>7</sup>.</p> <p><strong>To visualize the whole library of compounds, download the "index(2).rar", then extract the index.html that pop-up in the WinRAR application.</strong></p>
The FAIR-Device - a non-lethal and generalist semi-automatic Malaise trap for insect biodiversity monitoring: Proof of concept - Supplementary Material
<h3>Abstract</h3> <p>Field monitoring plays a crucial role in understanding insect dynamics within ecosystems. It facilitates pest distribution assessment, control measure evaluation, and prediction of pest outbreaks. Additionally, it provides important information on bioindicators with which the state of biodiversity and ecological integrity in specific habitats and ecosystems can be accurately assessed. However, traditional monitoring systems can present various difficulties, leading to a limited temporal and spatial resolution of the obtained information. Despite recent advancements in automatic insect monitoring traps, also called e-traps, most of these systems focus exclusively on studying agricultural pests, rendering them unsuitable for monitoring diverse insect populations. To address this issue, we introduce the Field Automatic Insect Recognition (FAIR)-Device, a novel non-lethal field tool that relies on semi-automatic image capture and species identification using artificial intelligence via the iNaturalist platform. Our objective was to develop an automatic, cost-effective, and non-specific monitoring solution capable of providing high-resolution data for assessing insect diversity. During a 26-day proof-of-concept evaluation, the FAIR-Device recorded 24.8 GB of video, identifying 431 individuals from 9 orders, 50 families, and 69 genera. While improvements are possible, our device demonstrated potential as a cost-effective, non-lethal tool for monitoring insect biodiversity. Looking ahead, we envision new monitoring systems such as e-traps as valuable tools for real-time insect monitoring, offering unprecedented insights for ecological research and agricultural practices.</p> <h3>Description of the data and file structure</h3> <p>This repository complements the publication <a href="https://www.biorxiv.org/content/10.1101/2024.03.22.586299v2" target="_blank" rel="noopener">"The FAIR-Device - a non-lethal and generalist semi-automatic Malaise trap for insect biodiversity monitoring: Proof of concept".</a> It contains the result data from the proof of concept field test of V1.0 of the FAIR-Device, conducted between July and August 2021 at the Thünen Institute of Agricultural Technology in Braunschweig. The repository comprises three compressed files (.zip):</p> <ul> <li><strong>FAIR-D_captures.zip</strong>: <ul> <li>Video captures from the field tests organized by recording day.</li> <li>Filenames indicating recording time (hh-mm-ss).</li> </ul> </li> </ul> <ul> <li><strong>FAIR-D_Tables&Code.zip</strong>: <ul> <li>Processed results from the obtained image captures, organized into: <ul> <li><strong>Monitoring2021_TotalPeriod.xlsx: </strong>Result table with taxonomic classifications, data analysis, and charts.</li> <li><strong>iNat_observations.xlsx: </strong>iNaturalist reviews analysis table.</li> <li><strong>R: </strong>code for generating article graphics.</li> </ul> </li> </ul> </li> </ul> <ul> <li><strong>FAIR-D_V1.0_3D_Models.zip</strong>: <ul> <li>Complete 3D design of the FAIR-D V1.0 in .stl format, organized into: <ul> <li><strong>3D_print_parts</strong>: 3D-printable parts with spatial coordinates for correct positioning in CAD software.</li> <li><strong>other_3Dparts</strong>: Non-printable parts, also in .stl format with spatial coordinates.</li> </ul> </li> </ul> </li> </ul> <p> </p> <p>NOTE: For visualizing the videos, we recommend <strong>VLC media player</strong> - <a href="https://www.videolan.org/vlc/">https://www.videolan.org/vlc/</a> </p>
Benchmarks for POPL'24 Paper "Commutativity Simplifies Proofs of Parameterized Programs"
<p>This archive contains the benchmark programs used in the POPL'24 paper <i>"Commutativity Simplifies Proofs of Parameterized Programs"</i> by A. Farzan, D. Klumpp and A. Podelski. <a href="https://doi.org/10.1145/3632925">https://doi.org/10.1145/3632925</a></p><p>A preprint of the paper can be found at <a href="https://arxiv.org/abs/2311.02673">https://arxiv.org/abs/2311.02673</a>.</p>
Machine Proofs for Adams Differentials and Extension Problems among CW Spectra
<p>Update notes: In this version, we reduce the number of spectra in this project from 210 to 49 (compared to the cw210 version), while keeping the outcome sufficient to prove <a href="https://arxiv.org/abs/2412.10879">the Last Kervaire Invariant Problem</a>. The size of the proof file <a href="https://zenodo.org/api/records/14875532/draft/files/proofs.db.rar/content" target="_blank" rel="noopener noreferrer">proofs.db.rar</a> is also reduced from 600MB to 44MB, leading to easier track for proofs.</p> <p>In this Zenodo repository we upload the computations of Adams differentials and extensions among many CW spectra and their proofs. This data will be used in the <a href="https://arxiv.org/abs/2412.10879">proof of the Last Kervaire Invariant Problem</a> by Weinan Lin, Guozhen Wang and Zhouli Xu.</p> <p>In <strong>programs.rar</strong>, we have two programs ./Adams and ./ss provided for both windows users and mac users and a definition file <strong>Adams.json</strong> for spectra involved in this project. The source code for the two programs is contained in <strong>source code.zip</strong>. You can also find the source code on Github <a href="https://github.com/WayneLin92/SSeqCpp">https://github.com/WayneLin92/SSeqCpp</a> together with user manual for the programs.</p> <p>In <strong>programs.rar</strong> there is also a demo for ./ss which is a category of five spectra: S0, C2, Ceta, Cnu, Csigma.</p> <p><strong>kervaire_database.rar</strong> contains all the Adams spectral sequence data and extension data. They are sqlite3 database files and can be read directly by the ./ss program. We also provide the same data in csv format in <strong>kervaire_csv.rar</strong>.</p> <p>The two zip files<strong> proofs.db.rar</strong> and <strong>proofs_csv.rar</strong> are proofs of all the differentials. Inside <strong>proofs_csv.rar</strong> there are 3 csv files. We break it to 3 csv files because Microsoft Excel has a limit of 1,000,000 rows.</p> <p>On the website <a href="https://waynelin92.github.io/ss/kervaire-49.html">https://waynelin92.github.io/ss/kervaire-49.html</a> you can find plots of the data. The website source code (html/javascript) is actually contained in <strong>programs.rar</strong>/webpages in this repository.</p> <p>Please read <strong>instructions.pdf</strong> for more infomation.</p>
juan-duenas/NHESS: Soil conditioner mixtures as an agricultural management alternative to mitigate drought impacts: a proof-of-concept.
<p>The dataset and the R script have been enhanced and corrected, respectively. The main figures of the associated publication have been added in two different qualities.</p> <p>This data is associated to a paper that will appear in an special issue of the journal Natural Hazards and Earth System Sciences. https://nhess.copernicus.org/articles/special_issue1295.html</p>
Proofs from interactive and automated theorem provers to evaluate Kontroli & Dedukti
<p>This dataset contains proofs in the Dedukti format<br> from the interactive theorem provers (ITPs) Matita, HOL Light, and Isabelle/HOL, as well as<br> from the automated theorem provers (ATPs) iProver Modulo and Zenon Modulo.<br> This data is used in the evaluation of the proof checkers Kontroli and Dedukti.</p>
Joint Communication and Sensing: a Proof of Concept and Datasets for Greenhouse Monitoring using LoRaWAN
<p>The goal of these LoRaWAN based greenhouse monitoring datasets, is to provide the global research community with a benchmark tool to evaluate different techniques for precision agriculture in large greenhouse environments. An identical collection methodology was used for both of the two datasets over the same tomato crop: during a period of five months, respectively. Together with temperature and humidity values, network information such as receiving time of the message and Received Signal Strength Indicator (RSSI) were stored in the greenhouse monitoring datasets:</p> <ul> <li><strong>Greenhouse-1.csv</strong> <ul> <li>Data from 27 sensors denoted as AF 16-42 with an average of 19687 LoRaWAN messages per sensor from April till August 2020, obtained in the greenhouse for tomato crop in Belgium.</li> </ul> </li> <li><strong>Greenhouse-2.csv</strong> <ul> <li>Data from 19 sensors denoted as AF 49-67 with an average of 19009 LoRaWAN messages per sensor from July till November 2020, obtained in the other greenhouse for tomato crop in the Netherlands.</li> </ul> </li> <li><strong>Greenhouse-1-Transformed-Data.csv</strong> <ul> <li>Mean temperature, humidity, and RSSI values along with plant height for the same period.</li> </ul> </li> </ul> <p>Both the greenhouses, had no LoRaWAN connectivity, so individual gateway were installed for both locations. For Greenhouse-1 data, sensors were switched on in a room on 10<sup>th</sup> of April and brought to the greenhouse chamber on 17<sup>th</sup> April at 06:38 am for sensing. It would be crucial to accordingly use data set, considering the above time period.</p> <p>The collection methodology of datasets, and first results of a joint communication and sensing proof-of-concept are documented in the journal paper : https://www.mdpi.com/1424-8220/22/4/1326.</p> <p> </p>
Home-based measurements of dystonia and choreoathetosis in cerebral palsy using smartphone-coupled inertial sensor technology and machine learning: A proof-of-concept study - dataset
<p>Home-based measurements of dystonia in cerebral palsy using smartphone-coupled inertial sensor technology and machine learning: A proof-of-concept study</p> <p> </p> <p>This project contains:</p> <p>- 1 main MATLAB script: MODYSathome_main.m<br> - 12 MATLAB functions:<br> - function_calc_mean_recall_precision.m<br> - function_create_dataframes.m<br> - function_deep_learning.m<br> - function_determine_best_ML_model.m<br> - function_display_DL_results.m<br> - function_display_ML_results.m<br> - function_index_extremities.m<br> - function_machine_learning.m<br> - function_oversample.m<br> - function_partition_data.m<br> - function_pick_best_models.m<br> - function_prepare_DL_data.m</p> <p>Downloading the Matlab scripts</p> <p> - Create a folder named 'MODYS' and create a subfolder named 'results'<br> - Download the zip file via <a href="https://zenodo.org/record/6379348">RehabAUmc/modys-at-home: v1.0 | Zenodo</a><br> - Unzip the zip file in the path MODYS\</p> <p>STEPS<br> 1. Open MATLAB<br> 2. In MATLAB, go to the 'HOME' tab and click on 'Set Path'<br> 3. Click on 'Add Folder' and browse to MODYS/RehabAUmc-modys-at-home-86b14c3/functions<br> 4. Click on 'Select Folder' and click on 'Save'<br> 5. Click on 'Browse to folder' and browse to a patients' data in MODYS/data/PatientXXX, then click on 'Select Folder'<br> 6. In the 'HOME' tab click on 'Open' and open MODYSathome.m in MODYS/RehabAUmc-modys-at-home-86b14c3<br> 7. In the 'EDITOR' tab click on 'Run Section' to run the script<br> 8. When the code has been run, the results are displayed in the Command Window and saved in MODYS/results/PatientXXX</p>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.