ONTIC: A Knowledge Representation System for Mathematics

Ontic is an interactive system for developing and verifying mathematics. Ontic's verification mechanism is capable of automatically finding and applying information from a library containing hundreds of mathematical facts. Starting with only the axioms of Zermelo-Fraenkel set theory, the Ontic system has been used to build a data base of definitions and lemmas leading to a proof of the Stone representation theorem for Boolean lattices. The Ontic system has been used to explore issues in knowledge representation, automated deduction, and the automatic use of large data bases.

Procedures as a Representation for Data in a Computer Program for Understanding Natural Language

This paper describes a system for the computer understanding of English. The system answers questions, executes commands, and accepts information in normal English dialog. It uses semantic information and context to understand discourse and to disambiguate sentences. It combines a complete syntactic analysis of each sentence with a "heuristic understander" which uses different kinds of information about a sentence, other parts of the discourse, and general information about the world in deciding what the sentence means. It is based on the belief that a computer cannot deal reasonably with language unless it can "understand" the subject it is discussing. The program is given a detailed model of the knowledge needed by a simple robot having only a hand and an eye. We can give it instructions to manipulate toy objects, interrogate it about the scene, and give it information it will use in deduction. In addition to knowing the properties of toy objects, the program has a simple model of its own mentality. It can remember and discuss its plans and actions as well as carry them out. It enters into a dialog with a person, responding to English sentences with actions and English replies, and asking for clarification when its heuristic programs cannot understand a sentence through use of context and physical knowledge.

Un análisis de la relación comercial entre Colombia y Estados Unidos en el marco de los acuerdos comerciales

Estados Unidos es el principal socio comercial de Colombia: es el país de destino del 36% de las exportaciones colombianas y el país de origen del 25% de las importaciones colombianas (DANE, 2011). La relación entre ambos profundizó sus lazos con el programa arancelario ATPA, luego ATPDEA, en virtud del cual al 80% de la oferta exportable de Colombia se le ofrecía ya sea con libre acceso al mercado estadounidense, o entrada con pago de arancel reducido. Posteriormente, la entrada en vigencia del TLC generó las bases para una relación comercial más profunda aún, que también incluyera beneficios para Estados Unidos y prolongara y profundizara los beneficios que Colombia ya recibía. Este trabajo se enfoca en analizar paso a paso el comportamiento del comercio entre ambos países a través de los años y, por supuesto, el comportamiento actual del comercio, teniendo siempre en cuenta el contexto económico mundial, así como el contexto económico bilateral.

Durability assessment of PbTe/II-IV infrared filters (Space Shuttle 1st LDEF)

Residual stress having been further reduced, selected infrared coatings composed of thin films of (PbTe/ ZnS (or ZnSe) can now be made which comply with the durability requirements of MIL-48616 whilst retaining transparency. Such improved durability is due to the sequence:- i) controlled deposition, followed by ii) immediate exposure to air, followed by iii) annealing in vacuo to relieve stress. (At the time of writing we assume the empiric procedure "exposure to air/annealing in vacuo" acts to relieve the inherent stresses of deposition). As part of their testing, representative sample filters prepared by the procedure are being assembled for the shuttle's 1st Long Duration Exposure Facility (to be placed in earth orbit for a considerable period and then recovered for analysis). The sample filters comprise various narrowband-designs to permit deduction of the constituent thin film optical properties. The Reading assembly also contains representative sample of the infrared crystals, glasses, thin-film absorbers and bulk absorbers, and samples of shorter-wavelength filters prepared similarly but made with Ge/SiO. Findings on durability and transparency after exposure will be reported.

Monodic Temporal Resolution

First-order temporal logic is a coincise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness result, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

Kanger's Choices in Automated Reasoning

This article explains these choices and their place in modern automated deduction.

Evidence Algorithm and Processing Formalized Mathematical Texts

The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

Análise econômica das políticas de incentivos à cultura no Brasil

O Brasil conta hoje com uma legislação que o coloca seguramente entre os melhores países, senão o melhor, para se realizar projetos culturais. Ao menos na teoria. Essa dissertação tem como objetivo trilhar o caminho das leis de incentivo, desde a sua criação, com a Lei Sarney até a Lei Rouanet, analisando inclusive as leis estaduais e municipais, que também surgiram como respostas a descontinuidades no processo. O mercado cultural brasileiro é caracterizado por externalidades que dificultam sua viabilidade, fazendo necessária a intervenção governamental. A política cultural brasileira tem como principal instrumento as leis de incentivo à cultura, que utilizam a renúncia fiscal para atrair o capital privado. São formalizadas parcerias onde as empresas privadas patrocinam projetos de interesse do governo e, como contrapartida, recebem o direito de deduzir esse valor, integral ou parcialmente, de seus impostos. Contudo, esse modelo de contrato de parceria é mal formulado, e traz perdas para a sociedade. O risco é assumido integralmente pelo Estado, o que acarreta problemas sérios de Moral Hazard. Além disso, devido às diferentes características dos projetos, o modelo acaba também por gerar problemas de Seleção Adversa. Para uma melhor comparação e análise da política cultural brasileira, foram levantados casos internacionais - Estados Unidos, Inglaterra, Portugal e Espanha. Levando-se em conta as análises e críticas levantadas, serão sugeridas alternativas para o modelo de contrato adotado pelo governo para incentivo à cultura, e formas alternativas de financiamento ao setor cultural, de forma a assegurar um melhor retorno para a sociedade sem deixar de cumprir o papel de fomentar o setor e corrigir as externalidades presentes.

Gestão democrática no serviço público: o caso FIOCRUZ

o objetivo deste trabalho é analisar o modelo de gestão implantado na Fundação Oswaldo Cruz - FIOCRUZ, procurando identificar os limites e possibilidades de um processo de gestão democrática no Serviço Público, e de outro, inventariar, criticamente, os modelos administrativos disponíveis que tenham a questão da gestão democrática como pressuposto organizacional. Norteou o trabalho a trajetória institucional da FIOCRUZ, notadamente o período da realização dos Congressos Internos (de 1988 a 1996). Para alcance do objetivo, foram analisados, a partir de fontes primárias e secundárias, os aspectos que abrem espaço para um processo de gestão democrática. Na realização do trabalho foram selecionadas como categorias analíticas: poder decisório, autonomia e controle social. Baseamo-nos, ainda, no método que privilegiou a descrição utilizando, porém, a dedução apoiada na análise qualitativa e quantitativa. A análise dos dados possibilitou concluir que os procedimentos participativos como o processo eletivo de escolha do presidente e dos diretores das Unidades da FIOCRUZ, a constituição dos órgãos colegiados de decisão e a realização dos Congressos Internos abriram espaços para a democratização da gestão, representando a materialização da vontade e do desejo de certos atores, e garantiram a unidade de ação em uma instituição pouco integrada. Algumas questões são ponto de partida para pesquisas futuras: como esse modelo participativo é implantado em cada Unidade da FIOCRUZ? Esse modelo corresponde ao desejo efetivo dos servidores? Em que medida o processo participativo de gestão contribuiu para o ganho de eficiência administrativa?

OpenWordNet-PT: an open brazilian wordnet for reasoning

Brazilian Portuguese needs a Wordnet that is open access, downloadable and changeable, so that it can be improved by the community interested in using it for knowledge representation and automated deduction. This kind of resource is also very valuable to linguists and computer scientists interested in extracting and representing knowledge obtained from texts. We discuss briefly the reasons for a Brazilian Portuguese Wordnet and the process we used to get a preliminary version of such a resource. Then we discuss possible steps to improving our preliminary version.

Fragmentos da construção histórica do pensamento neo-empirista

O presente trabalho procura identificar as idéias principais na construção histórica do pensamento neo-empirista a partir da visão mecânica do mundo e do método hipotético-dedutivo de Descartes. O método indutivo moderno é apresentado por Bacon e os empiristas ingleses colaboram na questão do pensamento “a posteriori”. No século XIX surge o positivismo que exclui a metafísica e considera a explicação dos fatos apenas como relações de sucessão e similidade. É nesse âmbito que se constroem as bases do método experimental moderno. No início do século XX, se desenvolve a ciência neoempirista cujas principais proposições são (1) a idéia da verificabilidade como forma de conferir a veracidade das teorias a partir da indução e das probabilidades e (2) o crescimento contínuo e acumulativo do conhecimento científico. Popper apresenta a impossibilidade de se obter grandes teorias oriundas da indução e sugere a substituição da indução pela dedução e da verificabilidade pela falseabilidade. Kuhn afirma que o conhecimento científico depende de paradigmas convencionais e Lakatos explica que a ciência não é uma sucessão temporal de períodos normais e revoluções, e sim sua justaposição.

Lévi-Strauss Mitológicas: Mito e música entre o largo e o prestíssimo

This study was elaborated based on our research of the work Mithologiques by the anthropologist Claude Lévi-Strauss (1908-2009), which affirms that languages, indigenous myths and music are related. He proposes that the understanding of myths occurs in a similar manner as with an orchestral score. In the course of his tetralogy we investigated the musical terms used in the analysis and in the division of the chapters, especially in the first volume of his work. Several compositional procedures and forms are named. Composers in pairs are categorized: Sebastian Bach for the code, Ludwig van Beethoven for the message, and Richard Wagner for the myths. In this deduction, we structured in parts: theme and variations, sonata and fugue with the aforementioned composers. Within the greatness of anthropological study, from among over 800 myths, we selected the first five of the indigenous tribe Bororo to discuss within the Theme and Variation segment. In the Sonata part there are two myths with the same theme: The wife of the jaguar which relates to the compositional structure, and four myths about The origin of women. Finally, in the segment related to the Fugue, we collected four myths that address The shortness of life. Honoring the many terms expressed in opposition, contrast, or symmetry under consideration in Levi-Strauss work, we entitled this thesis emphasizing the migration between the tempos Largo and Prestíssimo as these are oppositional presentations in music. Fifteen musical myths accompany the work supported by selected narratives. In light of this we questioned, we questioned: how are incest, murder and other events part of a society that elevates nature as an extension of life itself? And how did Lévi-Strauss think that anthropology harmonized with music? In the preparation of this study, philosophers like Peter Sloterdijk discuss the circular territory of Mythology

Os argumentos transcendentais: kant e o problema de hume

This work whose title is "The transcendental arguments: Kant Andy Hume's problem" has as its main objective to interpret Kant's answer to Hume's problem in the light of the conjunction of the causality and induction themes which is equivalent to skeptical- naturalist reading of the latter. In this sense, this initiative complements the previous treatment seen in our dissertation, where the same issue had been discussed from a merely skeptical reading that Kant got from Hume thought and was only examined causality. Among the specific objectives, we list the following: a) critical philosophy fulfills three basic functions, a founding, one negative and one would argue that the practical use of reason, here named as defensive b) the Kantian solution of Hume's problem in the first critisism would fulfill its founding and negative functions of critique of reason; c) the Kantian treatment of the theme of induction in other criticisms would will fulfill the defense function of critique of reason; d) that the evidence of Kant's answer to Hume's problem are more consistent when will be satisfied these three functions or moments of criticism. The basic structure of the work consists of three parts: the first the genesis of Hume's problem - our intention is to reconstruct Hume's problem, analyzing it from the perspective of two definitions of cause, where the dilution of the first definition in the second match the reduction of psychological knowledge to the probability of following the called naturalization of causal relations; whereas in the second - Legality and Causality - it is stated that when considering Hume in the skeptic-naturalist option, Kant is not entitled to respond by transcendental argument A􀁴B; A⊢B from the second Analogy, evidence that is rooted in the position of contemporary thinkers, such as Strawson and Allison; in third part - Purpose and Induction - admits that Kant responds to Hume on the level of regulative reason use, although the development of this test exceeds the limits of the founding function of criticism. And this is articulated in both the Introduction and Concluding Remarks by meeting the defensive [and negative] function of criticism. In this context, based on the use of so-called transcendental arguments that project throughout the critical trilogy, we provide solution to a recurring issue that recurs at several points in our submission and concerning to the "existence and / or the necessity of empirical causal laws. In this light, our thesis is that transcendental arguments are only an apodictic solution to the Hume s skeptical-naturalist problem when is at stake a practical project in which the interest of reason is ensured, as will, in short, proved in our final considerations

Sistemas de lógica modal em dedução natural

Formalization of logical systems in natural deduction brings many metatheoretical advantages, which Normalization proof is always highlighted. Modal logic systems, until very recently, were not routinely formalized in natural deduction, though some formulations and Normalization proofs are known. This work is a presentation of some important known systems of modal logic in natural deduction, and some Normalization procedures for them, but it is also and mainly a presentation of a hierarchy of modal logic systems in natural deduction, from K until S5, together with an outline of a Normalization proof for the system K, which is a model for Normalization in other systems

Condições de energia de hawking e ellis e a equação de raychaudhuri

In the Einstein s theory of General Relativity the field equations relate the geometry of space-time with the content of matter and energy, sources of the gravitational field. This content is described by a second order tensor, known as energy-momentum tensor. On the other hand, the energy-momentum tensors that have physical meaning are not specified by this theory. In the 700s, Hawking and Ellis set a couple of conditions, considered feasible from a physical point of view, in order to limit the arbitrariness of these tensors. These conditions, which became known as Hawking-Ellis energy conditions, play important roles in the gravitation scenario. They are widely used as powerful tools for analysis; from the demonstration of important theorems concerning to the behavior of gravitational fields and geometries associated, the gravity quantum behavior, to the analysis of cosmological models. In this dissertation we present a rigorous deduction of the several energy conditions currently in vogue in the scientific literature, such as: the Null Energy Condition (NEC), Weak Energy Condition (WEC), the Strong Energy Condition (SEC), the Dominant Energy Condition (DEC) and Null Dominant Energy Condition (NDEC). Bearing in mind the most trivial applications in Cosmology and Gravitation, the deductions were initially made for an energy-momentum tensor of a generalized perfect fluid and then extended to scalar fields with minimal and non-minimal coupling to the gravitational field. We also present a study about the possible violations of some of these energy conditions. Aiming the study of the single nature of some exact solutions of Einstein s General Relativity, in 1955 the Indian physicist Raychaudhuri derived an equation that is today considered fundamental to the study of the gravitational attraction of matter, which became known as the Raychaudhuri equation. This famous equation is fundamental for to understanding of gravitational attraction in Astrophysics and Cosmology and for the comprehension of the singularity theorems, such as, the Hawking and Penrose theorem about the singularity of the gravitational collapse. In this dissertation we derive the Raychaudhuri equation, the Frobenius theorem and the Focusing theorem for congruences time-like and null congruences of a pseudo-riemannian manifold. We discuss the geometric and physical meaning of this equation, its connections with the energy conditions, and some of its several aplications.