Isabelle e PVS Falam sobre o Controle dos Demônios

 

                            O professor Fabrício de algoritmos falou do Isabelle e do PVS, que são programas provadores de teoremas, que proliferam numa quantidade incrível, na base de 100 mil deles por ano na Matemática. Naturalmente, o modelo o diz, já por princípio ou definição da Curva do Sino 50 % falsificarão ou terão tendência a falsificar, mesmo sob vigilância, para conseguir graus de mestre, de doutor ou de pós-doutor. Tais falsificações podem levar a erros grosseiros na prática e com isso a perigo de sobregasto de recursos e dinheiro, daí a sensatez de realmente fazer prosperar celeremente os controladores do tipo do Isabelle, do PVS e outros.

                            Em anexo há textos sobre o assunto, porque é candente.

                            De fato, na medida em que o mundo vai ficando mais e mais complexo os ladrões se munem de tantas complexas disposições lógicas que é difícil controlá-los. Os governempresas e as instituições universitárias devem mesmo instituir grupos-tarefa de perseguir os atrevidos (imagine que qualquer outro vá seguir um teorema errado durante anos a fio!). Ademais, existem os honestos, que erram acreditando que estão fazendo certo. Se os provadores estiverem largamente disponíveis eles mesmos poderão submeter-se aos testes reparadores (por enquanto ainda com a supervisão de lógicos, porque os programas – iniciando sua carreira – costumam desviar-se).

                            Vitória, sábado, 30 de abril de 2005.

                           

A LUTA CONTRA OS DEMÔNIOS (na Rede Cognata teorema = TEMPO = DEMÔNIOS = TRAÇOS = DOMÍNIOS = EQUAÇÕES e assim por diante)

Licenciatura em Matemática Aplicada e Computação 2004/2005 Lógica Computacional Área Científica: Teoria da Computação 1º semestre, 3º ano Disciplina da responsabilidade da Secção de Lógica e Computação do Departamento de Matemática do Instituto Superior Técnico.

O que é Lógica?  Lógica é o estudo sistemático do pensamento dedutivo, que permite construir argumentos corretos nas ciências naturais nas ciências humanas e nas ciências formais, e que possibilita distinguir os argumentos corretos dos incorretos. Dessa forma, a questão central da Lógica é: o que significa filosófica e simbolicamente, que um argumento decorra (ou seja consequência) das premissas adotadas? Saudações, Joao Marcos.