Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Analyse der temporären Neuroblastenbildung und der segmentalen Spezifizierung des Neuroblasten 6-4 im embryonalen zentralen Nervensystem von Drosophila melanogaster

Die vorliegende Arbeit gewährte neue Einblicke in zwei fundamentale Vorgänge der frühen Neurogenese von Drosophila melanogaster. Der erste Teil untersuchte die zeitliche Spezifizierung der Neuroblastenidentitäten. Durch die Expression verschiedener Gene entlang der Dorsoventral- und der Anterioposteriorachse wird ein kartesisches Koordinatensystem aufgebaut, indem ein Neuroblast (NB), der in einem bestimmten Quadranten entsteht, eine spezifische Identität erhält. Die Delamination der NBs erfolgt in fünf Segregationswellen, wobei in jeder Welle die gleiche Population NBs gebildet wird. In dieser Arbeit konnte nun gezeigt werden, dass es nicht nur einen räumlichen, sondern auch einen zeitlichen Aspekt bei der Entstehung der NBs gibt: So zeigten Transplantationsexperimente, dass sowohl im frühen als auch im späten Neuroektoderm extrinsische induktive Signale an der Spezifizierung der Neuroblastenidentität beteiligt sind. Die Natur dieser Signale bleibt noch unklar. Allerdings stellen die Segmentpolaritätsgene aufgrund ihrer dynamischen Expression eine potenzielle Kandidatengruppe dar. Der zweite Teil beschäftigte sich mit der segmentalen Spezifizierung der Neuroblasten. Für diesen Prozess zeigten frühere Genexpressionsstudien, dass NBs, die zwar an korrespondierenden Positionen innerhalb des kartesischen Systems, aber in unterschiedlichen Segmenten gebildet werden, die gleichen Genexpressionsmuster aufweisen und fast identische Zellstammbäume hervorbringen. Einige dieser seriell homologen NBs generieren jedoch segmentspezifische Zellstammbäume – ein solches Beispiel ist der NB6-4, der als Modellsystem benutzt wurde. Für die thorakale Variante dieses NBs konnte ich zeigen, dass die Homöotischen Gene zur Spezifizierung nicht notwendig sind – thorakales Schicksal ist eine Grundidentität. Diese wird in abdominalen Segmenten jedoch durch die Funktion der Homöotischen Gene abdominal-A (abd-A) und Abdominal-B (Abd-B) in abdominales Schicksal transformiert. Dieser segmentale Unterschied wird durch die Regulation des Zellzyklusgens CycE bewerkstelligen. Genauer: CycE ist notwendig, um neurogliales Schicksal in thorakalen Segmenten zu generieren und ausreichend, dieses Schicksal ebenfalls in abdominalen Segmenten zu erzeugen. Eine direkte Inhibierung der Expression von CycE durch Abd-A in abdominalen Segmenten führt dagegen zu einer differenziellen Expression von CycE im neuronalen thorakalen Anteil des Zellstammbaums. Weiterhin konnten in einem Enhancerelement, das für die Expression von CycE im Nervensystem verantwortlich ist, mehrere Bindestellen für Abd-A und Abd-B gefunden werden. Die gewonnen Daten legen – in Verbindung mit bereits bekannten Ergebnissen – den Schluss nahe, dass diese neuronspezifizierende Funktion von CycE unabhängig von seiner Rolle im Zellzyklus ist.

Does improvisation lead to outcome deviation? A conceptual framework of improvisation, its antecedents and outcome deviation

Management and organization literature has extensively noticed the crucial role that improvisation assumes in organizations, both as a learning process (Miner, Bassoff & Moorman, 2001), a creative process (Fisher & Amabile, 2008), a capability (Vera & Crossan, 2005), and a personal disposition (Hmielesky & Corbett, 2006; 2008). My dissertation aims to contribute to the existing literature on improvisation, addressing two general research questions: 1) How does improvisation unfold at an individual level? 2) What are the potential antecedents and consequences of individual proclivity to improvise? This dissertation is based on a mixed methodology that allowed me to deal with these two general research questions and enabled a constant interaction between the theoretical framework and the empirical results. The selected empirical field is haute cuisine and the respondents are the executive chefs of the restaurants awarded by Michelin Guide in 2010 in Italy. The qualitative section of the dissertation is based on the analysis of 26 inductive case studies and offers a multifaceted contribution. First, I describe how improvisation works both as a learning and creative process. Second, I introduce a new categorization of individual improvisational scenarios (demanded creative improvisation, problem solving improvisation, and pure creative improvisation). Third, I describe the differences between improvisation and other creative processes detected in the field (experimentation, brainstorming, trial and error through analytical procedure, trial and error, and imagination). The quantitative inquiry is founded on a Structural Equation Model, which allowed me to test simultaneously the relationships between proclivity to improvise and its antecedents and consequences. In particular, using a newly developed scale to measure individual proclivity to improvise, I test the positive influence of industry experience, self-efficacy, and age on proclivity to improvise and the negative impact of proclivity to improvise on outcome deviation. Theoretical contributions and practical implications of the results are discussed.

Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

La concezione epistemica dell'analiticità: un dibattito in corso

Il lavoro è una riflessione sugli sviluppi della nozione di definizione nel recente dibattito sull'analiticità. La rinascita di questa discussione, dopo le critiche di Quine e un conseguente primo abbandono della concezione convenzionalista carnapiana ha come conseguenza una nuova concezione epistemica dell'analiticità. Nella maggior parte dei casi le nuove teorie epistemiche, tra le quali quelle di Bob Hale e Crispin Wright (Implicit Definition and the A priori, 2001) e Paul Boghossian (Analyticity, 1997; Epistemic analyticity, a defence, 2002, Blind reasoning, 2003, Is Meaning Normative ?, 2005) presentano il comune carattere di intendere la conoscenza a priori nella forma di una definizione implicita (Paul Horwich, Stipulation, Meaning, and Apriority, 2001). Ma una seconda linea di obiezioni facenti capo dapprima a Horwich, e in seguito agli stessi Hale e Wright, mettono in evidenza rispettivamente due difficoltà per la definizione corrispondenti alle questioni dell'arroganza epistemica e dell'accettazione (o della stipulazione) di una definizione implicita. Da questo presupposto nascono diversi tentativi di risposta. Da un lato, una concezione della definizione, nella teoria di Hale e Wright, secondo la quale essa appare come un principio di astrazione, dall'altro una nozione della definizione come definizione implicita, che si richiama alla concezione di P. Boghossian. In quest'ultima, la definizione implicita è data nella forma di un condizionale linguistico (EA, 2002; BR, 2003), ottenuto mediante una fattorizzazione della teoria costruita sul modello carnapiano per i termini teorici delle teorie empiriche. Un'analisi attenta del lavoro di Rudolf Carnap (Philosophical foundations of Physics, 1966), mostra che la strategia di scomposizione rappresenta una strada possibile per una nozione di analiticità adeguata ai termini teorici. La strategia carnapiana si colloca, infatti, nell'ambito di un tentativo di elaborazione di una nozione di analiticità che tiene conto degli aspetti induttivi delle teorie empiriche

Iodine speciation in atmospheric aerosols in the marine boundary layer

Iodine chemistry plays an important role in the tropospheric ozone depletion and the new particle formation in the Marine Boundary Layer (MBL). The sources, reaction pathways, and the sinks of iodine are investigated using lab experiments and field observations. The aims of this work are, firstly, to develop analytical methods for iodine measurements of marine aerosol samples especially for iodine speciation in the soluble iodine; secondly, to apply the analytical methods in field collected aerosol samples, and to estimate the characteristics of aerosol iodine in the MBL. Inductively Coupled Plasma – Mass Spectrometry (ICP-MS) was the technique used for iodine measurements. Offline methods using water extraction and Tetra-methyl-ammonium-hydroxide (TMAH) extraction were applied to measure total soluble iodine (TSI) and total insoluble iodine (TII) in the marine aerosol samples. External standard calibration and isotope dilution analysis (IDA) were both conducted for iodine quantification and the limits of detection (LODs) were both 0.1 μg L-1 for TSI and TII measurements. Online couplings of Ion Chromatography (IC)-ICP-MS and Gel electrophoresis (GE)-ICP-MS were both developed for soluble iodine speciation. Anion exchange columns were adopted for IC-ICP-MS systems. Iodide, iodate, and unknown signal(s) were observed in these methods. Iodide and iodate were separated successfully and the LODs were 0.1 and 0.5 μg L-1, respectively. Unknown signals were soluble organic iodine species (SOI) and quantified by the calibration curve of iodide, but not clearly identified and quantified yet. These analytical methods were all applied to the iodine measurements of marine aerosol samples from the worldwide filed campaigns. The TSI and TII concentrations (medians) in PM2.5 were found to be 240.87 pmol m-3 and 105.37 pmol m-3 at Mace Head, west coast of Ireland, as well as 119.10 pmol m-3 and 97.88 pmol m-3 in the cruise campaign over the North Atlantic Ocean, during June – July 2006. Inorganic iodine, namely iodide and iodate, was the minor iodine fraction in both campaigns, accounting for 7.3% (median) and 5.8% (median) in PM2.5 iodine at Mace Head and over the North Atlantic Ocean, respectively. Iodide concentrations were higher than iodate in most of the samples. In the contrast, more than 90% of TSI was SOI and the SOI concentration was correlated significantly with the iodide concentration. The correlation coefficients (R2) were both higher than 0.5 at Mace Head and in the first leg of the cruise. Size fractionated aerosol samples collected by 5 stage Berner impactor cascade sampler showed similar proportions of inorganic and organic iodine. Significant correlations were obtained in the particle size ranges of 0.25 – 0.71 μm and 0.71 – 2.0 μm between SOI and iodide, and better correlations were found in sunny days. TSI and iodide existed mainly in fine particle size range (< 2.0 μm) and iodate resided in coarse range (2.0 – 10 μm). Aerosol iodine was suggested to be related to the primary iodine release in the tidal zone. Natural meteorological conditions such as solar radiation, raining etc were observed to have influence on the aerosol iodine. During the ship campaign over the North Atlantic Ocean (January – February 2007), the TSI concentrations (medians) ranged 35.14 – 60.63 pmol m-3 among the 5 stages. Likewise, SOI was found to be the most abundant iodine fraction in TSI with a median of 98.6%. Significant correlation also presented between SOI and iodide in the size range of 2.0 – 5.9 μm. Higher iodate concentration was again found in the higher particle size range, similar to that at Mace Head. Airmass transport from the biogenic bloom region and the Antarctic ice front sector was observed to play an important role in aerosol iodine enhancement. The TSI concentrations observed along the 30,000 km long cruise round trip from East Asia to Antarctica during November 2005 – March 2006 were much lower than in the other campaigns, with a median of 6.51 pmol m-3. Approximately 70% of the TSI was SOI on average. The abundances of inorganic iodine including iodine and iodide were less than 30% of TSI. The median value of iodide was 1.49 pmol m-3, which was more than four fold higher than that of iodate (median, 0.28 pmol m-3). Spatial variation indicated highest aerosol iodine appearing in the tropical area. Iodine level was considerably lower in coastal Antarctica with the TSI median of 3.22 pmol m-3. However, airmass transport from the ice front sector was correlated with the enhance TSI level, suggesting the unrevealed source of iodine in the polar region. In addition, significant correlation between SOI and iodide was also shown in this campaign. A global distribution in aerosol was shown in the field campaigns in this work. SOI was verified globally ubiquitous due to the presence in the different sampling locations and its high proportion in TSI in the marine aerosols. The correlations between SOI and iodide were obtained not only in different locations but also in different seasons, implying the possible mechanism of iodide production through SOI decomposition. Nevertheless, future studies are needed for improving the current understanding of iodine chemistry in the MBL (e.g. SOI identification and quantification as well as the update modeling involving organic matters).

Institutional Processes and Discursive Strategies: Rhetoric and Vocabulary Analysis of CSR and Sustainability

The candidate tackled an important issue in contemporary management: the role of CSR and Sustainability. The research proposal focused on a longitudinal and inductive research, directed to specify the evolution of CSR and contribute to the new institutional theory, in particular institutional work framework, and to the relation between institutions and discourse analysis. The documental analysis covers all the evolution of CSR, focusing also on a number of important networks and associations. Some of the methodologies employed in the thesis have been employed as a consequence of data analysis, in a truly inductive research process. The thesis is composed by two section. The first section mainly describes the research process and the analyses results. The candidates employed several research methods: a longitudinal content analysis of documents, a vocabulary research with statistical metrics as cluster analysis and factor analysis, a rhetorical analysis of justifications. The second section puts in relation the analysis results with theoretical frameworks and contributions. The candidate confronted with several frameworks: Actor-Network-Theory, Institutional work and Boundary Work, Institutional Logic. Chapters are focused on different issues: a historical reconstruction of CSR; a reflection about symbolic adoption of recurrent labels; two case studies of Italian networks, in order to confront institutional and boundary works; a theoretical model of institutional change based on contradiction and institutional complexity; the application of the model to CSR and Sustainability, proposing Sustainability as a possible institutional logic.

Monitoring Complex Processes to Verify System Conformance: A Declarative Rule-Based Framework

Over the last 60 years, computers and software have favoured incredible advancements in every field. Nowadays, however, these systems are so complicated that it is difficult – if not challenging – to understand whether they meet some requirement or are able to show some desired behaviour or property. This dissertation introduces a Just-In-Time (JIT) a posteriori approach to perform the conformance check to identify any deviation from the desired behaviour as soon as possible, and possibly apply some corrections. The declarative framework that implements our approach – entirely developed on the promising open source forward-chaining Production Rule System (PRS) named Drools – consists of three components: 1. a monitoring module based on a novel, efficient implementation of Event Calculus (EC), 2. a general purpose hybrid reasoning module (the first of its genre) merging temporal, semantic, fuzzy and rule-based reasoning, 3. a logic formalism based on the concept of expectations introducing Event-Condition-Expectation rules (ECE-rules) to assess the global conformance of a system. The framework is also accompanied by an optional module that provides Probabilistic Inductive Logic Programming (PILP). By shifting the conformance check from after execution to just in time, this approach combines the advantages of many a posteriori and a priori methods proposed in literature. Quite remarkably, if the corrective actions are explicitly given, the reactive nature of this methodology allows to reconcile any deviations from the desired behaviour as soon as it is detected. In conclusion, the proposed methodology brings some advancements to solve the problem of the conformance checking, helping to fill the gap between humans and the increasingly complex technology.

Sistemi per la produzione di enzimi industriali finalizzati alla valorizzazione di scarti agroalimentari

La demolizione idrolitica delle pareti cellulari delle piante tramite enzimi lignocellulosici è quindi uno degli approcci più studiati della valorizzazione di scarti agricoli per il recupero di fitochimici di valore come secondary chemical building block per la chimica industriale. White rot fungi come il Pleurotus ostreatus producono una vasta gamma di enzimi extracellulari che degradano substrati lignocellulosici complessi in sostanze solubili per essere utilizzati come nutrienti. In questo lavoro abbiamo studiato la produzione di diversi tipi di enzimi lignocellulosici quali cellulase, xilanase, pectinase, laccase, perossidase e arylesterase (caffeoilesterase e feruloilesterase), indotte dalla crescita di Pleurotus ostreatus in fermentazione allo stato solido (SSF) di sottoprodotti agroalimentari (graspi d’uva, vinaccioli, lolla di riso, paglia di grano e crusca di grano) come substrati. Negli ultimi anni, SSF ha ricevuto sempre più interesse da parte dei ricercatori, dal momento che diversi studi per produzioni di enzimi, aromi, coloranti e altre sostanze di interesse per l' industria alimentare hanno dimostrato che SSF può dare rendimenti più elevati o migliorare le caratteristiche del prodotto rispetto alla fermentazione sommersa. L’utilizzo dei sottoprodotti agroalimentari come substrati nei processi SSF, fornisce una via alternativa e di valore, alternativa a questi residui altrimenti sotto/o non utilizzati. L'efficienza del processo di fermentazione è stato ulteriormente studiato attraverso trattamenti meccanici di estrusione del substrato , in grado di promuovere il recupero dell’enzima e di aumentare l'attività prodotta. Le attività enzimatiche prodotte dalla fermentazione sono strettamente dipendente della rimozione periodica degli enzimi prodotti. Le diverse matrici vegetali utilizzate hanno presentato diversi fenomeni induttivi delle specifiche attività enzimatiche. I processi SSF hanno dimostrato una buona capacità di produrre enzimi extracellulari in grado di essere utilizzati successivamente nei processi idrolitici di bioraffinazione per la valorizzazione dei prodotti agroalimentari.

Biofunktionalisierung oxidischer Titanoberflächen über eine spezifische Anbindung von biotinyliertem Fibronektin für die medizinische Anwendung

In der hier vorliegenden Dissertation wird die Entwicklung und Charakterisierung einer biomimetischen Beschichtung für Titanimplantatoberflächen, insbesondere Dentalimplantate, beschrieben. Ziel war es, die Adhäsion und Aktivität von Osteoblasten auf Titanoberflächen zu steigern und so eine Beschleunigung der Implantatintegration in das Knochengewebe zu erreichen. Hierfür wurde eine spezielle Art der biomimetischen Beschichtung entwickelt, bei der biotinyliertes Fibronektin (bFn) über Streptavidin auf eine biotinylierte TiOX-Modelloberfläche immobilisiert wurde. Die Biotinmodifizierung der TiOX-Oberfläche erfolgte hierbei über einen „Self-Assembly-Prozess“ durch sequenzielle Chemiesorption von N-(6-aminohexyl)aminopropyltrimethoxysilan sowie verschiedenen Sulfo-NHS-Biotin-Derivaten, welche den Aufbau einer Streptavidin-Monolage ermöglichten. Als ein wichtiges Resultat zeigte sich, dass die Streptavidin-Monolage effektiv die unspezifische Adsorption von Proteinen an die TiOX-Oberfläche unterbindet und hierdurch die Adhäsion von Osteoblasten auf dieser unterdrückt. Dies hat den Vorteil, dass auf eine antiadhäsive Basisbeschichtung, welche für eine spezifische Zellreaktion wichtig ist, verzichtet werden kann. Dieses osteoblastere Adhäsionsverhalten änderte sich signifikant nach Anbindung von bFn an die Streptavidin-Monolage, mit dem Ergebnis, einer drastischen Steigerung der Osteoblastenadhäsion. Weiterhin besaßen Osteoblasten auf diesen Oberflächen ein Proteinexpressionsmuster, das auf eine erhöhte Osteoinduktion schließen lässt. Es zeigte sich darüber hinaus eine verstärkte Zelladhäsion sowie eine Steigerung des osteoinduktiven Effekts auf Substraten, bei denen bFn über eine Streptavidin-Monolage immobilisiert wurde, gegenüber mit nativem Fibronektin (Fn) modifizierten TiOX-Oberflächen. Ein wesentlicher Schwerpunkt bestand daher in der Analyse der Zusammensetzung und Struktur der biomimetischen Beschichtung über „Surface Plasmon Spectroscopy“ und „Atomic Force Microscopy“. Diese ergab, dass bFn und natives Fn auf den jeweiligen Oberflächen eine unterschiedliche Konformation einnimmt. Im Gegensatz zu nativem Fn, das bei der Adsorption unter physiologischen Bedingungen auf TiOX-Oberflächen eine kompakte Konformation besitzt, nimmt bFn auf einer Streptavidin-Monolage eine entfaltete Konformation ein. Bei letzterer handelt es sich um dieselbe, welche Fn in vivo innerhalb der extrazellulären Matrix besitzt. Sie unterscheidet sich von der kompakten Fn-Konformation dahingehend, dass entlang der Fn-Achse weitere Proteinbindestellen zugänglich werden und hierdurch die Zellaffinität von Fn gesteigert wird. Die nachgewiesene Konformationsänderung kann somit als Grund für die gesteigerte Osteoblasten-Adhäsion und Aktivität auf Oberflächen mit bFn angenommen werden. Diese Kenntnisse konnten weiterhin für die Optimierung des biomimetischen Schichtsystems genutzt werden. So war es möglich, durch alternierendes Inkubieren der Biotin-aktivierten Oberfläche mit Streptavidin und bFn, ein Multilayersystem gezielt aufzubauen. Der Vorteil dieses Multilayersystems gegenüber einer einfachen Monolage aus bFn besteht in einer erhöhten Stabilität der biomimetischen Beschichtung, wodurch eine Anwendung in der Praxis erleichtert würde.

Charge-transport simulations in organic semiconductors

In this thesis we have extended the methods for microscopic charge-transport simulations for organic semiconductors. In these materials the weak intermolecular interactions lead to spatially localized charge carriers, and the charge transport occurs as an activated hopping process between diabatic states. In addition to weak electronic couplings between these states, different electrostatic environments in the organic material lead to a broadening of the density of states for the charge energies which limits carrier mobilities.rnThe contributions to the method development includern(i) the derivation of a bimolecular charge-transfer rate,rn(ii) the efficient evaluation of intermolecular (outer-sphere) reorganization energies,rn(iii) the investigation of effects of conformational disorder on intramolecular reorganization energies or internal site energiesrnand (iv) the inclusion of self-consistent polarization interactions for calculation of charge energies.These methods were applied to study charge transport in amorphous phases of small molecules used in the emission layer of organic light emitting diodes (OLED).rnWhen bulky substituents are attached to an aromatic core in order to adjust energy levels or prevent crystallization, a small amount of delocalization of the frontier orbital to the substituents can increase electronic couplings between neighboring molecules. This leads to improved charge-transfer rates and, hence, larger charge-mobility. We therefore suggest using the mesomeric effect (as opposed to the inductive effect) when attaching substituents to aromatic cores, which is necessary for example in deep blue OLEDs, where the energy levels of a host molecule have to be adjusted to those of the emitter.rnFurthermore, the energy landscape for charges in an amorphous phase cannot be predicted by mesoscopic models because they approximate the realistic morphology by a lattice and represent molecular charge distributions in a multipole expansion. The microscopic approach shows that a polarization-induced stabilization of a molecule in its charged and neutral states can lead to large shifts, broadening, and traps in the distribution of charge energies. These results are especially important for multi-component systems (the emission layer of an OLED or the donor-acceptor interface of an organic solar cell), if the change in polarizability upon charging (or excitation in case of energy transport) is different for the components. Thus, the polarizability change upon charging or excitation should be added to the set of molecular parameters essential for understanding charge and energy transport in organic semiconductors.rnWe also studied charge transport in self-assembled systems, where intermolecular packing motives induced by side chains can increase electronic couplings between molecules. This leads to larger charge mobility, which is essential to improve devices such as organic field effect transistors, where low carrier mobilities limit the switching frequency.rnHowever, it is not sufficient to match the average local molecular order induced by the sidernchains (such as the pitch angle between consecutive molecules in a discotic mesophase) with maxima of the electronic couplings.rnIt is also important to make the corresponding distributions as narrow as possible compared to the window determined by the closest minima of thernelectronic couplings. This is especially important in one-dimensional systems, where charge transport is limited by the smallest electronic couplings.rnThe immediate implication for compound design is that the side chains should assist the self-assemblingrnprocess not only via soft entropic interactions, but also via stronger specific interactions, such as hydrogen bonding.rnrnrnrn

Studio di componenti commerciali per sensing induttivo

Questa tesi ha lo scopo di indagare un particolare circuito commerciale che può connettersi con un sensore induttivo: l'LDC1000. Vi sono elencate e spiegate tutte le caratteristiche e le modalità di funzionamento con i link dove è possibile scaricare tutta la documentazione ufficiale del costruttore

Two ways to common knowledge

It is not clear what a system for evidence-based common knowledge should look like if common knowledge is treated as a greatest fixed point. This paper is a preliminary step towards such a system. We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge. As an alternative, we study two different deductive systems for the logic of common knowledge. The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory. We show the soundness and completeness for both systems.

I want to be my own person: the meaning-making and psychosocial processes of legacy students at Bucknell University

This study examined the meaning-making and psychosocial processes of five female legacy students at Bucknell University, each of whom having had at least one parent graduate from the institution. With a research philosophy, design, and methodology rooted in qualitative inquiry and phenomenology, inductive data analysis led to three primary categories that underscored legacy identity development. The first, Paradox of Influence and Identity, revealed through six themes nuanced experiences of separation-individuation. Second, Teaching and Learning, comprised of five themes, illuminated the impact of family — and of Bucknell parent alumni in particular — on their children’s internal working models. Lastly, Bucknell — the Environmental Contextand the five themes grouped therein highlighted the contributions of University community members, and of the campus culture and climate itself, to the co-construction of psychosocial formation. A tentative outline of grounded theory was offered, which explored categorical relationships; Paradox of Influence and Identity emerged as thedominant phenomenon, informing and being reinforced by the data of Teaching and Learning and Bucknell — the Environmental Context. Provisional intervention strategies for student affairs practice, in the contexts of academics, residential life, and career development, were discussed. Further, triangulated research is needed to substantiate and evolve the findings and theoretical model of this thesis.

Periodic breathing during ascent to extreme altitude quantified by spectral analysis of the respiratory volume signal

High altitude periodic breathing (PB) shares some common pathophysiologic aspects with sleep apnea, Cheyne-Stokes respiration and PB in heart failure patients. Methods that allow quantifying instabilities of respiratory control provide valuable insights in physiologic mechanisms and help to identify therapeutic targets. Under the hypothesis that high altitude PB appears even during physical activity and can be identified in comparison to visual analysis in conditions of low SNR, this study aims to identify PB by characterizing the respiratory pattern through the respiratory volume signal. A number of spectral parameters are extracted from the power spectral density (PSD) of the volume signal, derived from respiratory inductive plethysmography and evaluated through a linear discriminant analysis. A dataset of 34 healthy mountaineers ascending to Mt. Muztagh Ata, China (7,546 m) visually labeled as PB and non periodic breathing (nPB) is analyzed. All climbing periods within all the ascents are considered (total climbing periods: 371 nPB and 40 PB). The best crossvalidated result classifying PB and nPB is obtained with Pm (power of the modulation frequency band) and R (ratio between modulation and respiration power) with an accuracy of 80.3% and area under the receiver operating characteristic curve of 84.5%. Comparing the subjects from 1(st) and 2(nd) ascents (at the same altitudes but the latter more acclimatized) the effect of acclimatization is evaluated. SaO(2) and periodic breathing cycles significantly increased with acclimatization (p-value < 0.05). Higher Pm and higher respiratory frequencies are observed at lower SaO(2), through a significant negative correlation (p-value < 0.01). Higher Pm is observed at climbing periods visually labeled as PB with > 5 periodic breathing cycles through a significant positive correlation (p-value < 0.01). Our data demonstrate that quantification of the respiratory volume signal using spectral analysis is suitable to identify effects of hypobaric hypoxia on control of breathing.