A difference field M , is a field with a distinguished endomorphism, is called a generic difference field if it is existentially closed among the models of the theory of difference fields. In the language Ld, by a theorem of Hrushovski, it is characterized by the following: M is an algebraically closed field, s is an automorphism of M, and if W and V are varieties defined over M such that W is a subset of VU s (V ) and the projection maps W to V and W to s(V ) are generically onto, then there is a tuple a in M such that (a, s ( a)) in W. This thesis is a survey on the theory of generic difference fields, called ACFA, which has been studied by Angus Macintyre, Van den Dries, Carol Wood, Ehud Hrushovski and Zoe Chatzidakis. ACFA is the model completion of the theory of algebraically closed difference fields. It is very close to having full quantifier elimination, but it doesn&#039 / t. We can eliminate quantifiers down to formulas with one quantifier and hence obtain the completions of ACFA. This entails the decidability of the theory ACFA as well as its extensions obtained by specifying the characteristic. The fixed field of s is a pseudo-finite field

As the Web Services proliferate and complicate it is becoming an overwhelming job to manually prepare the Web Service Compositions which describe the communication and integration between Web Services. This thesis analyzes the usage of Event Calculus, which is one of the logical action-effect definition languages, for the automated preparation and execution of Web Service Compositions. In this context, planning capabilities of Event Calculus are utilized. Translations from Planning Domain Description Language and DARPA Agent Markup Language to Event Calculus are provided to show that Web Services can be composed with the help of Event Calculus. Also comparisons between Event Calculus and other planning languages used for the same purposes are presented.

No description available.

Thesis (Ph.D.)--Bowling Green State University, 2008. / Document formatted into pages; contains xii, 166 p. Includes bibliographical references.

Thesis (Ph. D.)--University of Chicago, Dept. of Mathematics, June 2000. / Includes bibliographical references. Also available on the Internet.

Intensionality is a phenomenon that occurs in logic and computation. In the most general sense, a function is intensional if it operates at a level finer than (extensional) equality. This is a familiar setting for computer scientists, who often study different programs or processes that are interchangeable, i.e. extensionally equal, even though they are not implemented in the same way, so intensionally distinct. Concomitant with intensionality is the phenomenon of intensional recursion, which refers to the ability of a program to have access to its own code. In computability theory, intensional recursion is enabled by Kleene's Second Recursion Theorem. This thesis is concerned with the crafting of a logical toolkit through which these phenomena can be studied. Our main contribution is a framework in which mathematical and computational constructions can be considered either extensionally, i.e. as abstract values, or intensionally, i.e. as fine-grained descriptions of their construction. Once this is achieved, it may be used to analyse intensional recursion. To begin, we turn to type theory. We construct a modal λ-calculus, called Intensional PCF, which supports non-functional operations at modal types. Moreover, by adding Löb's rule from provability logic to the calculus, we obtain a type-theoretic interpretation of intensional recursion. The combination of these two features is shown to be consistent through a confluence argument. Following that, we begin searching for a semantics for Intensional PCF. We argue that 1-category theory is not sufficient, and propose the use of P-categories instead. On top of this setting we introduce exposures, which are P-categorical structures that function as abstractions of well-behaved intensional devices. We produce three examples of these structures, based on Gödel numberings on Peano arithmetic, realizability theory, and homological algebra. The language of exposures leads us to a P-categorical analysis of intensional recursion, through the notion of intensional fixed points. This, in turn, leads to abstract analogues of classic intensional results in logic and computability, such as Gödel's Incompleteness Theorem, Tarski's Undefinability Theorem, and Rice's Theorem. We are thus led to the conclusion that exposures are a useful framework, which we propose as a solid basis for a theory of intensionality. In the final chapters of the thesis we employ exposures to endow Intensional PCF with an appropriate semantics. It transpires that, when interpreted in the P-category of assemblies on the PCA K1, the Löb rule can be interpreted as the type of Kleene's Second Recursion Theorem.

O uso adequado de ambientes computacionais pode representar um aumento de qualidade e conforto no processo de ensino-aprendizagem de algumas disciplinas. Percebeu-se, através de pesquisa, a inexistência de ferramentas voltadas para o ensino-aprendizagem de cálculo proposicional que atendessem aos critérios estabelecidos para um ambiente de suporte ao aluno (ASA). Como consequência do resultado da pesquisa, este trabalho introduz o conceito e os requisitos básicos de um ASA, concebe e implementa uma ferramenta ASA voltada para o ensino-aprendizagem de cálculo proposicional, acompanhada de um plano de ensino opcional, e os coloca à disposição da comunidade acadêmica. Apresenta também estudos de casos sobre apresentações e usos da ferramenta em vários estágios de desenvolvimento, além da descrição de cada módulo e dos métodos e regras disponibilizados pela ferramenta. Pretende-se que a ferramenta ASA-CalcPro e o plano de ensino sugerido, sejam uma contribuição social positiva e um estímulo ao ensino-aprendizagem de cálculo proposicional. / The adequate use of computational environments can increase the quality and comfort of the teaching-learning process for some of the academic disciplines. A review of the literature reveals the lack of existing tools for the teaching-learning of the propositional calculus that conform to the criteria established for the student support environment (ambiente de suporte ao aluno (ASA)). As a consequence of this conclusion, the current thesis introduces the concept of, and the basic requirements for, an ASA, conceives and implements an ASA tool for the teaching-learning of the propositional calculus, together with an optional teaching plan, and puts both at the disposition of the academic community. The thesis also presents case studies of presentations and uses of the tool at various stages of its development, as well as a description of each module and of the methods and rules made available for use by the tool. It is hoped that the ASA-CalcPro tool and the suggested plan of study will make a positive social contribution and will be a stimulant for the teaching-learning of the propositional calculus.

O uso adequado de ambientes computacionais pode representar um aumento de qualidade e conforto no processo de ensino-aprendizagem de algumas disciplinas. Percebeu-se, através de pesquisa, a inexistência de ferramentas voltadas para o ensino-aprendizagem de cálculo proposicional que atendessem aos critérios estabelecidos para um ambiente de suporte ao aluno (ASA). Como consequência do resultado da pesquisa, este trabalho introduz o conceito e os requisitos básicos de um ASA, concebe e implementa uma ferramenta ASA voltada para o ensino-aprendizagem de cálculo proposicional, acompanhada de um plano de ensino opcional, e os coloca à disposição da comunidade acadêmica. Apresenta também estudos de casos sobre apresentações e usos da ferramenta em vários estágios de desenvolvimento, além da descrição de cada módulo e dos métodos e regras disponibilizados pela ferramenta. Pretende-se que a ferramenta ASA-CalcPro e o plano de ensino sugerido, sejam uma contribuição social positiva e um estímulo ao ensino-aprendizagem de cálculo proposicional. / The adequate use of computational environments can increase the quality and comfort of the teaching-learning process for some of the academic disciplines. A review of the literature reveals the lack of existing tools for the teaching-learning of the propositional calculus that conform to the criteria established for the student support environment (ambiente de suporte ao aluno (ASA)). As a consequence of this conclusion, the current thesis introduces the concept of, and the basic requirements for, an ASA, conceives and implements an ASA tool for the teaching-learning of the propositional calculus, together with an optional teaching plan, and puts both at the disposition of the academic community. The thesis also presents case studies of presentations and uses of the tool at various stages of its development, as well as a description of each module and of the methods and rules made available for use by the tool. It is hoped that the ASA-CalcPro tool and the suggested plan of study will make a positive social contribution and will be a stimulant for the teaching-learning of the propositional calculus.

Made available in DSpace on 2014-06-12T15:48:50Z (GMT). No. of bitstreams: 2 arquivo2717_1.pdf: 481883 bytes, checksum: bb9d70f42c1cda245b5340284b5dc431 (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2011 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / Nesta tese, provamos que todo domínio infinito finitamente gerado é bi-interpretável com a estrutura dos números naturais. Usando este argumento, demonstramos que todo anel f.g. R que tem um ideal primo nilpotente I tal que R/I é um domínio é Quase-Finitamente Axiomatizável

Submitted by Renata Lopes (renatasil82@gmail.com) on 2017-01-13T17:27:04Z No. of bitstreams: 1 thiagodeoliveiraalves.pdf: 655489 bytes, checksum: e3e858183683f82164e751d989a96b35 (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-02-07T13:56:24Z (GMT) No. of bitstreams: 1 thiagodeoliveiraalves.pdf: 655489 bytes, checksum: e3e858183683f82164e751d989a96b35 (MD5) / Approved for entry into archive by Adriana Oliveira (adriana.oliveira@ufjf.edu.br) on 2017-02-07T14:05:47Z (GMT) No. of bitstreams: 1 thiagodeoliveiraalves.pdf: 655489 bytes, checksum: e3e858183683f82164e751d989a96b35 (MD5) / Made available in DSpace on 2017-02-07T14:05:47Z (GMT). No. of bitstreams: 1 thiagodeoliveiraalves.pdf: 655489 bytes, checksum: e3e858183683f82164e751d989a96b35 (MD5) Previous issue date: 2016-07-18 / O uso da Lógica é de fundamental importância no desenvolvimento de teorias matemáticas modernas, que buscam deduzir de axiomas e conceitos primitivos todo seu corpo de teoremas e consequências. O objetivo desta dissertação é descrever as ferramentas da Lógica Formal que possam ter aplicações imediatas nas demonstrações de conjecturas e teoremas, trazendo justificativa e significado para as técnicas dedutivas e argumentos normalmente utilizados na Matemática. Além de temas introdutórios sobre argumentação e âmbito da lógica, o trabalho todo é apresentado por método sistemático em busca de um critério formal que possa separar os argumentos válidos dos inválidos. Conclui-se que com uma boa preparação inicial no campo da Lógica Formal, o matemático iniciante possa ter uma referência sobre como proceder estrategicamente nos processos de provas de conjecturas e um conhecimento mais profundo ao entender os motivos da validade dos teoremas que encontrará ao se dedicar a sua área de formação. / TheuseofLogicisoffundamentalimportanceinthedevelopmentofmodernmathematical theories that seek deduce from axioms and primitive concepts all your body of theorems and consequences. The aim of this work is to describe the tools of Formal Logic that may have immediate applications in the statements of theorems and conjectures, bringing justification and meaning to the deductive techniques and arguments commonly used in Mathematics. In addition to introductory topics on argumentation and scope of Logic, all the work is presented by systematic method in search of a formal criterion that can separate the valid arguments of the invalids. It follows that with a good initial preparation in the field of Formal Logic, the novice mathematician could have a reference on how to strategically proceed in conjectures evidence processes and a deeper knowledge to understand the reasons for the validity of theorems found on their training area.