Please use this identifier to cite or link to this item: http://hdl.handle.net/10316/47640
Title: Implementação e automação de sistemas de dedução
Authors: Aires, Jorge Adriano Branco 
Orientador: Almeida, Pedro Henrique e Figueiredo Quaresma de
Costa, Ernesto Jorge Fernandes
Issue Date: 2004
Abstract: Sistemas lógicos permitem descrever e raciocinar de forma rigorosa acerca dos mais variados domínios, sejam eles teorias matemáticas abstractas como álgebra, análise ou geometria, ou áreas mais aplicadas como especificação de software, verificação de hardware ou processamentode linguagens naturais. Este rigor é conseguido à custa da utilização de linguagens bem definidas, que podem ser interpretadas de forma precisa sobre os domínios que pretendemos estudar. Assim, construíndo frases nestas linguagens lógicas, que designamos por proposições ou fórmulas, expressamos propriedades nos respectivos domínios, que poderão ser satisfeitas sempre, nunca, ou apenas mediante determinadas circunstâncias. Interessa-nos conseguir raciocinar acerca destas propriedades, ser capazes de determinar se são ou não sempre verificadas no nosso domínio de estudo, ou de um modo mais geral, se são verificadas mediante determinadas condições, ou seja, como consequência da verificação de certas propriedades no domínio. Tomando como exemplo a área da aritmética de inteiros, podemos querer tentar determinar se "qualquer número inteiro pode ser escrito como a soma de dois quadrados perfeitos", ou não. Uma representação comum desta frase num sistema lógico é dada por Vk. Ǝ m. Ǝ n. k = m2 + n2. Para que este tipo de estudo seja efectuado de forma rigorosa, é necessário não só a representação e interpretação precisa destas propriedades, mas uma base formal, perfeitamente definida, que sirva de suporte aos raciocínios efectuados durante esse mesmo estudo. Os sistemas lógicos dedutivos formam essa base. Tomando como ponto de partida relações de consequência elementares entre fórmulas (axiomas) e regras básicas que permitem inferir novas conclusões a partir de consequências conhecidas ou assumidas válidas num determinado contexto (regras de inferência), é possível criar e apresentar raciocínios de forma clara e concisa acerca dos objectos de estudo, ou seja, efectuar demonstrações no sistema. O objectivo deste trabalho passa por estudar sistemas lógicos dedutivos, com especial ênfase na sua implementação numa linguagem de programação (Haskell), tendo em vista a automação do processo de demonstração.
URI: http://hdl.handle.net/10316/47640
Rights: openAccess
Appears in Collections:FCTUC Eng.Informática - Teses de Mestrado

Files in This Item:
File Description SizeFormat
Tese_JorgeAires_2005.pdf684.6 kBAdobe PDFView/Open
Show full item record

Page view(s) 50

340
checked on Sep 18, 2019

Download(s)

53
checked on Sep 18, 2019

Google ScholarTM

Check


This item is licensed under a Creative Commons License Creative Commons