rationalskepticism.org

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.