Please use this identifier to cite or link to this item: http://hdl.handle.net/10316/47640
DC FieldValueLanguage
dc.contributor.advisorAlmeida, Pedro Henrique e Figueiredo Quaresma de-
dc.contributor.advisorCosta, Ernesto Jorge Fernandes-
dc.contributor.authorAires, Jorge Adriano Branco-
dc.date.accessioned2018-02-16T18:02:43Z-
dc.date.available2018-02-16T18:02:43Z-
dc.date.issued2004-
dc.identifier.urihttp://hdl.handle.net/10316/47640-
dc.description.abstractSistemas 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.por
dc.language.isoporpor
dc.rightsopenAccesspor
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/por
dc.titleImplementação e automação de sistemas de deduçãopor
dc.typemasterThesispor
thesis.degree.nameDissertação de Mestrado em Engenharia Informática apresentada à Faculdade de Ciências e Tecnologia da Universidade de Coimbrapor
item.languageiso639-1pt-
item.grantfulltextopen-
item.fulltextCom Texto completo-
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 simple item record

Page view(s) 50

346
checked on Oct 22, 2019

Download(s)

54
checked on Oct 22, 2019

Google ScholarTM

Check


This item is licensed under a Creative Commons License Creative Commons