List of statements for verifying ATPs

Miscellaneous
1

Greetings,

To verify automated theorem provers (ATP), datasets from for instance TPTP are used (tptp.org). Now, I am interested in verifying our ATP. Currently, I am only focussed on solving statements with Intuitionistic propositional logic at this time, so www.iltp.de provides a dataset in the TPTP format. Is there a straight forward way to translate this list of statements to Coq language? I need to get these statements into strings of plaintext, as the ATP interfaces with coq over sertop.

Alternatively, is there another dataset that contains statements that can be solved using intuitionistic propositional logic? I have looked through the dataset CoqGym provides but I did not find any proper indication of what was IPL.

Thank you for your help!

2

CoqHammer has a translation going in the other direction.

Here is a summary of the state of the art of Coq intuitionistic provers as of a few years ago:

It may be worth reaching out to the author of that abstract to see if he had a translation for the evaluation.

See also the discussion here:

3

Sorry if I don’t understand your question. Why doesn’t using the TPTP data set satisfy your needs to verify your ATP? Why do you need to translate to the Coq language?