[lojban-beginners] Re: logical proofs?

[jkominek@miranda.org]

On Tue, Aug 24, 2004 at 09:29:43AM +1200, mikevdg@gulik.co.nz wrote:
> What I'm interested in is whether it is possible that this could be
> mechanically derived, for example by somebody using a proof
> assistant such as COQ, but using lojban? I.e are all the steps in
> the proof mechanical enough to convince a computer that (e.g.) prime
> numbers are infinite?

I'll have to admit that I didn't even try reading the proof, but, one
could certainly restrain themselves to some sort of ritualized subset
of Lojban which was analagous to the syntax used by MetaMath
(http://metamath.org). At that point, the proofs could be mechanically
verified, manipulated, etc, just as the MetaMath ones are. Short of that,
mechanically understanding proofs is probably a bit too inherently
difficult.

-- 
Jay Kominek <jkominek@miranda.org>
UNIX is all about covering up
the fact that you can't type.