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.
260
datasets available to search
ShareScore release 0.9.0
Dataset results
260 results for “logic”
Superposition for Lambda-Free Higher-Order Logic — Supplementary Material
<p>We provide the following supplementary material for our <a href="http://matryoshka.gforge.inria.fr/pubs/lfhosup_paper.pdf">paper</a>. The longer version of our paper can be found here: <a href="http://matryoshka.gforge.inria.fr/pubs/lfhosup_report.pdf">report</a>.</p> <p><strong>Compiling Zipperposition</strong></p> <p>Compilation instructions for Zipperposition, in particular instructions for compilation for <a href="https://www.starexec.org">StarExec</a>, can also be found in the <a href="https://github.com/c-cube/zipperposition/#starexec">Zipperposition readme</a>.</p> <p>In general, follow the following steps:</p> <ul> <li>Install <a href="https://opam.ocaml.org/doc/Install.html">OPAM</a></li> <li>Zipperposition requires OCaml >= 4.03.0, e.g. use <pre>opam switch 4.05.0+flambda eval `opam config env`</pre> </li> <li>You might have to install gmplib on your system, e.g. <pre>sudo apt-get install libgmp3-dev</pre> </li> <li>Zipperposition requires the following dependencies. <pre>opam install zarith containers sequence oasis msat menhir jbuilder</pre> </li> <li>Clone Zipperposition and compile it (we used commit 7fe2ebeb0500e350fd0f1dd4c4ad402ba9cf99b6): <pre>git clone https://github.com/c-cube/zipperposition.git --branch dev cd zipperposition make build</pre> This will create the binary zipperposition.native.</li> <li>Compile the applicative encoder if needed: <pre>jbuilder build ./src/tools/app_encode.exe</pre> This will create the binary ./_build/default/src/tools/app_encode.exe.</li> </ul> <p><strong>Problems</strong></p> <p>We used the following first-order (TFF) and the higher-order (THF) <a href="http://www.tptp.org/">TPTP (v7.0.0) problems</a> for the evaluation:<br> <a href="/record/3975512/files/list_TFF.txt">TFF problem list </a><br> <a href="/record/3975512/files/list_THF.txt">THF problem list </a></p> <p>The selection criteria for the problems are described in our paper. We used these scripts to create these problems lists and to generate an XML file to link these problems into a seperate space in Starexec: <a href="/record/3975512/files/starexec_xml.tar.gz"> Problem selection & StarExec XML generation scripts </a></p> <p><strong>Run scripts</strong></p> <p>We used the following run scripts on starexec. This archive also contains the Zipperposition binary and the applicative encoder binary, compiled for Starexec: <a href="/record/3975512/files/run_scripts.tar.gz"> StarExec run scripts </a></p> <p>The scripts use the following command-line options for Zipperposition:</p> <ul> <li>First-order mode: <pre>./zipperposition.native -i tptp -o tptp --no-ho --no-avatar --no-induction --no-unif-pattern --simultaneous-sup false --no-max-vars --no-fool</pre> </li> <li>Intensional purifying calculus: <pre>./zipperposition.native -i tptp -o tptp --no-avatar --ho --force-ho --no-ho-elim-pred-var --ho-general-ext-pos --no-ho-unif --no-induction --no-unif-pattern --simultaneous-sup false --ho-purify int --ho-no-ext-pos --ho-no-ext-neg --ho-prim-enum none --no-max-vars --dont-select-ho-var-lits --no-fool</pre> </li> <li>Intensional nonpurifying calculus: <pre>./zipperposition.native -i tptp -o tptp --no-avatar --ho --force-ho --no-ho-elim-pred-var --ho-general-ext-pos --no-ho-unif --no-induction --no-unif-pattern --simultaneous-sup false --sup-at-vars --ho-no-ext-pos --ho-no-ext-neg --ho-prim-enum none --no-max-vars --dont-select-ho-var-lits --no-fool</pre> </li> <li>Extensional purifying calculus: <pre>./zipperposition.native -i tptp -o tptp --no-avatar --ho --force-ho --no-ho-elim-pred-var --ho-general-ext-pos --no-ho-unif --no-induction --no-unif-pattern --simultaneous-sup false --ho-purify ext --ho-ext-axiom --restrict-hidden-sup-at-vars --ho-prim-enum none --no-max-vars --dont-select-ho-var-lits --no-fool</pre> </li> <li>Extensional nonpurifying calculus: <pre>./zipperposition.native -i tptp -o tptp --no-avatar --ho --force-ho --no-ho-elim-pred-var --ho-general-ext-pos --no-ho-unif --no-induction --no-unif-pattern --simultaneous-sup false --sup-at-vars --restrict-hidden-sup-at-vars --ho-ext-axiom --ho-prim-enum none --no-max-vars --dont-select-ho-var-lits --no-fool</pre> </li> </ul> <p>Additionally, we provided the problem's filename as the first argument, the order (<code>--ord rpo6</code> or <code>--ord kbo</code>), the timeout (<code>--timeout 600</code>) and the memory limit (<code>--mem-limit 128000</code>). We used <code>--timeout 600</code> and Starexec's Wallclock timeout was set to 600s, but Starexec's CPU timeout was set to 300s. So effectively we allowed only 300s of calculation time.</p> <p>For the applicative encoder app_encode.exe, we provide the problem's filename as the first argument. The option <code>-o tptp</code> should be used to ensure that the output is also in TPTP format. To add the extensionality axiom to the applicative encoding, we use <code>--app-encode-extensional</code>.</p> <p><strong>Results</strong></p> <p>Download the raw output of the evaluation and the .csv files created by StarExec here: <a href="/record/3975512/files/output.tar.gz"> Evaluation output </a></p> <p>We used our own scripts to statistically analyse the results instead of using StarExec's statistics: <a href="/record/3975512/files/eval.tar.gz"> Evaluation scripts</a>. Set the location of the xml-file and the output files produced by StarExec in config.py and run stats.py to obtain the statistics displayed in the paper.</p> <p><strong>Examples</strong></p> <p>We tested the examples given in our paper in Zipperposition. Here are the problem files we used. Some are in TPTP format (.p) and some are in Zipperposition format (.zf).</p> <ul> <li><a href="/record/3975512/files/example_varcond.zf">Example "Justification for the weaker variable condition in the intensional variant" </a></li> <li><a href="/record/3975512/files/example_posext.zf">Example "Justification PosExt" (only in report) </a></li> <li><a href="/record/3975512/files/example_supatvars_rpo.zf">Example "Justification for purification and SUP inferences at variables" (only in report) </a></li> <li><a href="/record/3975512/files/example_add_equiv_defs.p">Example "Addition of Peano numbers" </a></li> <li><a href="/record/3975512/files/example_add_equiv_defs_app.p">Example "Addition of Peano numbers" (applicative encoding) </a></li> </ul>
Logical model for Model checking to assess T-helper cell plasticity
<p>Logical modeling has proven suitable for the dynamical analysis of large signaling and transcriptional regulatory networks. In this context, signaling input components are generally meant to convey external stimuli, or environmental cues. In response to such external signals, cells acquire specific gene expression patterns modeled in terms of attractors (e.g. stable states). The capacity for cells to alter or reprogram their differentiated states upon changes in environmental conditions is referred to as cell plasticity.</p> <p>In <a href="https://dx.doi.org/10.3389/fbioe.2014.00086">[1]</a>, it is presented an extended version of a published logical model of T-helper cell differentiation and plasticity, which accounts for novel cellular subtypes. The model encompasses 20 signaling pathways, a dozen of transcription factors, and about 30 cytokines, amounting to 101 components in total.</p> <p>Computational methods recently developed to efficiently analyze large models <a href="http://ginsim.org/node/185#ref1">[1]</a> are first used to study static properties of the model (i.e. stables states). Symbolic model checking is then applied to get further insights into reachability properties between Th canonical subtypes upon changes of specific prototypic environmental cues.</p> <p>The model reproduces novel reported Th subtypes (Tfh, Th9, Th22) and predicts additional Th hybrid subtypes in term of stables states. Using the model checker NuSMV-ARCTL, an abstract view of the dynamics, called reprograming graph, is produced providing a global and synthetic view of Th plasticity. The model is consistent with experimental data showing the polarization of naïve Th cells into the canonical Th subtypes. The model further predicts substancial plasticity of Th subtypes depending on the signalling environment.</p>
Logical model for Molecular Pathways Enabling Tumour Cell Invasion and Migration
<p>Understanding the etiology of metastasis is very important in clinical perspective, since it is estimated that metastasis accounts for 90% of cancer patient mortality. Metastasis results from a sequence of multiple steps including invasion and migration. The early stages of metastasis are tightly controlled in normal cells and can be drastically affected by malignant mutations; therefore, they might constitute the principal determinants of the overall metastatic rate even if the later stages take long to occur. To elucidate the role of individual mutations or their combinations affecting the metastatic development, a logical model has been constructed that recapitulates published experimental results of known gene perturbations on local invasion and migration processes, and predict the effect of not yet experimentally assessed mutations. The model has been validated using experimental data on transcriptome dynamics following TGF-β-dependent induction of Epithelial to Mesenchymal Transition in lung cancer cell lines. A method to associate gene expression profiles with different stable state solutions of the logical model has been developed for that purpose. In addition, we have systematically predicted alleviating (masking) and synergistic pairwise genetic interactions between the genes composing the model with respect to the probability of acquiring the metastatic phenotype. We focused on several unexpected synergistic genetic interactions leading to theoretically very high metastasis probability. Among them, the synergistic combination of Notch overexpression and p53 deletion shows one of the strongest effects, which is in agreement with a recent published experiment in a mouse model of gut cancer. The mathematical model can recapitulate experimental mutations in both cell line and mouse models. Furthermore, the model predicts new gene perturbations that affect the early steps of metastasis underlying potential intervention points for innovative therapeutic strategies in oncology.</p> <p> </p> <p>Included files:</p> <ul> <li>Master Model: the model includes detailed regulation of the major players involved in the crosstalks between Notch and p53 pathways</li> <li>Modular Model: the model is a reduction of the master model. To reduce the master model, we lumped together some entities that belonged to a module.</li> </ul>
Supporting Data: Complementary Organic Logic Gates on Plastic Formed by Self-Aligned Transistors with Gravure and Inkjet Printed Dielectric and Semiconductors
<p>The file contains the supporting data for the publication:</p> <p>S.G. Higgins, B.V.O. Muir, G. Dell'Erba, A. Perinot, M. Caironi, A.J. Campbell. Complementary Organic Logic Gates on Plastic Formed by Self-Aligned Transistors with Gravure and Inkjet Printed Dielectric and Semiconductors. doi: 10.1002/aelm.201500272. <em>Advanced Electronic Materials </em>(2015)</p> <p>See 'README.txt' for a description of the contents of the compressed file.</p>
Logic-Induced-Long-Tail (LINT)
<p>Logic-Induced-Long-Tail (LINT) dataset for arxiv paper "IN SEARCH OF THE LONG-TAIL: SYSTEMATIC GENERATION OF LONG-TAIL KNOWLEDGE VIA LOGICAL RULE GUIDED SEARCH."</p>
Data for "Highly-Automated, High-Throughput Replication of Yeast-based Logic Circuit Design Assessments"
<p>Flow Cytometry and plate reader data from "High Throughput Experimentation to replicate Yeast Gates Experiment," accompanied with jupyter noteboooks to replicate the analyses. Sequencing data is <a href="https://www.ncbi.nlm.nih.gov/bioproject/?term=PRJNA784977">available separately</a>.</p> <p>Files named <code>flow_cytometrya<em>x</em></code> should be concatenated: they are individual slices of a gzipped tar file. Concatenate them and then extract with <code>tar xzf <em>filename</em></code>.</p> <p>The paper is available on <a href="https://biorxiv.org/cgi/content/short/2022.05.31.493627">Biorxiv</a>.</p> <p>The Jupyter notebooks used to analyze this data for the paper are <a href="https://github.com/rpgoldman/replication-paper-data-analysis">available on GitHub</a>.</p>
Dataset of "Advancing Logic Circuits with Halide Perovskite Memristors for Next-Generation Digital Systems"
<p><span>This dataset supports the article "Advancing Logic Circuits with Halide Perovskite Memristors for Next-Generation Digital Systems" </span></p> <p> </p> <p><span>Raw data for the article "<span>Advancing Logic Circuits with Halide Perovskite Memristors for Next-Generation Digital Systems</span>". For further details see the readme.txt file.</span></p>
Samples of Rectified Transfemoral Sockets with Fuzzy-Logic-Based Decision Support System
<p>This dataset contains sample rectified transfemoral sockets as an output of the fuzzy-logic DSS.</p> <p>This work was supported by the EU Horizon2020 research and innovation project SocketSense, No 825429.</p> <p>Relevant paper DOI: <a href="https://doi.org/10.3390/s21113743">https://doi.org/10.3390/s21113743</a></p>
Logical reasoning study
Open the record for dataset details and reuse information.
Additional material for "Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities"
<p>Complementary material including the proofs of all theorems presented at TACAS 2020, a detailed description of the RERS 2019 experiment, and the actual data used for the RERS 2018,RERS 2019, and TFTP experiments.</p>
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic -- Evalution Data
<p>This package contains problems used for evalaution and the raw evaluation data for the Extending a Brainiac Prover to Lambda-Free Higher-Order Logic article</p>
Data of "A quantum-logic gate between distant quantum-network modules"
<p>Data published in "<em>A Quantum-Logic Gate between Distant Quantum-Network Modules</em>"</p> <p>Science</p>
Accepted Artifact for Little Tricky Logic: Misconceptions in the Understanding of LTL
<p>Datasets and source materials for our studies of Linear Temporal Logic (LTL).</p> <p>Includes:</p> <ul> <li> <p> Labelled responses to our surveys</p> </li> <li> <p>The surveys themselves</p> </li> <li> <p>The coding rubric that guided our categorization</p> </li> </ul>
Data from: 3D printed digital pneumatic logic for the control of soft robotic actuators
<p>Soft robots are paving their way to catch up with the application range of metal-based machines and to occupy fields which are challenging for traditional machines. Pneumatic actuators play an important role in this development, allowing the construction of bioinspired motion systems. Pneumatic logic gates provide a powerful alternative for controlling pressure-activated soft robots, which are often controlled by metallic valves and electric circuits. Many existing approaches for fully compliant pneumatic control logic suffer from high manual effort and low pressure tolerance. In our work, we invented 3D printable, pneumatic logic gates that perform Boolean operations and imitate electric circuits. Within 7 hours, an FDM printer is able to produce a module that serves as either an OR, AND or NOT gate; the logic function is defined by the assigned input signals. The gate contains two alternately acting pneumatic valves, whose work principle is based on the interaction of pressurized chambers and a 3D printed 1 mm tube inside. The gate design does not require any kind of support material for its hollow parts, which makes the modules ready to use directly after printing. Depending on the chosen material, the modules can operate on a pressure supply between 80 and over 750 kPa. The capabilities of the invented gates were verified by implementing an electronics-free drink dispenser based on a pneumatic ring oscillator and a 1-bit memory. Their high compliance is demonstrated by driving a car over a fully flexible, 3D printed robotic walker controlled by an integrated circuit.</p>
Supplemental material to "Solving Quantified Modal Logic Problems by Translation to Classical Logics"
<p>These files are associated with the manuscript entitled<br>"Solving Quantified Modal Logic Problems by Translation to Classical Logics"<br>by Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller.</p> <p>Contact: Alexander Steen <alexander.steen@uni-greifswald.de></p> <p>Contents<br>-----------</p> <p> - QMLTP-monomodal-NX0.tar.gz<br> This archive contains the TPTP NX0 representations of the 580 mono-modal<br> problems translated from the QMLTP library [1,2].<br> <br> - QMLTP-monomodal-TF0-embedded-rigid-local.tar.gz<br> This archive contains the embedded TF0 files created <br> from the monomodal NX0 files using the Logic Embedding Tool [3].<br> <br> - QMLTP-monomodal-TH0-embedded-rigid-local.tar.gz<br> This archive contains the embedded TH0 files created <br> from the monomodal NX0 files using the Logic Embedding Tool [3,4].<br> <br> - QMLTP-multimodal-NX0-and-embedded.tar.gz<br> This archive contains the TPTP NX0 representations of the 20 multi-modal<br> problems translated from the QMLTP library [1,2]. Additionally, it<br> contains the 20 embedded TF0 and the 20 embedded THF files created <br> from the NX0 files using the Logic Embedding Tool [3,4].<br> <br> - QMLTP-primary-evaluation-results-QMLTP.zip<br> This archive contains the primary evaluation data creating from<br> running E 3.0.03, Leo-III 1.7.8, Nitpick 2016, Vampire 4.8, <br> MleanCoP 1.3, nanoCoP-M 2.0 on the problem files.<br> All reasoning systems except Nitpick were run on the StarExec Miami cluster with a 60s<br> wall clock and 480 CPU time limit. The StarExec Miami computers have an<br> octa-core Intel Xeon E5-2667 3.20 GHz CPU, 128 GiB memory, and run the<br> CentOS Linux release 7.4.1708 operating system. Nitpick was run on a server<br> with a 60s wall clock time limit. The server has an octa-core Intel Xeon E5-<br> 2609 2.50 GHz CPU, 64 GiB memory, and the CentOS Linux release 7.9.2009<br> operating system.<br> <br> - README<br> This file.<br> <br> <br> <br>[1] T. Raths and J. Otten. The QMLTP Problem Library for First-Order Modal Logics.<br> In B. Gramlich, D. Miller, and U. Sattler, editors, Proceedings of the 6th International Joint Conference on Automated Reasoning,<br> number 7364 in Lecture Notes in Artificial Intelligence, pages 454–461. Springer, 2012.<br>[2] http://www.iltp.de/qmltp/<br>[3] A. Steen. An extensible logic embedding tool for lightweight non-classical reasoning (short paper).<br> In B. Konev, C. Schon, and A. Steen, editors, Proceedings of the 8th Workshop on Practical Aspects of Automated<br> Reasoning, number 3201 in CEUR Workshop Proceedings, 2022.<br>[4] https://github.com/leoprover/logic-embedding</p>
Dataset for Logical-layout analysis on French historical newspapers
<p><strong>Dataset for Logical-layout analysis on French historical newspapers</strong></p> <p>This dataset is intended for training and testing Logical Layout Analysis and recognition system on French historical documents published between 1900 and 1950. The original data is part of the "<a href="https://gallica.bnf.fr/services/engine/search/sru?operation=searchRetrieve&exactSearch=false&version=1.2&query=%28colnum%20adj%20%22Appartient%20%C3%A0%20l%27ensemble%20documentaire%20:%20FrancComt1%22%29">Fond régional: Franche-Comté</a>", which is curated by <a href="https://gallica.bnf.fr/accueil/fr/content/accueil-fr?mode=desktop">Gallica</a>, the digital portal of the Bibliothèque Nationale de France (BnF). This dataset has the following structure:</p> <p>├── train<br> ├── 1c<br> ├── cb32836282t<br> ├── cb32836282t.xml<br> ├── bpt6k112325g<br> ├── bpt6k112325g.xml<br> ├── truelabels_block.csv<br> ├── truelabels_line.csv<br> ├── …<br> ├── …<br> ├── 2c<br> ├── 3c+<br> └── test<br> ├── 1c<br> ├── 2c<br> └── 3c+</p> <p>The dataset is divided into a train and a test set. The train and test datasets have been designed to cover as much as possible the various possible layouts that exist in the "Fond régional: Franche-Comté" dataset. To do so, we have divided them into three layout types:<br> • <strong>1c</strong>: documents where the text is displayed in one column, as in books;<br> • <strong>2c</strong>: documents where the text is displayed into two columns;<br> • <strong>3c+</strong>: documents where there are at least 3 columns of text, as in newspapers.</p> <p>Each of the 1c, 2c, and 3c+ folder contains subfolders prefixed by ‘cb’, which contain a collection of documents. For instance, « cb32836282t » is the identifier used in Gallica for « Le Petit écho du 21e Régiment d'infanterie », a French military periodical published during WWI. An XML file with the same name, for instance «cb32836282t.xml », contains metadata about the collection, such as its title, publisher, creator, number of issues, etc. This XML file serves only to describe the collection, and is not to be used for Logical-Layout analysis.</p> <p>The issues in each collection can be found in the subfolders prefixed with « bpt ». For instance, « bpt6k112325g » is the identifier used in Gallica for an issue published in September 1917 of « Le Petit écho du 21e Régiment d'infanterie ». The information about each issue is given in three files, which are described below:</p> <p><strong>1-bptXXXXXXXXXX.xml </strong><br> The original data, as collected from Gallica. The most important tags of this document and their values are described below:<br> • <strong>oai</strong>: metadata about the document, such as its author, title, publisher, original publication date, number of issues, …<br> • <strong>image_url</strong>: the url to the document’s scan (in high resolution)<br> • <strong>pagination</strong>: a description of each page in the document (size of the page, if it contains a table of content or not, …)<br> • <strong>num_pages</strong>: the total number of pages in the document<br> • <strong>ocr</strong>: the OCR representation of the document in the XML ALTO format</p> <p>The XML ALTO format provides the text content and physical layout of documents in the following manner. Lines of text are contained in TextLine tags, which in their turn contain String tags for words and SP tags for spaces. TextLine tags are grouped into blocks in TextBlock tags. Sometimes, TextBlock tags are also grouped into ComposedBlock tags. TextBlock and TextLine tags have the following attributes:<br> • <strong>Id</strong> : the tag’s identifier<br> • <strong>Height</strong>, <strong>Width</strong> : the text height and width<br> • <strong>Vpos</strong> : the vertical position of the text on the page. The higher the value, the lower the word is on the page<br> • <strong>Hpos</strong> : the horizontal position of the text on the page. The higher the value, the further on the right the text is on the page<br> • <strong>Language</strong> : the language of the text (only for TextBlock tags).</p> <p>Among the attributes listed above, some TextBlock tags also have a Type attribute. This attribute contains logical labels of the lines in the block. In this dataset it appears most often for tables or advertisements. Overall, TextBlock tags that have a Type attribute are rare in this dataset (about 4 % only).</p> <p><strong>Note</strong>: The original scan of every document is accessible on the Gallica website, using the URL https://gallica.bnf.fr/ark:/12148/<IDENTIFIER>, where <IDENTIFIER> should be replaced by the id of the document (e.g.: bpt6k112325g) or the collection (e.g.: cb32836282t).</p> <p><strong>2-truelabels_block.csv </strong><br> A CSV file where each line corresponds to a TextBlock tag from the file bptXXXXXXXXXX.xml. This CSV file contains the following columns:<br> • <strong>page</strong>: the page on which the TextBlock tag is located<br> • <strong>block_id</strong>: the id of the TextBlock tag<br> • <strong>first_last_line</strong>: the text content of the first and last TextLine tags inside this TextBlock tag<br> • <strong>classes</strong>: the logical label(s) associated with this TextBlock tag</p> <p>The possible values in the column classes are : Text, Title, Header and Other.</p> <p><strong>3-truelabels_line.csv </strong><br> A CSV file where each line corresponds to a TextLine tag from the file bptXXXXXXXXXX.xml. This CSV file contains the following columns:<br> • <strong>page</strong>: the page where the TextLine tag is located<br> • <strong>block_id</strong>: the id of the TextBlock tag that contains this TextLine tag<br> • <strong>line_id</strong>: the id of this TextLine tag<br> • <strong>text_line</strong>: the text content of this TextLine tag<br> • <strong>classes</strong>: the logical label(s) associated with this TextLine tag</p> <p>The possible values in the column classes are : Text, Firstline, Title, Header and Other. Firstline indicates the « first line » of a paragraph.<br> </p>
Burst Noise Injection through Antenna Recorded on a UAV at Logic Level using HEIST
<p>A UAV exposed to burst noise injected through an antenna. The noise is recorded at logic level using HEIST.</p> <p> </p> <p>https://github.com/MaSkr09/heist_datalog.git</p>
Extending a High-Performance Prover to Higher-Order Logic
<p>This is the package containing raw evaluation data and other related data for the submission<br> Extending a High-Performance Prover to Higher-Order Logic.</p> <p>The problems used for the evaluation are stored in the problems/ directory. Higher-order TPTP benchmarks are in TPTP_HO subdirectory, while first-order TPTP benchmarks are in TPTP_FO subdirectory. Sledgehammer benchmarks are stored in SH subdirectory.</p> <p>Figures 2 and 3 in the submission are automatically created using Python script get_table.py from scripts/ directory. This script processes raw data obtained from StarExec, which is stored in the results/ directory.</p> <p>To create Figure 2 use the following command:</p> <p> python3 scripts/get_table.py results/ scripts/tptp_sh.json</p> <p>Figure 3 is created using:</p> <p> python3 scripts/get_table.py results/ scripts/fo.json</p> <p>Directory e-26-4 contains both first-order (eprover) and higher-order (eprover-ho)<br> binaries compiled under Ubuntu 18-04. The directory e-26-4 can be packaged in<br> an archive and submitted to StarExec for evaluation. starexec_run_as4_serialize.sh<br> was used on SH benchmarks, starexec_run_as8.sh was used on higher-order TPTP<br> benchmarks. starexec_run_fo-boa and starexec_run_ho-boa were used on first-order<br> benchmarks. To run the scripts locally, environment variables STAREXEC_CPU_LIMIT<br> and STAREXEC_WALLCLOCK_LIMIT must be set. Note these scripts do not limit any resources<br> of lambdaE and rely on StarExec facilities for this purpose.</p> <p> </p> <p>lambdaE was compiled from the master_bce_merge, branch of eprover github (https://github.com/eprover/eprover),<br> with the git commit hash 693e48236d18e6b9a8f60db9ff2c56503ed16945.</p>
Supplementary material and supplementary data files for: Handling logical character dependency in phylogenetic inference: Extensive performance testing of assumptions and solutions using simulated and empirical data
<p>Logical character dependency is a major conceptual and methodological problem in phylogenetic inference of morphological datasets, as it violates the assumption of character independence that is common to all phylogenetic methods. It is more frequently observed in higher-level phylogenies or in datasets characterizing major evolutionary transitions, as these represent parts of the tree of life where (primary) anatomical characters either originate or disappear entirely. As a result, secondary traits related to these primary characters become "inapplicable" across all sampled taxa in which that character is absent. Various solutions have been explored over the last three decades to handle character dependency, such as alternative character coding schemes and, more recently, new algorithmic implementations. However, the accuracy of the proposed solutions, or the impact of character dependency across distinct optimality criteria, has never been directly tested using standard performance measures. Here, we utilize simple and complex simulated morphological datasets analyzed under different maximum parsimony optimization procedures and Bayesian inference to test the accuracy of various coding and algorithmic solutions to character dependency. This is complemented by empirical analyses using a recoded dataset on palaeognathid birds. We find that in small, simulated datasets, absent coding performs better than other popular coding strategies available (contingent and multistate), whereas in more complex simulations (larger datasets controlled for different tree structure and character distribution models) contingent coding is favored more frequently. Under contingent coding, a recently proposed weighting algorithm produces the most accurate results for maximum parsimony. However, Bayesian inference outperforms all parsimony-based solutions to handle character dependency due to fundamental differences in their optimization procedures—a simple alternative that has been long overlooked. Yet, we show that the more primary characters bearing secondary (dependent) traits there are in a dataset, the harder it is to estimate the true phylogenetic tree, regardless of the optimality criterion, owing to a considerable expansion of the tree parameter space.</p>
Figure 4. Portal Logical Architecture-A Proposed Data Driven Architecture for Cardiology Network Application
<p>The applications that are based on a SOA environment can be configured to work both<br> as services exchanging data in point to point protocol and as a communication channel<br> between two entities that call a service provided by an entity that has the role of mediator or<br> broker. The letter can be seen as intermediary level that represents an “enterprise service bus”<br> (ESB) between service producers and consumers, offering messaging exchange services.</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.