Posted By: Lumo (www.visaci.cz/~lumo) on 'CZscience'
Title:     Pocitacove dokazovani
Date:      Thu Aug 28 09:00:42 1997

Ahoj Earle!

>  Ale trochu jinak. Pokud je totiz definovano, co to je formalni dukaz, neni
> problem vytvorit celou axiomatiku iterovanim nejakych pravidel na jeji
> axiomy. Kazda veta neodpovidajici formalnimu dukazu neni dokazatelna. Howg.

To je sice lakava idea, ale asi nikdy nebude mozne, aby pocitace touto hrubou 
iterativni silou hledaly nove zajimave vety. Je to podobne, jako kdybys 
pocitac nechal vypisovat postupne vsechny stopismenne texty "aaaaaa....aaa", 
"aaaaa....aab"... a cekal, az ti z toho vypadne Romeo a Julie. Presto jsem v 
pokuseni verit, ze aspon urcite logicke kroky se pocitace velmi dobre nauci.

      /////  Superstring/M-theory is the language in which God wrote the world.
    /// O __        Your Lumidek.  mailto:motl@karlin.mff.cuni.cz
   ///           ---------------------------------------------------
  ///_______/             http://www.kolej.mff.cuni.cz/~lumo/
Mazte zbytecne casti replikovanych postu. Uzijte hmat CTRL/K pro smazani radky!
-------------------------------------------------------------------------------