Posted: Mar 13, 2012 8:48 am
by VazScep
mizvekov wrote:I have one question though, is it of any utility here to do something like this:
Code: Select all
inst (\v -> if v == "p" then (theoremTerm (inst (\v -> Var v) axiom3)) else Var "b") axiom1

Ie getting the term of a theorem (using theoremTerm) and then using that to instantiate another axiom?
Note that
Code: Select all
inst (\v -> Var v)
is just the identity.

It wouldn't surprise me if "inst" turned out to be useful. In this style of theorem prover, there is a lot of bootstrapping. You build a load of machinery on top of the kernel and then completely forget about the basic inference rules. This doesn't mean that the inference rules are useless. It just means that I haven't played with them much!

Hahaha cool, did you write that?
Oh, I wish! I think it appeared on the FSF mailing list at one time.