FundaÃÃo Cearense de Apoio ao Desenvolvimento Cientifico e TecnolÃgico / A noÃÃo de menor ponto-fixo de um operador à amplamente aplicada na ciÃncia da computaÃÃo como, por exemplo, no contexto das linguagens de consulta para bancos de dados relacionais. Algumas extensÃes da LÃgica de Primeira-Ordem (FOL)1 com operadores de ponto-fixo em estruturas finitas, como a lÃgica de menor ponto-fixo (LFP)2, foram propostas para lidar com problemas relacionados à expressividade de FOL. A LFP captura as classes de complexidade PTIME sobre a classe das estruturas finitas ordenadas. A caracterizaÃÃo descritiva de classes computacionais à uma abordagem central em Teoria do Modelos Finitos (FMT)3. O teorema de Trakhtenbrot, considerado o ponto de partida para FMT, estabelece que a validade sobre modelos finitos nÃo à recursivamente enumerÃvel, isto Ã, a completude falha sobre modelos finitos. Este resultado à baseado na hipÃtese de que qualquer sistema dedutivo à de natureza finita. Entretanto, nos podemos relaxar tal hipÃtese como foi feito no escopo da teoria da prova para aritmÃtica. A teoria da prova tem raÃzes no programa de Hilbert. ConseqÃÃncias teÃricas da noÃÃo de prova sÃo, por exemplo, relacionadas a teoremas de normalizaÃÃo, consistÃncia, decidibilidade, e resultados de complexidade. A teoria da prova para aritmÃtica tambÃm à motivada pelos teoremas de incompletude de GÃdel, cujo alvo foi fornecer um exemplo de um princÃpio matemÃtico verdadeiro e significativo que nÃo à derivÃvel na aritmÃtica de primeira-ordem. Um meio de apresentar esta prova à baseado na definiÃÃo de um sistema de prova com uma regra infinitÃria, a w-rule, que estabiliza a consistÃncia da aritmÃtica de primeira-ordem atravÃs de uma perspectiva de teoria da prova. Motivados por esta prova, iremos propor aqui um sistema infinitÃrio de prova para LFP que nos permitirà investigar propriedades em teoria da prova. Com tal sistema dedutivo infinito, pretendemos apresentar uma teoria da prova para uma lÃgica tradicionalmente definida no escopo de FMT. Permanece aberto um caminho alternativo de provar resultados jà obtidos com FMT e tambÃm novos resultados do ponto de vista da teoria da prova. AlÃm disso, iremos propor um procedimento de normalizaÃÃo com restriÃÃes para este sistema dedutivo, que pode ser usado em um provador de teoremas para computar consultas em banco de dados relacionais / The notion of the least fixed-point of an operator is widely applied in computer science
as, for instance, in the context of query languages for relational databases. Some extensions
of FOL with _xed-point operators on finite structures, as the least fixed-point logic
(LFP), were proposed to deal with problem problems related to the expressivity of FOL.
LFP captures the complexity class PTIME over the class of _nite ordered structures. The
descriptive characterization of computational classes is a central issue within _nite model
theory (FMT). Trakhtenbrot's theorem, considered the starting point of FMT, states that
validity over finite models is not recursively enumerable, that is, completeness fails over
finite models. This result is based on an underlying assumption that any deductive system
is of finite nature. However, we can relax such assumption as done in the scope of
proof theory for arithmetic. Proof theory has roots in the Hilbert's programme. Proof
theoretical consequences are, for instance, related to normalization theorems, consistency,
decidability, and complexity results. The proof theory for arithmetic is also motivated
by Godel incompleteness theorems. It aims to o_er an example of a true mathematically
meaningful principle not derivable in first-order arithmetic. One way of presenting this
proof is based on a definition of a proof system with an infinitary rule, the w-rule, that establishes
the consistency of first-order arithmetic through a proof-theoretical perspective.
Motivated by this proof, here we will propose an in_nitary proof system for LFP that
will allow us to investigate proof theoretical properties. With such in_nitary deductive
system, we aim to present a proof theory for a logic traditionally defined within the scope
of FMT. It opens up an alternative way of proving results already obtained within FMT
and also new results through a proof theoretical perspective. Moreover, we will propose a
normalization procedure with some restrictions on the rules, such this deductive system
can be used in a theorem prover to compute queries on relational databases.
| Identifer | oai:union.ndltd.org:IBICT/oai:www.teses.ufc.br:1168 |
| Date | 24 August 2007 |
| Creators | Alexandre Matos Arruda |
| Contributors | Ana Teresa de Castro Martins, Luiz Carlos Pinheiro Dias Pereira, Carlos Eduardo Fisch de Brito |
| Publisher | Universidade Federal do CearÃ, Programa de PÃs-GraduaÃÃo em CiÃncia da ComputaÃÃo, UFC, BR |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Biblioteca Digital de Teses e Dissertações da UFC, instname:Universidade Federal do Ceará, instacron:UFC |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.1022 seconds