info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Is it possible to load theorems from TPTP files?
23 views
Skip to first unread message
nbd...@gmail.com
Mar 6, 2017, 11:51:33 AM3/6/17
to
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.
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.
0 new messages