2017-04-26 2:55 GMT+02:00 Marcelo Finger <[email protected]>: > > Sobre provas geradas automaticamente, em especial para o caso da > 4-coloração, avento a possibilidade de que uma prova automaticamente > gerada (e verificada) possa term MAIS CASOS que a atualmente > conhecida. > > Aliás, isso seria o esperado. Se é fácil gerar e verificar casos, é > provável que seja assim programado.
Confesso que não sei dizer se a demonstração automatizada tem mais casos do que os que seriam previstos... Na demonstração original de Appel & Haken [1976] havia 1936 mapas "minimais" com 5 cores a analisar (a estratégia da demonstração, seguindo a ideia principal da demonstração errada publicada por Kempe em 1879, é justamente a do raciocínio por absurdo, mostrando que cada uma destas configurações pode ser reduzida a uma configuração menor que ainda necessitaria 5 cores). Em 1996, Robertson et al mostraram que é possível diminuir o número de casos a considerar para "apenas" 633 configurações. Até onde sei, foi esta última versão da demonstração que foi formalizada pelo Gonthier. Abraços, Joao Marcos -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para postar neste grupo, envie um e-mail para [email protected]. Visite este grupo em https://groups.google.com/a/dimap.ufrn.br/group/logica-l/. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LgphyNLZSRJyrfmMzga7UtRebWyyc7gZL6m%2BHWPpdTruQ%40mail.gmail.com.
