Die vorliegende Dissertation hat als unmittelbares Ziel, die Verwandtschaft zwischen den Werken von Parmenides, Zenon und Empedokles zu untersuchen und aufzuzeigen, wie überaus stark die beiden letzten vom ersten abhängen. Im Werk des Parmenides finden Zenon und Empedokles ihren Ausgangspunkt und ihren Beweggrund. Nachdem die enge verwandtschaftliche Beziehung der Werke und damit die Verbindung der Autoren aufgezeigt wurde, wird ausgeführt, wie Zenon und Empedokles die Umdeutung der parmenideischen Gedanken betreiben, und zwar unter besonderer Berücksichtigung der Frage des Seienden, da sowohl die unbestreitbaren Ähnlichkeiten wie die entscheidenden Unterschiede sich speziell im Bereich der parmenideischen Konzeption des Seienden und dessen Wiedererarbeitung durch Zenon und Empedokles befinden, was diesen beiden Autoren den soliden Aufbau eines eigenen Denkens und einer eigenen Philosophie ermöglicht. Diese geht grundlegend von einer Unterscheidung der parmenideischen Vernunft aus. Aus dieser Konstellation resultiert die singuläre Beziehung der Philosophie Zenons und auch der von Empedokles zur parmenideischen Philosophie: einerseits entfernen sie sich von dieser, andereseits sind sie ihr sehr nahe; sowohl gelangen sie zu einem eigenständigen Denkinhalt, als auch bleiben sie unvermeidlich an ihre Matrix gebunden.

Orientador: Maria de Fátima Morethy Couto / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Artes / Made available in DSpace on 2018-08-17T10:12:09Z (GMT). No. of bitstreams: 1 Costa_SabrinaAlbuquerquedeAraujo_M.pdf: 4834519 bytes, checksum: d61f8e8e98414d10c3535b098e7c5b2c (MD5) Previous issue date: 2010 / Resumo: Esta pesquisa teve por finalidade analisar os trabalhos do artista cearense Zenon Barreto na cidade de Fortaleza, no Ceará. Considerando a metade do século 20 como recorte histórico e artístico, foram analisadas as limitações e especificidades das obras do artista de acordo com os valores estéticos do modernismo brasileiro. Inicialmente, foi delineado um panorama do meio artístico cearense da época com o objetivo de contextualizar o artista e as obras em questão. Em seguida, foram apresentadas algumas considerações a respeito do conceito de arte pública e suas ressignificações no decorrer do tempo, que contribuíram para uma melhor compreensão dos trabalhos em espaços públicos da capital cearense. Por fim, as obras do artista em questão foram apresentadas e analisadas, estabelecendo sempre que necessário um diálogo com a produção artística cearense e brasileira / Abstract: This research had for purpose analyze the works of the artist Zenon Barreto in the city of Fortaleza, in Ceará. Considering the half of the century 20 as artistic and historical cutting, were analyzed the limitations and specificities of the works of the artist according to the esthetic values of the Brazilian modernism. Initially, it was delineated a panorama of the local artistic environment of the epoch with the objective of put into context the artist and the works in question. Right away, were presented some considerations about the concept of public art and its meanings in elapse of the time, that contributed for a better comprehension of the works in public spaces of the capital of Ceará. Finally, the works of the artist in question were presented and analyzed, establishing whenever necessary a dialogue with the local and Brazilian artistic works / Mestrado / Artes / Mestre em Artes

O debate da imagética mental consiste de uma controvérsia iniciada nos anos 1970 a respeito da forma das representações mentais, e foi travada principalmente entre Stephen Kosslyn, que propunha uma forma imagética, e Zenon Pylyshyn, que propunha um formato simbólico-estrutural, além de apontar falhas conceituais na teoria da afiguração implícita no modelo pictorialista. Nesta dissertação, apresenta-se um balanço filosófico deste debate, levando em conta também críticas adicionais de Daniel Dennett aos pressupostos da abordagem pictorialista. / The mental imagery debate is a controversy that began in the 1970s concerning the form of mental representation, and was carried out mainly by Stephen Kosslyn, who defended a picture-like representation, and Zenon Pylyshyn, who proposed a symbolic-structural format. The latter also pointed out conceptual problems of the pictorialist model. This thesis presents a philosophical discussion of the debate, also taking into account additional criticisms by Daniel Dennett to the presuppositions of the pictorialist approach.

O debate da imagética mental consiste de uma controvérsia iniciada nos anos 1970 a respeito da forma das representações mentais, e foi travada principalmente entre Stephen Kosslyn, que propunha uma forma imagética, e Zenon Pylyshyn, que propunha um formato simbólico-estrutural, além de apontar falhas conceituais na teoria da afiguração implícita no modelo pictorialista. Nesta dissertação, apresenta-se um balanço filosófico deste debate, levando em conta também críticas adicionais de Daniel Dennett aos pressupostos da abordagem pictorialista. / The mental imagery debate is a controversy that began in the 1970s concerning the form of mental representation, and was carried out mainly by Stephen Kosslyn, who defended a picture-like representation, and Zenon Pylyshyn, who proposed a symbolic-structural format. The latter also pointed out conceptual problems of the pictorialist model. This thesis presents a philosophical discussion of the debate, also taking into account additional criticisms by Daniel Dennett to the presuppositions of the pictorialist approach.

Cette thèse revisite les problèmes d'accessibilité et de vivacité pour les au-tomates temporisés.L'accessibilité est couramment résolue par le calcul d'un arbre de recherche abstrait. L'abstraction est paramétrée par des bornes provenant des gardes de l'automate. Nous montrons que l'abstraction a 4LU de Behrmann et al. est la plus grande abstraction saine et complète pour les bornes LU. N' étant pas convexe, elle n'est pas mise en oeuvre dans les outils. Nous introduisons une méthode qui permet son utilisation éfficace. Finalement, nous proposons une optimisation des bornes à la volée exploitant le calcul de l'arbre.Le problème de vivacité requiert de détecter les exécutions Zenon/non-Zenon. Une solution standard ajoute une horloge à l'automate. Nous montrons qu'elle conduit a une explosion combinatoire. Nous proposons une solution qui évite ce problème pour une grande classe d'abstractions. Pour les abstractions LU nous montrons que détecter ces exécutions est un problèmeNP-complet. / We consider the classic model of timed automata introduced by Alurand Dill. Two fundamental properties one would like to check in this modelare reachability and liveness. This thesis revisits these classical problems.The reachability problem for timed automata asks if there exists a run ofthe automaton from the initial state to a given final state. The standard solutionto this problem constructs a search tree whose nodes are abstractionsof zones. For effectiveness, abstractions are parameterized by maximal lowerand upper bounds (LU-bounds) occurring in the guards of the automaton.Such abstractions are also termed as LU-abstractions. The a4LU abstractiondefined by Behrmann et al is the coarsest known LU-abstraction. Althoughit is potentially most productive to use the a4LU abstraction, it has not beenused in implementations as it could lead to non-convex sets. We show howone could use the a4LU abstraction efficiently in implementations. Moreover,we prove that a4LU abstraction is optimal: given only the LU-bound information,it is the coarsest possible abstraction that is sound and completefor reachability. We then concentrate on ways to get better LU-bounds. Inthe standard procedure the LU-bounds are obtained from a static analysisof the automaton. We propose a new method to obtain better LU-boundson-the-fly during exploration of the zone graph. The potential gains of proposedimprovements are validated by experimental results on some standardverification case studies.The liveness problem deals with infinite executions of timed automata.An infinite execution is said to be Zeno if it spans only a finite amountof time. Such runs are considered unrealistic. While considering infiniteexecutions, one has to eliminate Zeno runs or dually, find runs that arenon-Zeno. The B¨uchi non-emptiness problem for timed automata asks ifthere exists a non-Zeno run visiting an accepting state infinitely often. Thestandard solution to this problem adds an extra clock to take care of non-Zenoness. We show that this solution might lead to an exponential blowupin the search space. We propose a method avoiding this blowup for a wideclass of abstractions weaker than LU-abstractions. We show that such amethod does not exist for LU-abstractions unless P=NP. Another questionrelated to infinite executions of timed automata is to decide the existenceof Zeno runs. We provide the first complete solution to this problem. Itworks for a wide class of abstractions weaker than LU. Yet again, we showthe solution could lead to a blowup for LU-abstractions, unless P=NP.

Public part of this work summarizes theoretical knowledge of industrial visualization from definition of basic concepts to more specific description of the types and possibilities of current visualization. The second part deals with design and creation application for automatic data import and creation of graphic library of symbols conveyor technology for Zenon. To protect know-how of atx – technicka kancelar pro komplexni automatizaci s.r.o. is this part private.

Les techniques de refroidissement laser ont réalisé des progrès immenses depuis le début des années 80. Affranchis de toutes les incertitudes inhérentes au mouvement thermique, les physiciens sont désormais en mesure de réaliser des dispositifs de mesure toujours plus précis, tels des horloges ou des gravimètres, en s'appuyant sur l'interaction parfaitement contrôlée entre le champ électromagnétique et de simples nuages d'atomes. De plus en plus, l'utilisation d'atomes ou d'ions comme ultime porteurs d'information apparait comme une solution plausible à la réalisation d'ordinateurs quantiques. Dans cette optique, de nombreux efforts sont consentis afin de miniaturiser, de simplifier, et de rendre possible la production en masse de cette technologie permettant de manipuler les atomes avec tant de précision. L'introduction des puces à atomes a permis de réaliser un grand pas dans cette direction, réduisant drastiquement l'encombrement et le coût des expériences de refroidissement d'atomes. Désormais, la réalisation de dispositifs sur puce permettant d'étendre les possibilités de manipulation des atomes piégés est devenue un objectif majeur. <br> Dans ce travail de thèse, nous avons réalisé le premier détecteur d'atomes uniques piégés sur une puce à atomes, basé sur l'interaction avec un mode de cavité optique dans le régime de couplage fort. La cavité optique est directement intégrée à la puce à atomes. Fonctionnant dans le régime de détection dite "non-destructive", le dispositif de détection permet de préparer de manière déterministe un atome unique piégé dans un piège dipolaire, avec une précision en position submicrométrique, et dans un état interne spécifique. La détection en tant que telle permet de mesurer l'état hyperfin de l'atome, en perturbant son état externe nettement moins qu'un système de détection fonctionnant en espace libre. <br> Ce nouveau dispositif de préparation et de mesure est utilisé dans une expérience d'effet Zénon quantique, la première à être effectuée avec des atomes neutres individuels. Sous l'effet de la mesure, l'oscillation de Rabi entre les deux sous-niveaux hyperfins $\s{F=1}$ et $\s{F=2}$ du niveau fondamental de l'atome de Rubidium 87 est stoppée. L'expérience, effectuée à la fois dans le régime continu et le régime pulsé, permet de montrer l'adéquation entre le flux d'information extraite du système et le flux de photons traversant la cavité optique de détection.

Nous avons realise une mesure Quantiques Non Destructives du nombre de photons d'un champ piege dans une cavite de temps d'amortissement T=0,13s. Nous envoyons des atomes de Rydberg circulaires a travers la cavite ou une interaction dispersive deplace leur frequence propre proportionnellement au nombre de photons. Ce deplacement lumineux est detecte par interferometrie atomique de Ramsey. Le temps d'amortissement du champ est suffisamment long pour permettre d'observer les sauts quantiques du nombre de photons dus a la relaxation. L'analyse statistique des differentes trajectoires permet de realiser une tomographie partielle de ce processus responsable de la decoherence des etats de Fock |n> en un temps T/n. La projection d'un champ initialement coherent sur un etat de Fock lors de la mesure s'accompagne d'une dispersion totale de sa phase. Cette action en retour est utilisee pour geler la croissance coherente du champ par effet Zenon quantique.

Cette thèse porte sur la vérification des règles ajoutées de l'Atelier B en utilisant une plate-forme appelée BCARe qui repose sur un plongement de la théorie sous-jacente à la méthode B (théorie de B) dans l'assistant à la preuve Coq. En particulier, nous proposons trois approches pour prouver la validité d'une règle, ce qui revient à prouver une formule exprimée dans la théorie de B. Ces trois approches ont été évaluées sur les règles de la base de règles de SIEMENS IC-MOL. La première approche dite autarcique est développée avec le langage de tactiques de Coq Ltac.  Elle repose sur une première étape qui consiste à déplier tous les opérateurs ensemblistes pour obtenir une formule de la logique du premier ordre. Puis nous appliquons une procédure de décision qui met en oeuvre une heuristique naïve en ce qui concerne les instanciations. La deuxième approche, dite sceptique,appelle le prouveur automatique de théorèmes Zenon après avoir effectué l'étape de normalisation précédente. Nous vérifions ensuite les preuves trouvées par Zenon dans le plongement profond de B en Coq.  La troisième approche évite l'étape de normalisation précédente grâce à une extension de Zenon utilisant des règles d'inférence spécifiques à la théorie de B. Ces règles sont obtenues grâce à la technique de superdéduction. Cette dernière approche est généralisée en une extension de Zenon à toute théorie grâce à un calcul dynamique des règles de superdéduction. Ce nouvel outil, appelé Super Zenon, peut par exemple prouver des problèmes issus de la bibliothèque de problèmes TPTP. / The purpose of this thesis is the verification of Atelier B added rules using the framework named BCARe which relies on a deep embedding of the B theory within the logic of the Coq proof assistant. We propose especially three approaches in order to prove the validity of a rule, which amounts to prove a formula expressed in the B theory. These three approaches have been assessed on the rules coming from the rule database maintained by Siemens IC-MOL.  To do so, the first approach, so-called autarkic approach, is developed thanks to the Coq tactic language, Ltac. It rests upon a first step which consists in unfolding the set operators so as to obtain a first order formula.  A decision procedure which implements an heuristic is applied afterwards to deal with instantiation.  We propose a second approach, so-called skeptic approach, which uses the automated first order theorem prover Zenon, after the previous normalization step has been applied.  Then we verify the Zenon proofs in the deep embedding of B in Coq. A third approach consists in using anextension of Zenon to the B method thanks to the superdeduction. Superdeduction allows us to add the axioms of the B theory by means of deduction rules in the proof mechanism of Zenon. This last approach is generalized in an extension of Zenon to every theory thanks to a dynamic calculus of the superdeduction rules. This new tool, named Super Zenon, is able to prove problems coming from the problem library TPTP, for example.