[opentheory-users] web tactics

[Ramana Kumar]

I have so far uploaded two "web tactics", which just make some piece
of HOL4 functionality available to others.
They are http://cam.xrchz.net/holqbf.cgi, which is described a bit in
this thread http://www.gilith.com/opentheory/mailing-list/2011-October/000184.html,
and http://cam.xrchz.net/skico.cgi, which removes abstractions from a
HOL term by rewriting it in combinatory form (using S,K,I,C, and o
(aka B)).

I have a note and a question for the list.
Note: holqbf.cgi will fail on any reasonably complicated QBF because
it tries to call an external SAT solver and I haven't uploaded one.
One of my next steps might be to make the HOL Light integration of
MiniSat into a web tactic, and then get holqbf to call it. I would
choose the integration into HOL Light because the kernel is closest to
OpenTheory's, but it might be interesting to see if there are
significant differences using say the HOL4 integration, or a
from-scratch OpenTheory integration.

I also wrote a little function in HOL4, url_conv : string -> term ->
thm, which takes the URL of a conversion and then calls and runs it.
In general, the term might not be of type bool, so the original plan
of encoding a term t as an article that just assumes and exports the
theorem |- t does not work. For the time being I am encoding a term as
an article that assumes and exports |- Function.Combinator.k
Data.Bool.F t.
Question: What do you think of this encoding scheme; would you prefer
something else?
Example alternatives are a dedicated tagging constant with the same
semantics as K, or a convention for taking a term left on the virtual
machine's stack (but that would get in the way of optimizing
articles).