[opentheory-users] necessity of the primitive inference rules

Ramana Kumar ramana.kumar at gmail.com
Thu Jan 13 23:17:35 UTC 2011


Are the OpenTheory inference rules (virtual machine commands that
leave theorems on the stack, apart from axiom) all necessary?
More precisely I mean are they any commands for which there are
certain imports and exports such that any article file with those
imports and exports must include the command, and one such article
exists?

I presume this is also a question about HOL Light's kernel, since
OpenTheory's inference rules are the same... right?



More information about the opentheory-users mailing list