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! -------------------------------------------------------------------------------