[isabelle] How does one load TPTP theorems?



Greetings!

Sorry for maybe a very basic question, but is there a possibility to get automatic proofs 
for theorems from TFF/THF files from TPTP site?

On TPTP site I read the following: "Isabelle includes a parser for the TPTP syntaxes CNF, 
FOF, TFF0, and THF0, due to Nik Sultana." So I installed Isabelle, see that there is a 
number of TPTP related theories, but cannot figure out how to load into Isabelle theorems 
from "*.p" files. 

Should .p files first be converted to .thy files with some command-line 
tool? Or can one refer (include) to .p files from .thy files?

Can someone help please?


Thanks.

Albert Berger. 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.