The relationship between quantity traded and transaction costs has been one of the main focuses among financial scholars and practitioners. The purpose of this thesis is to investigate the informational relationship between these variables. Following insights and results of Milgrom (1981), Feldman (2004), and Feldman and Winer (2004), we use New York Stock Exchange (NYSE) data and kernel estimation methods to construct the distribution of one variable conditional on the other. We then study the information in these conditional distributions: the extent to which they are ordered by first order stochastic dominance (FOSD) and by monotone likelihood ratio property (MLRP). We find that transaction size and effective spread are statistically significantly orrelated. FOSD, a necessary condition for a "separating signaling equilibrium", holds under certain conditions. We start from two-subsample case. We choose a cut-off point in transaction size and categorize the observations with transaction sizes smaller than the cut-off point into group "low". The remaining data is classified as "high". We repeat this procedure for all possible transaction size cut-off points. It turns out that FOSD holds nowhere. However, once we eliminate transactions at the quote midpoint, the "crossings" between exchange members not specialists, FOSD holds for all the cut-off points fewer than 15800 shares. MLRP, a necessary and sufficient condition for the separating equilibrium to hold point by point of the conditional density functions, does not hold but might not be ruled out considering the error in the estimates. We also find that large trades are not necessarily associated with large spread. Instead, it is more likely that larger trades are transacted at the quote midpoint (again, the non-specialist "crossings") than smaller trades. Our results confirm the findings of Barclay and Warner (1993) regarding the informativeness of medium-size transactions: we identify informational relationships between mid-size transactions and spreads but not for trades at the quote midpoint and large-size transactions. That is, we identify two regimes, an informational one and a non-informational/liquidity one.

Ce mémoire présente le résultat de mon travail de thèse sur la génération d'impliqués premiers en logique équationnelle fermée, i.e., la génération des conséquences les plus générales de formules logiques contenants des équations et des disequations entre termes sans variables. Ce mémoire est divisé en trois parties. Tout d'abord, deux calculs de génération d'impliqués sont définis. Leur complétude pour la déduction est prouvée, ce qui signifie qu'ils sont tous deux capables de générer l'ensemble des impliqués modulo redondance d'une formule équationnelle fermée. Dans une deuxième partie, une structure de données arborescente est proposée pour stocker les impliqués générés, accompagnée d'algorithmes pour déceler les redondances et couper les branches de l'arbre lorsque c'est nécessaire. Cette structure de données est adaptée aux différents types de clauses (avec et sans symboles de fonctions, avec et sans contraintes) ainsi qu'aux différentes notions de redondance utilisées dans les calculs. En effet, chaque calcul utilise un critère de redondance légèrement différent des autres. Les preuves de correction et de terminaison des algorithmes sont fournies pour chaque algorithme. Enfin, une évaluation expérimentale des différentes méthodes de génération d'impliqués premiers est réalisée. Pour cela, un prototype de ces méthodes, écrit en Ocaml est comparé à des outils de génération d'impliqués premiers récents.Les résultats de ces expériences sont utilisés pour identifier les variantes les plus efficaces des algorithmes proposés. Les résultats sont prometteurs et dans la plupart des cas, meilleurs que ceux de l'état de l'art. / The work presented in this memoir deals with the generation of prime implicates in ground equational logic, i.e., of the most general consequences of formulae containing equations and disequations between ground terms.It is divided in three parts. First, two calculi that generate implicates are defined. Their deductive-completeness is proved, meaning they can both generate all the implicates up to redundancy of equational formulae.Second, a tree data structure to store the generated implicates is proposed along with algorithms to detect redundancies and prune the branches of the tree accordingly. This data structure is adapted to the different kinds of clauses (with and without function symbols, with and without constraints) and to the various formal definitions of redundancy used in the calculi since each calculus uses different -- although similar -- redundancy criteria. Termination and correction proofs are provided with each algorithm. Finally, an experimental evaluation of the different prime implicate generation methods based on research prototypes written in Ocaml is conducted including a comparison with state-of-the-art prime implicate generation tools. This experimental study is used to identify the most efficient variants of the proposed algorithms. These show promising results overstepping the state of the art.

abstract: Natural Language Processing is a subject that combines computer science and linguistics, aiming to provide computers with the ability to understand natural language and to develop a more intuitive human-computer interaction. The research community has developed ways to translate natural language to mathematical formalisms. It has not yet been shown, however, how to automatically translate different kinds of knowledge in English to distinct formal languages. Most of the recent work presents the problem that the translation method aims to a specific formal language or is hard to generalize. In this research, I take a first step to overcome this difficulty and present two algorithms which take as input two lambda-calculus expressions G and H and compute a lambda-calculus expression F. The expression F returned by the first algorithm satisfies F@G=H and, in the case of the second algorithm, we obtain G@F=H. The lambda expressions represent the meanings of words and sentences. For each formal language that one desires to use with the algorithms, the language must be defined in terms of lambda calculus. Also, some additional concepts must be included. After doing this, given a sentence, its representation and knowing the representation of several words in the sentence, the algorithms can be used to obtain the representation of the other words in that sentence. In this work, I define two languages and show examples of their use with the algorithms. The algorithms are illustrated along with soundness and completeness proofs, the latter with respect to typed lambda-calculus formulas up to the second order. These algorithms are a core part of a natural language semantics system that translates sentences from English to formulas in different formal languages. / Dissertation/Thesis / M.S. Computer Science 2010

Some climate models are still lacking features such as dynamical modelling of ice sheets due to their computational cost which results in poor accuracy and estimates of e.g. sea level rise. The need for low-cost high-order models initiated the development of the First-Order Stokes (or Blatter-Pattyn) model which retains much of the accuracy of the full-Stokes model but is also cost-effective. This model has proven accurate for ice sheets and glaciers with frozen bedrocks, or no-slip basal boundary conditions. However, experimental evidence seems to be lacking regarding its accuracy under sliding, or stress-free, bedrock conditions (ice-shelf conditions). Hence, it became of interest to investigate this. Numerical experiments were set up by formulating the first-order Stokes equations as a variational finite element problem, followed by implementing them using the open-source FEniCS framework. Two types of geometries were used with both no-slip and slip basal boundary conditions. Specifically, experiments B and D from the Ice Sheet Model Intercomparison Project for Higher-Order ice sheet Models (ISMIP-HOM) were used to benchmark the model. Local model errors were investigated and a convergence analysis was performed for both experiments. The results yielded an inherent model error of about 0.06% for ISMIP-HOM B and 0.006% for ISMIPHOM D, mostly relating to the different types of geometries used. Errors in stress-free regions were greater and varied on the order of 1%. This was deemed fairly accurate, and probably enough justification to replace models such as the Shallow Shelf Approximation with the First-Order Stokes model in some regions. However, more rigorous tests with real-world geometries may be warranted. Also noteworthy were inconsistent results in the vertical velocity under slippery conditions (ISMIPHOM D) which could either be due to coding errors or an inherent problem with the decoupling of the horizontal and vertical velocities of the First-Order Stokes model. This should be further investigated. / Vissa klimatmodeller saknar fortfarande funktioner så som dynamisk modellering av istäcken på grund av dess höga beräkningskostnad, vilket resulterar låg noggrannhet och uppskattningar av t.ex. havsnivåhöjning. Behovet av enkla modeller med hög noggrannhet satte igång utvecklingen av den s.k. Första Ordningens Stokes (eller Blatter-Pattyn) modellen. Denna modell behåller mycket av noggrannheten i den mer exakta full-Stokes-modellen men är också väldigt kostnadseffektiv. Denna modell har visat sig vara noggrann för istäcken och glaciärer med frusna berggrunder eller s.k. no-slip randvillkor. Experimentella bevis tycks dock saknas med avseende på dess noggrannhet under glidning, eller stressfria, berggrundsförhållanden (t.ex. vid ishyllor). Därför ville vi undersöka detta. Numeriska experiment upprättades genom att formulera Blatter-Pattyn ekvatonerna som ett variationsproblem (via finita elementmetoden), följt av att implementera dem med hjälp av den öppna källkoden FEniCS. Två typer av geometrier användes med både glidande och stressfria basala randvillkor. Specifikt användes experiment B och D från Ice Sheet Model Intercomparison Project for Higher-Order ice sheet Models (ISMIP-HOM) för att testa modellen. Lokala fel undersöktes och en konvergensanalys utfördes för båda experimenten. Resultaten gav ett modellfel på ca 0,06 % för ISMIP-HOM B och 0,006 % för ISMIP-HOM D, vilka var mest relaterade till de olika typerna av geometrier som användes. Fel i stressfria regioner var större och varierade i storleksordningen 1 %. Detta ansågs vara ganska noggrant och sannolikt tillräckligt för att ersätta modeller så som Shallow Shelf Approximationen med Blatter-Pattyn-modellen i vissa regioner. Dock krävs mer noggranna tester med mer verkliga geometrier för att dra konkreta slutsatser. Också anmärkningsvärt var motsägande resultat i den vertikala hastigheten under glidande förhållanden (ISMIP-HOM D) som antingen kan ha berott på kodningsfel eller ett modelproblem som härstammar utifrån särkopplingen mellan den horizontella- och den vertikala hastigheten i Blatter-Pattyn-modellen. Detta bör undersökas vidare.

Constructed Wetlands are used in many parts of the world for the treatment of wastewater from diverse sources. They are effective, low cost and sustainable alternative to most conventional wastewater treatment processes. They are engineered to mimic many of the same processes that occur in natural wetlands but within a more controlled environment. The need for proper design of constructed wetlands for secondary and tertiary wastewater treatment is of utmost importance in meeting today's stringent water quality standards. Subsequently, numerous design tools have been proposed for the assessment of constructed wetland performance. Currently, applied modeling approaches include regression models, mass loading versus outflow concentration analysis, Monod type analytical models and first-order removal kinetic models. The principal objective of this research was to estimate the biochemical oxygen demand (BOD) removal using both the plug flow and complete-mix first order kinetic models. Results obtained by these models were then validated by comparing with published data from the Arcata constructed wetland. This study also investigated the sensitivity of effluent BOD quality to variation in influent concentration, temperature and hydraulic retention time. Analysis of the results revealed that variations in the field conditions influenced the removal rate of BOD in each zone of the wetland. The design reaction rate coefficient for each zone varied and was corrected for using the Arrhenius expression. The BOD removal performance of the Arcata wetland and any wetland operated under similar conditions was found to be better modeled by the plug flow model at zero background concentration. The study also found the BOD removal to be much influenced by the influent concentration and minimally influenced by temperature and hydraulic retention time.

The modal logic S5 gives us a simple technical tool to analyze some main notions from philosophy (e.g. metaphysical necessity and epistemological concepts such as knowledge and belief). Although S5 can be axiomatized by some simple rules, this logic shows some puzzling properties. For example, an interpolation result holds for the propositional version, but this same result fails when we add first-order quantifiers to this logic. In this dissertation, we study the failure of the Definability and Interpolation Theorems for first-order S5. At the same time, we combine the results of justification logic and we investigate the quantified justification counterpart of S5 (first-order JT45). In this way we explore the relationship between justification logic and modal logic to see if justification logic can contribute to the literature concerning the restoration of the Interpolation Theorem. / A lógica modal S5 nos oferece um ferramental técnico para analizar algumas noções filosóficas centrais (por exemplo, necessidade metafísica e certos conceitos epistemológicos como conhecimento e crença). Apesar de ser axiomatizada por princípios simples, esta lógica apresenta algumas propriedades peculiares. Uma das mais notórias é a seguinte: podemos provar o Teorema da Interpolação para a versão proposicional, mas esse mesmo teorema não pode ser provado quando adicionamos quantificadores de primeira ordem a essa lógica. Nesta dissertação vamos estudar a falha dos Teoremas da Definibilidade e da Interpolação para a versão quantificada de S5. Ao mesmo tempo, vamos combinar os resultados da lógica da justificação e investigar a contraparte da versão quantificada de S5 na lógica da justificação (a lógica chamada JT45 de primeira ordem). Desse modo, vamos explorar a relação entre lógica modal e lógica da justificação para ver se a lógica da justificação pode contribuir para a restauração do Teorema da Interpolação.

Orientador: Walter Carnielli / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas / Made available in DSpace on 2018-08-12T05:55:31Z (GMT). No. of bitstreams: 1 Podiacki_Rodrigo_M.pdf: 538726 bytes, checksum: 3a51529177d89ce92122bde746a321c3 (MD5) Previous issue date: 2008 / Resumo: Esta dissertação tem como objetivo desenvolver uma semântica correta e completa para uma classe de lógicas de primeira ordem conhecidas como Lógicas da Inconsistência Formal (LIFs). Após uma elucidação geral sobre semânticas paraconsistentes e de primeira ordem, uma LIF particular, chamada QmbC, será caracterizada axiomaticamente. Em seguida será construída uma semÂntica que se demonstrará correta e completa para a LIF em questão. Por fim, uma série de LIFs com propriedades sintáticas interessantes serão caracterizadas axiomaticamente, e será visto como a semântica construída para QmbC pode ser estendida para todas essas lógicas. / Abstract: This dissertation aims to develop a sound and complete semantics for a class of first-order logics known as Logics of Formal Inconsistency (LFIs). After general explanation about paraconsistent and first-order semantics, a particular LFI, labeled QmbC, will be characterized by means of an axiom system. Then a sound and complete semantics for it will be constructed. Finally, a variety of LFIs having nice syntactic properties will be axiomatically defined, and it will be shown how the semantics proposed for QmbC can be extended for all these logics. / Mestrado / Filosofia / Mestre em Filosofia

Orientador: Kleber Roberto Pirota / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Física Gleb Wataghin / Made available in DSpace on 2018-08-19T11:29:30Z (GMT). No. of bitstreams: 1 CostaArzuza_LuisCarlos_M.pdf: 3383467 bytes, checksum: 8fac04d42ba77c741416d15d643d402a (MD5) Previous issue date: 2011 / Resumo: Este trabalho visa estudar o comportamento histerético, observado a baixos campos magnéticos, do fenômeno da magnetoimpedância gigante (GMI) em fitas amorfas a base de CoFeSiB com anisotropia magnética transversal. O fenômeno da GMI consiste na variação da impedância elétrica (aproximadamente do 100%) de uma amostra magnética mole quando submetida à aplicação de campo magnético DC externo. Apesar da importância da presença de histerese na GMI, tanto do ponto de vista básico quanto do tecnológico, existem poucos estudos na literatura que visam à explicação da origem desse efeito. Desde o ponto de vista fundamental, o completo entendimento do fenômeno poderia revelar importantes aspectos envolvidos com o processo de magnetização nos materiais considerados. De um ponto de vista prático, a presença da histerese na GMI tanto pode ser desfavorável, quando pensamos na fabricação de sensores, quanto favorável, se levamos em consideração a sua possível aplicação em sistemas de memória magnética. Por outro lado, o método denominado curva de inversão da primeira ordem (first-order reversal curve, FORC, em inglês) mostra-se uma poderosa ferramenta para o estudo e compreensão de fenômenos histeréticos, principalmente da histerese magnética presente em curvas de magnetização de materiais ferromagnéticos. Tal método, fundamentado no modelo clássico de Preisach, dá importantes informações através de medidas de ciclos de histerese secundarias da curva principal. Neste trabalho utilizamos a técnica FORC para estudar o fenômeno da histerese na GMI. Utilizamos fitas amorfas de composição (CoxFe1-x)70Si12B18, com x = 0,040 e 0,045 como sistema de estudo devido a suas propriedades magnéticas moles. Tais fitas possuem 22 µm de espessura, 0,8 mm de largura e constante de anisotropia de 139 J/m3 e 145 J/m3 respetivamente. As medidas de GMI foram realizadas com um analisador de rede vetorial (vector network analizer, VNA, em inglês). Tal equipamento, combinado a um sistema de bobina e fonte de corrente, permitiu-nos fazer medidas de impedância em função da frequência (entre 10 MHz e 1 GHz) e do campo magnético aplicado (até 100 Oe). Consideramos como principal resultado deste trabalho o desenvolvimento de um método eficiente para testar e aprimorar modelos teóricos sobre a origem de tal histerese. Os resultados obtidos do comportamento histeretico no volume e na superficie, foram interpretados levando-se em conta uma estrutura magnética estática volumétrica não uniforme e ao amortecimento das paredes de domínio / Abstract: We studied the hysteretic behavior, observed at low magnetic fields, of the giant magnetoimpedance (GMI) phenomenon in CoFeSiB amorphous ribbons with transversal magnetic anisotropy. The GMI phenomenon consists in the electrical impedance variation (around 100 %) of a soft magnetic sample in the presence of an external DC magnetic field.Despite the importance of hysteresis presence in GMI from technological and basic points of view, it exists only few studies about the description of this effect. From the fundamental outlook, the complete understanding of the phenomenon could reveal important aspects involved in the magnetization process of the concerned materials. For practical applications, the hysteretic GMI can be unfavorable (for example for sensor development) or favorable (for example for magnetic storage memories). On the other side, first-order reversal curve (FORC) method is a powerful tool for the study and understanding of hysteretic phenomena, mainly for the hysteresis present in the magnetization curves of ferromagnetic materials. This method, based on the classical Preisach model, allows to extract important information through minor hysteresis loops inside the major one. In this work, we used the FORC technique to study the GMI hysteretic phenomenon. We investigated amorphous ribbons of (CoxFe1-x)70Si12B18 composition, where x = 0.040 and 0.045. Those ribbons were 2 µm thick and 0.8 mm wide. The GMI measurements were performed with a vector network analyzer (VNA). This equipment, coupled with a system of coil and power supply, allowed impedance measurements versus frequency (between 10 MHz and 1 GHz) and applied magnetic field (until 100 Oe). We consider that the main achievement of this work is the development of an efficient method allowing to test and improve theoretical models about the hysteresis origin. The obtained results were interpreted taking into account a non homogeneous static magnetic structure along the ribbon volume with domain walls damping / Mestrado / Física / Mestre em Física

Orientadores: Marcelo Knobel, Kleber Roberto Pirota / Tese (doutorado) - Universidade Estadual de Campinas, Instituto de Física Gleb Wataghin / Made available in DSpace on 2018-08-19T10:38:36Z (GMT). No. of bitstreams: 1 ValenzuelaAcuna_LeninaAlejandra_D.pdf: 6580739 bytes, checksum: f221d85ff3a59859f824164188637f28 (MD5) Previous issue date: 2011 / Resumo: No nosso trabalho utilizamos o fenômeno da magnetoimpedância gigante (GMI) como uma ferramenta de pesquisa na caracterização de ferromagnetos amorfos. Estes materiais são muito moles do ponto de vista magnético, o que pode servir para diversas aplicações, tais como na construção de sensores e de dispositivos de alta frequencia. Na primeira parte da tese veremos como a GMI se torna uma técnica complementar na caracterização da cristalização em materiais amorfos. Na segunda parte da tese estudamos uma fita que apresenta histerese na GMI, de modo inédito utiliza-se o método de First Order Reversal Curves (FORC), em medidas da impedância. Os resultados apresentam um comportamento complexo, para os quais estamos propondo uma interpretação particular. Os materiais que mostram este comportamento podem ser úteis nas aplicações de, por exemplo, armazenamento de informação. Inicialmente, realizamos tratamento térmico convencional e por aquecimento Joule em fitas amorfas de composição Fe86Zr7Cu1B6 fabricadas pelo método melt spinning. Quando tratadas termicamente ocorre a cristalização de partículas a-Fe, e no geral o tamanho das partículas aumenta com o aumento da magnitude do tratamento (temperatura ou corrente). Nas medidas de magnetização vemos geralmente que a coercividade apresenta baixos valores e há um endurecimento nas amostras onde se observou um aumento no tamanho dos grãos no início da cristalização. Por outro lado, a fração cristalina nas amostras tem uma tendência ao aumento com o tratamento térmico, que se reflete nas medidas de raios X e da magnetização de saturação Ms. Vimos também que as medidas de GMI em função da frequência, apresentam resultados atípicos: diferente da relação com a raiz quadrada da frequência, a GMI máxima apresenta curvas que indicam uma diminuição da resposta GMI para frequências altas. Isto foi interpretado como sendo devido à não-homogeneidade da formação dos cristais no volume das amostras. Consideramos a relação inversa do coeficiente de penetração dm com a frequência. Vemos que com o aumento da frequência diminui a região onde circula a corrente ac a qual está mais próxima à superfície, onde há partículas maiores o que deixa o material magneticamente mais duro. Na segunda parte do trabalho apresentamos uma aplicação inovadora da união da técnica de caracterização FORC com medidas de GMI. Utilizamos fitas amorfas, de composição (FexCo1-x)70Si12B18 (x = 0,045; 0,048; 0,049; 0,050) que foram fabricadas pelo método melt spinning. Nestas induziu-se anisotropia transversal por meio de tratamentos térmicos junto à aplicação de tensão. A resposta GMI apresentou um comportamento histerético, o eu nos levou a querer usar a técnica FORC para entender a causa deste. A forma de interpretação das curvas e diagramas FORC apresentou um novo desafio. Sabemos que a variação da impedância é ocasionada pela variação da permeabilidade transversal na amostra. Foi proposta a hipótese de que o processo histerético se deve a uma transformação no tipo de paredes de domínio com o campo, de modo que cada tipo de parede tem uma µt associada. Observou-se também a dependência da distribuição FORC com a frequência, anisotropia, e relativa à componente da impedância (parte real ou imaginária) / Abstract: In this work, we used the giant magnetoimpedance (GMI) effect as a research tool to characterize ferromagnetic amorphous materials. These materials have ultra-soft magnetic features, which can be useful for various applications, e.g. sensors and high frequency devices. In the first part, we will see how GMI becomes a complementary technique to characterize the crystallization in amorphous materials. In the second place, we studied a ribbon that shows hysteresis in the GMI response. The First Order Reversal Curves (FORC) method was applied in impedance measurements as a novel technique. We are proposing a particular interpretation for the complex obtained results. The applications of these materials with hysteretic behavior can be useful to magnetic recording, for example. In the first part of the work, we induced the crystallizations of a-Fe particles in amorphous ribbons of composition Fe86Zr7Cu1B6 manufactured by melt spinning method, by thermal treatment (conventional and Joule heating). In general, the size of particles increases with the temperature or current of treatment. In magnetization measurements the coercivity has usually low values. There is a hardening in samples with bigger size grains, at the beginning of crystallization. On the other hand, the crystalline fraction in the samples has a tendency to increase with thermal treatment, which is reflected in measurements of X-rays and the saturation magnetization Ms. We have also seen that the GMI measurements as a function of frequency show rather atypical results: the maximum GMI as a function of frequency shows a decrease in the GMI response to high frequencies, that differ from the relationship with the square root of frequency. This was interpreted as being due to non-homogeneity of the formation of crystals in the volume of samples. If we consider the inverse relationship of penetration coefficient with frequency dm, we can see that with the increase of frequency decreases the region where the ac current flows, which, in turn, is closer to the surface. In this region there are larger particles, making the material magnetically harder. In the second part of the work, we present an innovative application of the junction of characterization technique FORC with measurements of GMI. We use amorphous ribbons of composition (FexCo1-x)70Si12B18 (x = 0,045; 0,048; 0,049; 0,050)produced by melt spinning. A transverse anisotropy was induced by thermal treatments with the application of stress. We applied the FORC technique in order to help to understand the hysteretic behavior in the GMI response. The interpretation of the GMI curves and FORC diagrams is a new challenge. We know that the variation of impedance is caused by the change of transverse permeability sample µ t. We proposed the hypothesis that the hysteretic process is due to a change in the type of domain walls with the field, so that each type of wall has an associated µt. We also observed the dependence of the FORC distribution with frequency, anisotropy, and with the components of the impedance (real or imaginary part) / Doutorado / Doutora em Ciências

The purpose of this master thesis was to investigate which of the two methods, resolution and tableaux, that is the most appropriate for automated theorem proving. This was done by implementing an automated theorem prover, comparing and documenting implementation problems, and measuring proving efficiency. In this thesis, I conclude that the resolution method might be more suitable for an automated theorem prover than tableaux, in the aspect of ease of implementation. Regarding the efficiency, the test results indicate that resolution is the better choice. / Syftet med detta magisterarbete var att undersöka vilken av de två metoderna, resolution och tablå, som är mest lämpad för automatisk teorembevisning. Detta gjordes genom att implementera en automatisk teorembevisare, jämföra och dokumentera problem, samt att mäta prestanda för bevisning. I detta arbete drar jag slutsatsen att resolutionsmetoden förmodligen är mer lämpad än tablåmetoden för en automatisk teorembevisare, med avseende på hur svår den är att implementera. När det gäller prestanda indikerar utförda tester att resolutionsmetoden är det bästa valet.