[opentheory-users] necessity of the primitive inference rules

[Joe Hurd]

Hi Ramana,

I'm not an expert in these matters, but I believe that John Harrison
chose a minimal kernel for HOL Light, so every inference rule is
necessary. There is one exception to this, which is that he included
the TRANS rule

 A |- t = u  B |- u = v
---------------------------
      A u B |- t = v

in the logical kernel, even though it can be derived from the other rules.

The OpenTheory kernel is essentially the same as the HOL Light kernel,
except that it does not include a TRANS rule. Instead, the logging
code (in logging.ml) looks like

            | Trans_proof (th1,th2) ->
                let tm = rator (concl th1) in
                let () = log_term tm in
                let () = log_command "refl" in
                let () = log_thm th2 in
                let () = log_command "appThm" in
                let () = log_thm th1 in
                let () = log_command "eqMp" in
                ()

which reduces TRANS to refl, appThm and eqMp.

Cheers,

Joe

On Thu, Jan 13, 2011 at 3:17 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> 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?
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>