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.
9
datasets available to search
ShareScore release 0.9.0
Dataset results
9 results for “Automated reasoning”
Datset of automated economic reasoning problems for QE / SMT
<p>This dataset is generated by 45 economics theorems "A implies H" where A are assumptions and H a hypothesis. These are taken from textbooks and papers and chosen for their suitability for automatic solution with Quantifier Elimination (QE) or Satisfiability Modulo Theory (SMT) technology. </p> <p>For each theorem three problems are generated: checking the compatibility of the assumptions; checking for the existence of an example of the theorem; and checking for the existence of a counterexample. </p> <p>There are three files:</p> <p>1. EconomicReasoningBenchmarks-Apr18-SMT2.zip</p> <p>This zip file will uncompress into a directory with 45 files, one for each theorem stating the three existence checks within the SMT2 format. Thus these files are suitable for use with any SMT solver supporting the theory.</p> <p> </p> <p>2. EconomicReasoningBenchmarks-Apr20-Redlog.txt</p> <p>This plain text file can be run with the Redlog Package for the Computer Algebra System Reduce. It contains definitions and calls to Redlog's QE command to check for a counterexample for all 45 theorems.</p> <p> </p> <p>3. EconomicReasoningBenchmarks-Apr23-Maple.txt</p> <p>This plain text file is for use with the Maple Computer Algebra System. For each theorem it provides the polynomials used in the Tarski formula to check for a counterexample. The polynomials are given as a list of lists with the outer list representing logical OR between entries and each inner list logical AND. </p> <p> </p>
Automated Reasoning in Temporal DL-Lite
<p><strong>Automated Reasoning in Temporal DL-Lite*</strong></p> <p>We investigate the feasibility of automated reasoning over temporal DL-Lite (TDL-Lite) knowledge bases (KBs). We translate TDL-Lite KBs into a fragment of First Order temporal logic and then into LTL, and apply off-the-shelf LTL and FO-based reasoners for checking the satisfiability. We conduct various experiments to analyse the size of the LTL translation as well as the runtime performance of different reasoners on toy scenarios and on randomly generated TDL-Lite KBs. To improve the reasoning performance when dealing with large ABoxes, our work also proposes an approach for abstracting temporal assertions in KBs. We run several experiments with this approach to assess the effectiveness of the technique by measuring the gain in terms of the size of the translation, and the number of both ABox assertions and individuals. We also measure the runtime of the solvers on such abstracted KBs. Lastly, in an effort to make the usage of TDL-Lite KBs a reality, we present a fully-fledged tool with a graphical interface to design and reason over them. Our interface is based on conceptual modeling principles and it is integrated with our translation tool and a temporal reasoner.</p> <p>(*) This work has been submitted to the Journal of Automated Reasoning</p>
Supplemental data for submission "Bridging between LegalRuleML and TPTP for Automated Normative Reasoning"
<p>These files are supplementary material to the submission<br> Bridging between LegalRuleML and TPTP for Automated Normative Reasoning<br> by<br> Alexander Steen and David Fuenmayor<br> submitted to the 6th International Joint Conference on Rules and Reasoning (RuleML+RR 2022), 2022.</p> <p>Files ex1.lrml.xml and ex2.lrml.xml are two example LegalRuleML files.<br> Files ex1.dsl.p and ex2.dsl.p are two examples from above translated to the NMF DSL.<br> The files ex1.output.X.p and ex2.output.X.p are the translations of the NMF files into the concrete logic X (X = SDL or X = cJ (Carmo Jones) or X = aqvist (system E)).</p> <p>Alexander Steen, <alexander.steen@uni-greifswald.de></p>
DATA for the paper SEMIGROUPS, KEIS AND GROUPS INDUCED BY KNOT DIAGRAMS: AN EXPERIMENTAL INVESTIGATION WITH AUTOMATED REASONING
<p>This upload contains supplementary materials for the paper SEMIGROUPS, KEIS AND GROUPS INDUCED BY KNOT DIAGRAMS: AN EXPERIMENTAL INVESTIGATION WITH AUTOMATED REASONING</p>
Experimental data for the paper Automated reasoning for knot semigorups and \pi-orbifold groups of knots
<p>This upload contains experimental data to supplement the <br> paper Automated reasoning for knot semigroups and \pi-orbifold <br> groups of knots, by Alexei Lisitsa and Alexei Vernitski, 2017 </p> <p>ALTERNATING-SG.zip Proofs by Prover9 for Section 3, (4-plats) <br> KS_Models.zip Models found by Mace4 for Section 2.3 (Non-cyclic knot semigorups: small knots) <br> PROVING-TRIVIAL.zip Proofs by Prover 9 for Section 2.2 (Cyclic knot semigroups) <br> </p>
Code and data for the paper "Automated reasoning for proving non-orderability of groups"
<p>Code and data for the paper titled "Automated reasoning for proving non-orderability of groups". Containing the input files, output files and proofs obtained by Prover9; the input files, output files and models obtained by Mace4; and a Python 3 script to generate this data set.</p>
Materials for "Invalidator: Automated Patch Correctness Assessment via Semantic and Syntactic Reasoning"
<p>This repository contains materials including source code, datasets and results for "Invalidator: Automated Patch Correctness Assessment via Semantic and Syntactic Reasoning"</p>
Automation Bias in Physician-LLM Diagnostic Reasoning
ClinicalTrials.gov study NCT06963957. IPD Sharing: NO. Countries: 1. Publications: 0.
Mitigating Automation Bias in Physician-LLM Diagnostic Reasoning Using Behavioral Nudges
ClinicalTrials.gov study NCT07328815. IPD Sharing: NO. Countries: 1. Publications: 0.
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.