Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How does one load TPTP theorems?

Email Gateway (Aug 22 2022 at 15:12):

From: Albert Berger <nbdspcl@gmail.com>
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.

Email Gateway (Aug 22 2022 at 15:12):

From: Albert Berger <nbdspcl@gmail.com>
Dear Jasmin,

many thanks! That works.

Best regards,

Albert Berger.

Tue, Mar 07, 2017 at 03:34:46PM +0100, Blanchette, J.C. wrote:

Last updated: Apr 23 2024 at 16:19 UTC