Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pós-Graduação em Ciência da Computação. / Made available in DSpace on 2012-10-19T11:45:02Z (GMT). No. of bitstreams: 0Bitstream added on 2014-09-26T00:14:39Z : No. of bitstreams: 1
184301.pdf: 1994981 bytes, checksum: 06897e01ca96b80d4e81bfbdf621f13c (MD5) / 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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/82117 |
| Date | January 2001 |
| Creators | Knoblauch, Helmut Willy |
| Contributors | Universidade Federal de Santa Catarina, Barreto, Jorge Muniz |
| Publisher | Florianópolis, SC |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFSC, instname:Universidade Federal de Santa Catarina, instacron:UFSC |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0015 seconds