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.
5
datasets available to search
ShareScore release 0.9.0
Dataset results
5 results for “higher-order 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>
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>
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>
Superposition for Lambda-Free Higher-Order Logic — Supplementary Material for the Journal Article
<p>We provide the following supplementary material for our <a href="http://matryoshka-project.github.io/pubs/lfhosup_article.pdf">article</a>.</p> <p><strong>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/sneeuwballen/zipperposition#starexec">Zipperposition readme</a>. We used OCaml 4.07.0, branch <code>lmcs2020</code>, commit <a href="https://github.com/sneeuwballen/zipperposition/tree/2031e216c1941acd76187882a073e8f1e53383f2">2031e216c1941acd76187882a073e8f1e53383f2</a></p> <p><strong>Problems</strong></p> <p>We used the following first-order (TFF) and the higher-order (THF) <a href="http://www.cs.miami.edu/~tptp/">TPTP (v7.3.0) problems</a> for the evaluation: <a href="https://zenodo.org/record/3992618/files/list_TFF.txt">TFF problem list</a> <a href="https://zenodo.org/record/3992618/files/list_THF.txt"> THF problem list</a>. These lists were obtained by excluding all problems that contain arithmetic, the symbols <code>(@@+)</code>, <code>(@@-)</code>, <code>(@+)</code>, <code>(@-)</code>, <code>(&)</code>, or tuples, as well as the <code>SYN000</code> problems, which are only intended to test the parser, and problems whose clausal normal form takes longer than 15s to compute or falls outside the lambda-free fragment. The following archive contains instructions on how the benchmarks were selected: <a href="https://zenodo.org/record/3992618/files/benchmark_selection.zip">Benchmark selection</a></p> <p>Note that Zipperposition is not aware that our calculi are complete for this fragment and it will always report "GaveUp" instead of "CounterSatisfiable" if the calculus saturates.</p> <p>The selection of TPTP problems and the problems generated by Isabelle/Sledgehammer can be downloaded here: <a href="https://zenodo.org/record/3992618/files/benchmarks.zip">Benchmarks</a></p> <p><strong>Run scripts</strong></p> <p>We used the following run scripts on StarExec. This archive also contains the Zipperposition binary, compiled for StarExec: <a href="https://zenodo.org/record/3992618/files/run_scripts.zip">StarExec run scripts</a></p> <p>The scripts use the following command-line options for Zipperposition</p> <ul> <li>First-order mode:<br> <code>./zipperposition.exe --mode=fo-complete-basic</code></li> <li>Applicative encoding mode (intensional):<br> <code>./zipperposition.exe --mode=fo-complete-basic --app-encode=intensional</code></li> <li>Applicative encoding mode (extensional):<br> <code>./zipperposition.exe --mode=fo-complete-basic --app-encode=extensional</code></li> <li>Nonpurifying intensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-intensional</code></li> <li>Nonpurifying extensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-extensional</code></li> <li>Purifying intensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-purify-intensional</code></li> <li>Purifying extensional calculus:<br> <code>./zipperposition.exe --mode=lambda-free-purify-extensional</code></li> </ul> <p>As additional command line arguments, we provided the problem's filename, the order (<code>--ord=lambdafree_rpo</code> or <code>--ord lambdafree_kbo</code> or <code>--ord epo</code>), and the following parameters for heuristics that were obtained by optimizing the first-order mode in preliminary experiments:</p> <pre>--kbo-weight-fun=modarity \ -q "7|prefer-sos|pnrefined(2,1,1,1,2,2,2)" \ -q "4|prefer-short-trail|pnrefined(1,1,1,2,2,2,0.5)" \ -q "1|prefer-processed|fifo" \ -q "7|prefer-ground|conjecture-relative-var(1,l,f)" \ -q "6|prefer-goals|conjecture-relative-var(1,s,f)" \ --select=e-selection7 </pre> <p>On Starexec, we chose a wallclock timeout of 360 s, a CPU timeout of 180 s, and a memory limit of 128 GB. StarExec's machine specifications are:</p> <pre>Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz (2393 MHZ) 10240 KB Cache 263932744 kB main memory OS: CentOS Linux release 7.7.1908 (Core) kernel: 3.10.0-1062.4.3.el7.x86_64 </pre> <p><strong>Results</strong></p> <p>Download the raw output of the evaluation and the .csv files created by StarExec here:</p> <ul> <li><a href="https://zenodo.org/record/3992618/files/results_tff.zip">Raw evaluation output TFF</a></li> <li><a href="https://zenodo.org/record/3992618/files/results_sh256.zip">Raw evaluation output SH256</a></li> <li><a href="https://zenodo.org/record/3992618/files/results_sh16.zip">Raw evaluation output SH16</a></li> <li><a href="https://zenodo.org/record/3992618/files/results_thf.zip">Raw evaluation output THF</a></li> <li><a href="https://zenodo.org/record/3992618/files/results_csv.zip">Evaluation results as CSV file + script to compile the statistics</a></li> </ul> <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="https://zenodo.org/record/3992618/files/example_varcond.zf">Example 3.3</a></li> <li><a href="https://zenodo.org/record/3992618/files/example_posext.zf">Example 3.4</a></li> <li><a href="https://zenodo.org/record/3992618/files/example_supatvars_rpo.zf">Example 3.5</a></li> <li><a href="https://zenodo.org/record/3992618/files/example_negext.zf">Example 3.6</a></li> <li><a href="https://zenodo.org/record/3992618/files/example_add_equiv_defs.p">Example 3.7</a></li> </ul>
Constraint Superposition for Higher-order Logic
<p>This archive contains the evaluation results, scripts, problems and executables used for the evaluation in the thesis "Constraint Superposition for Higher-order Logic".</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.