[isabelle] How does one load TPTP theorems?
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and