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

The primary objective of this thesis is to assess the impacts of VAT on municipal economy, to determine when it is advisable for a municipality to become a VAT payer and how the VAT payership affects the municipality{\crq}s income, and what the associated rights and obligations are. Based on an analysis, we review Municipality ``X{\crqq} that registered for VAT voluntarily on July 1, 2004 and Municipality ``Y{\crqq} that only became a VAT payer beginning January 1, 2009. According to the information revealed, the VAT registration associated financial benefits for Municipality X were closely connected with its financial investments made with the assistance of received subsidies and capital investments into property. Compared to Municipality X, the implications are that Municipality Y would have not benefited from becoming a voluntary VAT payer. The anticipated financial effect would have been neutral. At present, we can state that the greatest financial benefits for municipalities under the VAT scheme arise from investments into the renovation, repairing work or construction of water-supply and public sewer systems provided that the municipality operates or lets it on lease to another VAT payer.

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.

Essay I: Employment Security Agreements, which are elements of Swedish collective agreements, offer a unique opportunity to study very early job search counselling of displaced workers. These agreements provide individual job search assistance to workers who are dismissed due to redundancy, often as early as during the period of notice. Compared to traditional labor market policies, the assistance provided is earlier and more responsive to the needs of the individual worker. In this study, I investigate the effects of the individual counseling and job search assistance provided through the Employment Security Agreement for Swedish blue-collar workers on job finding and subsequent job quality. The empirical strategy is based on the rules of eligibility in a regression discontinuity framework. I estimate the effect for workers with short tenure, who are dismissed through mass-layoffs. My results do not suggest that the program has an effect on the probability of becoming unemployed, the duration of unemployment, or income. However, the results indicate that the program has a positive effect on the duration of the next job. Essay II: The well-known positive relationship between the unemployment benefit level and unemployment duration can be separated into two potential sources; a moral hazard effect, and a liquidity effect pertaining to the increased ability to smooth consumption. The latter is a socially optimal response due to credit and insurance market failures. These two effects are difficult to separate empirically, but the social optimality of an unemployment insurance policy can be evaluated by studying the effect of a non-distortionary lump-sum severance grant on unemployment durations. In this study, I evaluate the effects on unemployment duration and subsequent job quality of a lump-sum severance grant provided to displaced workers, by means of a Swedish collective agreement. I use a regression discontinuity design, based on the strict age requirement to be eligible for the grant. I find that the lump-sum grant has a positive effect on the probability of becoming unemployed and the length of the completed unemployment duration, but no effect on subsequent job quality. My analysis also indicates that spousal income is important for the consumption smoothing abilities of displaced workers, and that the grant may have a greater effect in times of more favorable labor market conditions. Essay III: Evidence from around the world suggest that individuals who are awarded disability benefits in some cases still have residual working capacity, while disability insurance systems typically involve strong disincentives for benefit recipients to work. Some countries have introduced policies to incentivize disability insurance recipients to use their residual working capacities on the labor market. One such policy is the continuous deduction program in Sweden, introduced in 2009. In this study, I investigate whether the financial incentives provided by this program induce disability insurance recipients to increase their labor supply or education level. Retroactively determined eligibility to the program with respect to time of benefit award provides a setting resembling a natural experiment, which could be used to estimate the effects of the program using a regression discontinuity design. However, a simultaneous regime change of disability insurance eligibility causes covariate differences between treated and controls, which I adjust for using a matching strategy. My results suggest that the financial incentives provided by the program have not had any effect on labor supply or educational attainment.

[pt] Existem diferentes estilos de cálculos dedutivos, usados para derivar os teoremas de uma lógica. Os mais habituais são os sistemas axiomáticos; mas, do ponto de vista da teoria da prova, os sistemas em dedução natural parecem ser mais interessantes. Essa é a motivação que leva ao desenvolvimento de técnicas que visam a facilitar a transformação de um cálculo dedutivo para o estilo em dedução natural. Esse trabalho se concentra no aspecto de modelar regras para os quantificadores da linguagem considerada e, para isso, faz uso de rótulos. Após uma apresentação intuitiva da técnica desenvolvida, passa-se à exposição de sistemas lógicos tratados pelo método: lógica de ultrafiltros, lógica de filtros, CTL, lógica de Keisler e CTL*. Em cada caso, analisam-se aspectos de teoria da prova. / [en] There are many kinds of deductive calculus. The axiomatic ones are the more usual. However, from the point of view of proof theory, Natural Deduction systems seem to be more interesting. This is the motivation for developping a technique that aims to ease the transformation from deductive calculus to Natural Deduction style. This work concentrates on the aspect of modeling the rules for the quantifiers of the logic considered, and for this purpose labels are used. After an intuitive presentation of the technique developped, some logical systems are treated by the method: ultrafilter logic, filter logic, CTL, Keisler`s logic and CTL*. For each one of them proof-theoretical aspects are analysed.

The main question this dissertation addresses is which sermon forms are the most befitting for effective and communicative preaching within the context of the Korean church. The background to this question being the fact that most of the Korean sermons are structured according to the traditional method, namely a three-point sermon structure. It seems that no real analysis has been made of the hearers, as well as the different styles of worship being encountered in the Korean church. This leads to the fact that sermons (sermon forms) are structured in such a manner that the hearers are unable to follow either the sermon’s content or the sermon’s movements. This results in the preacher experiencing a lack of communication during his/her preaching/sermons. Before climbing on the pulpit all preachers should pay attention to creative sermon forms and styles, in order to be conducive to effective communication. This study deals with four main focus areas. Firstly, it is necessary to study different sermon forms and also to undertake a comparative analysis of the historical development of sermon forms in the South Korean Churches (SKC) and in US churches. In South Korea the sermon form has a more traditional feature, which is still present up till today in the local SKCs. Secondly, the preacher should be able to construct as well as use two different approaches in order to promote the most effective and communicative sermon: (1) induction, deduction and interduction, (2) analysis of the hearers within their present context. Thirdly, in this thesis five sermon forms have been discussed: (1) topical form, (2) textual sermon form, (3) expository sermon form, (4) narrative sermon form, (5) homily sermon form. Having discussed these forms, the aim was then to find a more useful and suitable sermon form. The choice was eventually made in favour of the multi-sermon form: multi-topical, multi-textual, multi-expository, multi-narrative and multi-homily sermon form. Fourthly, the preacher must be acquainted with the characteristics of the current worship patterns of the hearers attending the service: (1) dawn worship, (2) Wednesday evening worship, (3) Friday evening worship, (4) Sunday morning worship, (5) Sunday evening worship. / Thesis (PhD (Practical Theology))--University of Pretoria, 2006. / Practical Theology / unrestricted

Act no. 235/2004 Coll., Value Added Tax (hereinafter "the VAT Act"), is for non-profit organizations very difficult area, because of its frequent amendment. Also its meaning and content is for many of these organizations difficult to understand. This thesis wants to provide non-profit organizations comprehensive overview of the issue of value added tax. In addition to the application of special provisions of the VAT Act this thesis also focuses on provisions which relate generally to all taxpayers. The aim is the elimination of errors, in which non-profit organizations make mistakes. The most problematic provisions in practice are those which bind to the registration or vice versa deregistration. Problematic provisions are also those which relate to the right to deduct VAT on received taxable supplies. The practical part of this thesis is dedicated to these provisions.

Trots en rättsutveckling som pågått sedan början av 2000-talet råder fortfarande viss oklarhet rörande möjligheterna att enligt unionsrätten pröva en nationell lagstiftning mot den fria rörligheten för kapital. För tillämpningen av ändamålstestet saknas tydliga riktlinjer både vad gäller definitionen av begreppet definitivt inflytande och betydelsen av lagstiftarens vilja med den ifrågavarande nationella lagstiftningen. Min tolkning, som alltså i huvudsak bygger på rättsfallen Lasertec och Itelcar, är att begreppet definitivt inflytande inte kan knytas till en exakt procent av ägandet i ett annat bolag. Genom en jämförelse av flera avgöranden från EU-domstolen tycks dock slutsatsen kunna dras att ett definitivt utövande typiskt sett följer av en ägarandel om 25 %. Samtidigt ger ordalydelsen i domstolens resonemang i till exempel Itelcar vid handen att ett innehav om ner till 10 % kan ge ett definitivt inflytande i kombination med andra faktorer, men inte i sig. Det är heller inte omöjligt att detsamma gäller ännu mindre innehav. I och med att definitivt inflytande kan utövas vid mindre innehav än 25 % måste det också vara möjligt för nationella lagstiftningar att tillämpas på sådana innehav utan att för den sakens skull kunna angripas med den fria rörligheten för kapital.  Det sagda innebär att en lagstiftning, likt den i Lasertec, som är tillämplig på ägarandelar om 25 %, eller mindre andelar men där ett sådant inflytande som generellt följer av en sådan ägarandel likväl kan utövas, ska anses ha som ändamål att tillämpas på situationer där definitivt inflytande föreligger och ska därför inte prövas mot den fria rörligheten för kapital. Att tillämpningen av lagstiftningen utgår från en ägarandel om 25 % visar att lagstiftaren haft som avsikt att lagstiftningen ska tillämpas i situationer där ett sådant inflytande som motsvarar det som typiskt sett följer av en sådan ägarandel kan utövas. En lagstiftning likt den i Itelcar, som i stället som utgångspunkt för tillämpning förutsätter ett innehav om 10 % kan dock inte sägas ha som ändamål att endast tillämpas på ägarandelar som ger ett definitivt inflytande. Det inflytande som typiskt sett kan utövas vid ägarandelar om 10 % kan nämligen inte anses vara definitivt. De svenska ränteavdragsbegränsningsreglerna kräver för sin tillämpning att åtminstone ett väsentligt inflytande kan utövas över det räntebetalande företaget. Vad ett väsentligt inflytande närmare innebär är inte helt entydigt, men tycks avse ägarandelar om minst 40 %. Det är dock tydligt att även andra omständigheter än storleken på ägandet kan beaktas. Vid innehav under 40 % måste således ett väsentligt inflytande kunna påvisas på annan grund för att lagstiftningen ska vara tillämplig. Mot bakgrund av det ovan sagda är min slutsats att de svenska ränteavdragsbegränsningsreglerna inte kan prövas mot den fria rörligheten för kapital. Då förarbetsuttalanden antyder att det inflytande som ska kunna utövas ska motsvara en ägarandel om 40 %, måste ändamålet med lagstiftningen anses vara att den endast ska tillämpas i situationer där ett definitivt inflytande föreligger. Att lagstiftningen även kan komma att tillämpas vid mindre innehav ändrar inte denna bedömning, då detta har godkänts av EU-domstolen i Lasertec. Jag har visserligen dragit en annan slutsats än Ohlsson rörande tillämpligheten av den fria rörligheten för kapital på de svenska ränteavdragsbegränsningsreglerna, men jag delar hans uppfattning att en svensk domstol bör inhämta ett förhandsavgörande från EU-domstolen för att få frågan avgjord. Det skulle dessutom ge EU-domstolen en möjlighet att ytterligare förtydliga tillämpningen av ändamålstestet i tredjelandssituationer.

No description available.

[pt] A lógica descritiva intuicionista iALC foi criada para modelar e raciocinar sobre o domínio de Leis baseada na Jurisprudência Kelseniana [1]. No decorrer da década anterior, essa lógica foi usada de diversas maneiras para modelar normas ou formalizar raciocínio jurídico [2, 3, 4, 5, 6, 7, 8, 9, 10]. Neste trabalho pretendemos complementar trabalhos anteriores ralizados com essa lógica ao preencher algumas lacunas encontradas enquanto trabalhando com ela. A primeira lacuna ocorre por iALC não ter um modo intuitivo de explicar raciocínio nela realizado para pessoas fora do domínio da Lógica. Ela tem um Cálculo de Sequentes (CS) [6] correto e completo (com respeito a modelos conceituais intuitionistas [3]) que tem sido menos usado que o desejado, e isso se dá em grande parte devido à maneira pouco intuitiva com que CS representa provas. Apresentamos um sistema de Dedução Natural (DN) correto e completo e com (quasi-)normalização para compensar por essa dificuldade em explicar CS para não-lógicos, especialmente os do domínio legal, essenciais para nossa pesquisa. Normalização completa não é possível devido a um tipo de derivação - tirando essa exceção, o resto do sistema gera derivações uniformes. A segunda lacuna envolve não poder lidar com raciocínio não-monotônico (RNM). Em geral, utiliza-se raciocínio monotônico, no qual, se é possível concluir algo de um conjunto de premissas, não há como acrescentar outra premissa de modo a evitar a conclusão prévia. Isso não é o caso em um julgamento legal, por exemplo, no qual lados opostos buscam convencer um juiz ou júri de consequências opostas ao adicionar premissas diferentes ao caso em questão. Propomos uma investigação de caráter exploratório em busca de uma extensão de iALC para lidar com RNM a fim de representar raciocínio jurídico em outras facetas da Lei como o processo judicial, que é não-monotônico por natureza. Apresentamos propriedades desejadas e uma possível aplicação de um sistema assim via um estudo de caso. Detalhamos mais a motivação tanto para o sistema de DN quanto a extensão de RNM, assim como as decisões tomadas ao criar cada um. / [en] The intuitionistic description logic iALC was created to model and reason over the domain of Law based on Kelsenian Jurisprudence [1]. Over the past decade, this logic has been used in several ways to either model norms or formalise legal reasoning [2, 3, 4, 5, 6, 7, 8, 9, 10]. In this work we intend to complement previous research done with this logic by filling some gaps found while working with it. The first gap occurs in iALC needing an intuitive way to explain reasoning for non-logicians. It has a sound and complete (concerning intuitionistic conceptual models [3]) Sequent Calculus (SC) [6] that has seen less usage than expected due to its non-intuitive way of presenting a proof. We present a (quasi-)normalising, sound and complete (w.r.t. TBox validity for intuitionistic conceptual models) Natural Deduction (ND) System to cover this difficulty in explaining SC to non-logicians, especially those in the domain of Law, which are essential to us. We do not achieve full normalisation due to a kind of derivation which cannot be normalised - aside from this exception, the rest of the system can provide uniform derivations. The second gap is being unable to deal with non-monotonic reasoning (NMR). Usually, one considers monotonic reasoning, in which, if one can conclude something from a set of premises, there is no way to add another premise to avoid said conclusion. This is not the case in a court of law, for instance, in which different parties aim to convince a judge or jury of opposite consequences by adding different premises to the case itself. We provide an exploratory investigation of an extension of iALC to deal with NMR to represent legal reasoning in aspects of the Law, such as the judicial process, which is non-monotonic by nature. We present desirable properties and a possible application of such a system via a case study. We explain further the motivation for both the ND system and the NMR extension and the decisions taken for both.