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


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                                [EMAIL PROTECTED]             
Room 2075, Red Centre                    http://parallel.hpc.unsw.edu.au/rks

Reply via email to