Superposition for Full Higher-Order Logic

Dataset / Software

Description

This package contains problems used for evaluation, and the raw evaluation data, and the scripts necessary for the reproduction of the results for the conference paper Superposition for Full Higher-Order Logic, the associated technical report, and the journal article Superposition for Higher-Order Logic.

Zipperposition is available at https://github.com/sneeuwballen/zipperposition. See the README file in the archive below for detailed instructions on how to run it.

Note: For Figure 2, configuration <em>dynamic_cl</em> in the package corresponds to <em>outer</em> in the paper; <em>fluid_off </em>(the base configuration) corresponds to <em>immediate</em>; and <em>clausification_off </em>corresponds to <em>inner</em>.
Date made available2021
PublisherZenodo

Cite this