Superposition for Full Higher-Order Logic

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 dynamic_cl in the package corresponds to outer in the paper; fluid_off (the base configuration) corresponds to immediate; and clausification_off corresponds to inner.