Experimental Data on Translations from Higher-Order Clauses to First-Order Clauses

Here you can download the theorem prover input files used for the experiments described in the paper "Translating Higher-Order Clauses to First-Order Clauses" by Paulson and Meng. The following items are available, all compressed to tbz format.

The ATP directories also include the outputs generated by the experiments themselves. Look for files matching the patterns output*.txt and error*.txt.

Subdirectories called 0Vminimal and 0Eminimal contain versions of the problems that have been automatically reduced by Vampire or E, respectively. Subdirectories called 0Vsoundness and 0Esoundness are similar, but the reduced problems have been converted to the fully-typed translation, for soundness testing.

Last modified 12 January, 2012


Lawrence C. Paulson