The Public Works Tax Deduction Law has been enacted to foster public investment at a local and regional level by including participation from the private sector and through the subscription of agreements with local and regional governments.Nonetheless its noble purposes, in the application field of the Law, normative gaps are put into evidence, which impede its practical application. In the present article, the author shows which are the Law’s deficiencies, while analyzing them and proposing possible solutions. / La Ley de Obras por Impuestos tiene como objetivo principal impulsar la inversión pública de impacto regional y local, con la participación del sector privado, mediante la suscripción de convenios con los gobiernos regionales y/o locales.No obstante su noble propósito, en el ámbito aplicativo de la ley se evidencian ciertos vacíos normativos que dificultan su aplicación práctica. Es así que –en el presente artículo– la autora nos muestra cuáles son estas deficiencias a la vez que, luego de hacer un análisis de las mismas, nos propone posibles soluciones.

ARRUDA, Alexandre Matos. Um sistema infinitário para a lógica de menor ponto fixo. 2007. 91 f. : Dissertação (mestrado) - Universidade Federal do Ceará, Departamento de Computação, Fortaleza-CE, 2007. / Submitted by guaracy araujo (guaraa3355@gmail.com) on 2016-05-20T15:28:27Z No. of bitstreams: 1 2007_dis_amarruda.pdf: 427889 bytes, checksum: b0a54f14f17ff89b515a4101e02f5b58 (MD5) / Approved for entry into archive by guaracy araujo (guaraa3355@gmail.com) on 2016-05-20T15:29:23Z (GMT) No. of bitstreams: 1 2007_dis_amarruda.pdf: 427889 bytes, checksum: b0a54f14f17ff89b515a4101e02f5b58 (MD5) / Made available in DSpace on 2016-05-20T15:29:23Z (GMT). No. of bitstreams: 1 2007_dis_amarruda.pdf: 427889 bytes, checksum: b0a54f14f17ff89b515a4101e02f5b58 (MD5) Previous issue date: 2007 / 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. / 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

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.

Dependency parsing can be a useful tool to allow computers to parse text. In 2015, Kuhlmann and Jonsson proposed a logical deduction system that parsed to non-crossing dependency graphs with an asymptotic time complexity of O(n3), where “n” is the length of the sentence to parse. This thesis extends the deduction system by Kuhlmann and Jonsson; the extended deduction system introduces certain crossing edges, while maintaining an asymptotic time complexity of O(n4). In order to extend the deduction system by Kuhlmann and Jonsson, fifteen logical item types are added to the five proposed by Kuhlmann and Jonsson. These item types allow the deduction system to intro-duce crossing edges while acyclicity can be guaranteed. The number of inference rules in the deduction system is increased from the 19 proposed by Kuhlmann and Jonsson to 172, mainly because of the larger number of combinations of the 20 item types. The results are a modest increase in coverage on test data (by roughly 10% absolutely, i.e. approx. from 70% to 80%), and a comparable placement to that of Kuhlmann and Jonsson by the SemEval 2015 task 18 metrics. By the method employed to introduce crossing edges, derivational uniqueness is impossible to maintain. It is hard to defien the graph class to which the extended algorithm, QAC, parses, and it is therefore empirically compared to 1-endpoint crossing and graphs with a page number of two or less, compared to which it achieves lower coverage on test data. The QAC graph class is not limited by page number or crossings. The takeaway of the thesis is that extending a very minimal deduction system is not necessarily the best approach, and that it may be better to start off with a strong idea of to which graph class the extended algorithm should parse. Additionally, several alternative ways of extending Kuhlmann and Jonsson are proposed. / Dependensparsning kan vara ett användbart verktyg för att få datorer att kunna läsa text. Kuhlmann och Jonsson kom 2015 fram till ett logiskt deduktionssystem som kan parsa till ickekorsande grafer med en asymptotisk tidskomplexitet O(n3), där "n" är meningens som parsas längd. Detta arbete utökar Kuhlmann och Jonssons deduktionssystem så att det kan introducera vissa korsande bågar, medan en asymptotisk tidskomplexitet O(n4) uppnås. För att tillåta deduktionssystemet att introducera korsande bågar, introduceras 15 nya logiska delgrafstyper, eller item. Dessa item-typer tillåter deduktionssystemet att introducera korsande bågar på ett sådant sätt att acyklicitet bibehålls. Antalet logiska inferensregler tags från Kuhlmanns och Jonssons 19 till 172, på grund av den större mängden kombinationer av de nu 20 item-typerna. Resultatet är en mindre ökning av täckning på testdata (ungefär 10 procentenheter, d v s från cirka 70% till 80%), och jämförbar placering med Kuhlmann och Jonsson enligt måtten från uppgift 18 från SemEval 2015. Härledningsunikhet kan inte garanteras på grund av hur bågar introduceras i det nya deduktionssystemet. Den utökade algoritmen, QAC, parsar till en svårdefinierad grafklass, som jämförs empiriskt med 1-endpoint-crossing-grafer och grafer med pagenumber 2 eller mindre. QAC:s grafklass har lägre täckning än båda dessa, och har ingen högre gräns i pagenumber eller antal korsningar. Slutsatsen är att det inte nödvändigtvis är optimalt att utöka ett mycket minimalt och specifikt deduktionssystem, och att det kan vara bättre att inleda processen med en specifik grafklass i åtanke. Dessutom föreslås flera alternativa metoder för att utöka Kuhlmann och Jonsson.