[opentheory-users] Importing from the Gilith OpenTheory Repo

[Rob Arthan]

Ramana,

On 24 Nov 2013, at 09:45, Ramana Kumar wrote:

> I think the idea of the base package is that everything in it should already be supported by your theorem prover, so you don't need to import it - rather, you use it as a dependency for things you export from your theorem prover.
> 
I want to import it so I can have a better look at it. The kind of thing I want to do is to make sure that my reader can prove all the assumptions in it and to make sure that my writer only uses definitions and theorems that it provides when it is writing out a ProofPower inference as a sequence of OpenTheory inferences.

> That said, I think you can generate a single article that performs all the proofs in a package, like base, using the opentheory tool with the info command and the --article option.
> 
I invoked opentheory like this:

	opentheory info --article base

and after 12 minutes learnt that I should have invoked it like this:

	opentheory info --article base >base.art

I am then able to import all 1117 theorems and 3 assumptions from base.art into ProofPower.

Thanks!

Rob.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20131124/0a2dd0d2/attachment.html>