I disagree. The UD will have a particular way of generating (or
enumerating) the theorems of the FAS, such that it doesn't generate
the same theorem twice. However, that is not to say that the proofs it
generates are elegant, as other proof algorithms exist, which may
generate shorter proofs. I would think that moreover it is impossible
to ascertain in general whether a particular proof output by the UD is
elegant or not, as this appears to be equivalent to the problem of
evaluating the K-complexity of a given program, which is known to be
uncomputable.
Cheers
Hal Ruhl wrote:
>
> Dear Russell:
>
> To condense the idea the UD is generating the collection of strings by the
> only path it has so the proof is automatically elegant.
>
> It is also extremely complex.
>
> Hal
>
----------------------------------------------------------------------------
Dr. Russell Standish Director
High Performance Computing Support Unit, Phone 9385 6967
UNSW SYDNEY 2052 Fax 9385 6965
Australia R.Standish.domain.name.hidden
Room 2075, Red Centre
http://parallel.hpc.unsw.edu.au/rks
----------------------------------------------------------------------------
Received on Thu Apr 19 2001 - 21:22:26 PDT