|
Abstract:
|
Expõe que ambos os métodos, tanto dos Tableaux como das Resoluções fazem parte daquilo que se chama prova automática de teoremas. O método da Resolução trabalha com prova por refutação: "se a negação de um teorema é falsa, então ele será verdadeiro." Este método é baseado em uma regra de inferência única, chamada regra de resolução, e utiliza intensivamente um algoritmo de casamento de padrões chamado algoritmo de unificação. Faz-se algumas comparações entre os dois métodos, pois, o algoritmo dos Tableaux não necessita de transformações para qualquer forma normal. Revela que a principal vantagem do método dos Tableaux, em relação ao método tradicional e conhecido de Resolução é fato deste evitar utilização de cláusulas nas suas formas. Forma de Medição no Processo de Alfabetização dos (as) Alunos (as) com Necessidades Educativas Especiais |
