[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