[opentheory-users] extracting intermediate theorems

[Joe Leslie-Hurd]

Hi Ramana,

> Is there a way to get the OpenTheory tool to do any of the following?
>
> Show me the intermediate (i.e. unexported) theorems that arise when running
> an article.

No, unfortunately not. The best it can do is tell you *how many*
theorems are generated, by using the --inference option:

$ opentheory info --inference base
Inference rules:
subst .............. 72,087
eqMp ............... 60,924
appThm ............. 40,895
proveHyp ........... 17,201
betaConv ........... 16,499
absThm ............. 12,581
trans .............. 12,292
refl ............... 10,727
deductAntisym ....... 7,995
sym ................. 7,695
assume .............. 4,247
axiom ............... 3,184
defineConst ........... 159
defineConstList ........ 63
defineTypeOp ........... 13
Total ............. 266,562

Did you have any thoughts on a way to present intermediate theorems to the user?

> Create an article that exports a previously unexported theorem, taking an
> existing article as input.

Also no I'm afraid.

> Minimise an article for what is required for a particular theorem (I think
> the answer here is yes, by creating a package with the desired theorem and
> then asking for an article for it to be generated...?)

Indeed. Suppose article foo.art exports a set of theorems containing a
theorem T of interest, then you can create an article bar.art that
proves T by axiom, and then run

echo 'a { article: "foo.art" } main { import: a article: "bar.art" }'
| opentheory info --article -o baz.art theory:-

to get a minimal article baz.art proving T.

Cheers,

Joe