A System for Models of First Order Theories

If you want to know whether a property is true or not in a specific algebraic structure,you need to test that property on the given structure. This can be done by hand, which can be cumbersome and erroneous. In addition, the time consumed in testing depends on the size of the structure where the property is applied. We present an implementation of a system for finding counterexamples and testing properties of models of first-order theories. This system is supposed to provide a convenient and paperless environment for researchers and students investigating or studying such models and algebraic structures in particular. To implement a first-order theory in the system, a suitable first-order language.( and some axioms are required. The components of a language are given by a collection of variables, a set of predicate symbols, and a set of operation symbols. Variables and operation symbols are used to build terms. Terms, predicate symbols, and the usual logical connectives are used to build formulas. A first-order theory now consists of a language together with a set of closed formulas, i.e. formulas without free occurrences of variables. The set of formulas is also called the axioms of the theory. The system uses several different formats to allow the user to specify languages, to define axioms and theories and to create models. Besides the obvious operations and tests on these structures, we have introduced the notion of a functor between classes of models in order to generate more co~plex models from given ones automatically. As an example, we will use the system to create several lattices structures starting from a model of the theory of pre-orders.

Simultaneous extraction of order parameters and orientational distribution fuctions from 31[superscript]P NMR spectra of magnetically partially oriented phospholipid bilayers

Order parameter profiles extracted from the NMR spectra of model membranes are a valuable source of information about their structure and molecular motions. To al1alyze powder spectra the de-Pake-ing (numerical deconvolution) ~echnique can be used, but it assumes a random (spherical) dist.ribution of orientations in the sample. Multilamellar vesicles are known to deform and orient in the strong magnetic fields of NMR magnets, producing non-spherical orientation distributions. A recently developed technique for simultaneously extracting the anisotropies of the system as well as the orientation distributions is applied to the analysis of partially magnetically oriented 31p NMR spectra of phospholipids. A mixture of synthetic lipids, POPE and POPG, is analyzed to measure distortion of multilamellar vesicles in a magnetic field. In the analysis three models describing the shape of the distorted vesicles are examined. Ellipsoids of rotation with a semiaxis ratio of about 1.14 are found to provide a good approximation of the shape of the distorted vesicles. This is in reasonable agreement with published experimental work. All three models yield clearly non-spherical orientational distributions, as well as a precise measure of the anisotropy of the chemical shift. Noise in the experimental data prevented the analysis from concluding which of the three models is the best approximation. A discretization scheme for finding stability in the algorithm is outlined

Extending relAPS to first order logic

RelAPS is an interactive system assisting in proving relation-algebraic theorems. The aim of the system is to provide an environment where a user can perform a relation-algebraic proof similar to doing it using pencil and paper. The previous version of RelAPS accepts only Horn-formulas. To extend the system to first order logic, we have defined and implemented a new language based on theory of allegories as well as a new calculus. The language has two different kinds of terms; object terms and relational terms, where object terms are built from object constant symbols and object variables, and relational terms from typed relational constant symbols, typed relational variables, typed operation symbols and the regular operations available in any allegory. The calculus is a mixture of natural deduction and the sequent calculus. It is formulated in a sequent style but with exactly one formula on the right-hand side. We have shown soundness and completeness of this new logic which verifies that the underlying proof system of RelAPS is working correctly.

Genetic programming for the RoboCup Rescue Simulation System

The Robocup Rescue Simulation System (RCRSS) is a dynamic system of multi-agent interaction, simulating a large-scale urban disaster scenario. Teams of rescue agents are charged with the tasks of minimizing civilian casualties and infrastructure damage while competing against limitations on time, communication, and awareness. This thesis provides the first known attempt of applying Genetic Programming (GP) to the development of behaviours necessary to perform well in the RCRSS. Specifically, this thesis studies the suitability of GP to evolve the operational behaviours required of each type of rescue agent in the RCRSS. The system developed is evaluated in terms of the consistency with which expected solutions are the target of convergence as well as by comparison to previous competition results. The results indicate that GP is capable of converging to some forms of expected behaviour, but that additional evolution in strategizing behaviours must be performed in order to become competitive. An enhancement to the standard GP algorithm is proposed which is shown to simplify the initial search space allowing evolution to occur much quicker. In addition, two forms of population are employed and compared in terms of their apparent effects on the evolution of control structures for intelligent rescue agents. The first is a single population in which each individual is comprised of three distinct trees for the respective control of three types of agents, the second is a set of three co-evolving subpopulations one for each type of agent. Multiple populations of cooperating individuals appear to achieve higher proficiencies in training, but testing on unseen instances raises the issue of overfitting.

Competing demands for a complex system : photosystem II repair, photoprotection and quantum yield

Photosynthesis in general is a key biological process on Earth and Photo system II (PSII) is an important component of this process. PSII is the only enzyme capable of oxidizing water and is largely responsible for the primordial build-up and present maintenance of the oxygen in the atmosphere. This thesis endeavoured to understand the link between structure and function in PSII with special focus on primary photochemistry, repair/photodamage and spectral characteristics. The deletion of the PsbU subunit ofPSII in cyanobacteria caused a decoupling of the Phycobilisomes (PBS) from PSII, likely as a result of increased rates of PSII photodamage with the PBS decoupling acting as a measure to protect PSII from further damage. Isolated fractions of spinach thylakoid membranes were utilized to characterize the heterogeneity present in the various compartments of the thylakoid membrane. It was found that the pooled PSIILHCII pigment populations were connected in the grana stack and there was also a progressive decrease in the reaction rates of primary photochemistry and antennae size of PSII as the sample origin moved from grana to stroma. The results were consistent with PSII complexes becoming damaged in the grana and being sent to the stroma for repair. The dramatic quenching of variable fluorescence and overall fluorescent yield of PSII in desiccated lichens was also studied in order to investigate the mechanism by which the quenching operated. It was determined that the source of the quenching was a novel long wavelength emitting external quencher. Point mutations to amino acids acting as ligands to chromophores of interest in PSII were utilized in cyanobacteria to determine the role of specific chromophores in energy transfer and primary photochemistry. These results indicated that the Hl14 ligated chlorophyll acts as the 'trap' chlorophyll in CP47 at low temperature and that the Q130E mutation imparts considerable changes to PSII electron transfer kinetics, essentially protecting the complex via increased non-radiative charge Photosynthesis in general is a key biological process on Earth and Photo system II (PSII) is an important component of this process. PSII is the only enzyme capable of oxidizing water and is largely responsible for the primordial build-up and present maintenance of the oxygen in the atmosphere. This thesis endeavoured to understand the link between structure and function in PSII with special focus on primary photochemistry, repair/photodamage and spectral characteristics. The deletion of the PsbU subunit ofPSII in cyanobacteria caused a decoupling of the Phycobilisomes (PBS) from PSII, likely as a result of increased rates of PSII photodamage with the PBS decoupling acting as a measure to protect PSII from further damage. Isolated fractions of spinach thylakoid membranes were utilized to characterize the heterogeneity present in the various compartments of the thylakoid membrane. It was found that the pooled PSIILHCII pigment populations were connected in the grana stack and there was also a progressive decrease in the reaction rates of primary photochemistry and antennae size of PSII as the sample origin moved from grana to stroma. The results were consistent with PSII complexes becoming damaged in the grana and being sent to the stroma for repair. The dramatic quenching of variable fluorescence and overall fluorescent yield of PSII in desiccated lichens was also studied in order to investigate the mechanism by which the quenching operated. It was determined that the source of the quenching was a novel long wavelength emitting external quencher. Point mutations to amino acids acting as ligands to chromophores of interest in PSII were utilized in cyanobacteria to determine the role of specific chromophores in energy transfer and primary photochemistry. These results indicated that the Hl14 ligated chlorophyll acts as the 'trap' chlorophyll in CP47 at low temperature and that the Q130E mutation imparts considerable changes to PSII electron transfer kinetics, essentially protecting the complex via increased non-radiative charge.

An Interactive Theorem Prover for First-Order Dynamic Logic

Dynamic logic is an extension of modal logic originally intended for reasoning about computer programs. The method of proving correctness of properties of a computer program using the well-known Hoare Logic can be implemented by utilizing the robustness of dynamic logic. For a very broad range of languages and applications in program veri cation, a theorem prover named KIV (Karlsruhe Interactive Veri er) Theorem Prover has already been developed. But a high degree of automation and its complexity make it di cult to use it for educational purposes. My research work is motivated towards the design and implementation of a similar interactive theorem prover with educational use as its main design criteria. As the key purpose of this system is to serve as an educational tool, it is a self-explanatory system that explains every step of creating a derivation, i.e., proving a theorem. This deductive system is implemented in the platform-independent programming language Java. In addition, a very popular combination of a lexical analyzer generator, JFlex, and the parser generator BYacc/J for parsing formulas and programs has been used.

Methoxypyrazine removal in grape juice: Development of a removal system using odorant and pheromone binding proteins coupled with bentonite fining

Multicoloured Asian Lady Beetles (MALB) and 7-spot Lady Beetles that infect vineyards can secrete alkyl-methoxypyrazines when they are processed with the grapes, resulting in wines containing a taint. The main methoxypyrazine associated with this taint is 3-isopropyl-2-methoxypyrazine (IPMP). The wines are described as having aroma and flavours of peanut butter, peanut shells, asparagus and earthy which collectively, have become known as “ladybug taint”. To date, there are no known fining agents used commercially added to juice or wine that are effective in removing this taint. The goal of this project was to use previously identified proteins with an ability to bind to methoxypyrazines at low pH, and subsequently develop a binding assay to test the ability of these proteins to bind to and remove methoxypyrazines from grape juice. The piglet odorant binding protein (plOBP) and mouse major urinary protein (mMUP) were identified, cloned and expressed in the Pichia pastoris expression system. Protein expression was induced using methanol and the proteins were subsequently purified from the induction media using anion exchange chromatography. The purified proteins were freeze-dried and rehydrated prior to use in the methoxypyrazine removal assay. The expression and purification system resulted in yields of approximately 78% of purified plOBP and 62% of purified mMUP from expression to rehydration. Purified protein values were 87 mg of purified plOPB per litre of induction media and 19 mg of purified mMUP per litre of induction medium. In order to test the ability of the protein to bind to the MPs, an MP removal assay was developed. In the assay, the purified protein is incubated with either IPMP or 3-isobutyl-2-methoxypyrazine (IBMP) for two hours in either buffer or grape juice. Bentonite is then used to capture the protein-MP complex and the bentonite-protein-MP complex is then removed from solution by filtration. Residual MP is measured in solution following the MP removal assay and compared to that in the starting solution by Gas Chromatography Mass Spectrometry (GC/MS). GC/MS results indicated that the mMUP was capable of removing IBMP and IPMP from 300 ng/L in buffer pH 4.0, buffer pH 3.5 and Riesling Juice pH 3.5 down to the limit of quantification of the instrument, which is 6ng/L and 2ng/L for IBMP and IPMP, respectively. The results for the plOBP showed that although it could remove some IBMP, it was only approximately 50-70 ng/L more than bentonite treatment followed by filtration, resulting in approximately 100 ng/L of the MPs being left in solution. pIOBP was not able to remove IPMP in buffer pH 3.5 using this system above that removed by bentonite alone. As well, the pIOBP was not able to remove any additional MPs from Chardonnay juice pH 3.5 above that already removed by the bentonite and filtration alone. The mouse MUP was shown to be a better candidate protein for removal of MPs from juice using this system.

Cell-selective modulation of the neuromuscular system in Drosophila

The capacity for all living cells to sense and interact with their environment is a necessity for life. In highly evolved, eukaryotic species, like humans, signalling mechanisms are necessary to regulate the function and survival of all cells in the organism. Synchronizing systemic signalling systems at the cellular, organ and whole-organism level is a formidable task, and for most species requires a large number of signalling molecules and their receptors. One of the major types of signalling molecules used throughout the animal kingdom are modulatory substances (e.x. hormones and peptides). Modulators can act as chemical transmitters, facilitating communication at chemical synapses. There are hundreds of circulating modulators within the mammalian system, but the reason for so many remains a mystery. Recent work with the fruit fly, Drosophila melanogaster demonstrated the capacity for peptides to modulate synaptic transmission in a neuron-specific manner, suggesting that peptides are not simply redundant, but rather may have highly specific roles. Thus, the diversity of peptides may reflect cell-specific functions. The main objective of my doctoral thesis was to examine the extent to which neuromodulator substances and their receptors modulate synaptic transmission at a cell-specific level using D. melanogaster. Using three different modulatory substances, i) octopamine - a biogenic amine released from motor neuron terminals, ii) DPKQDFMRFa - a neuropeptide secreted into circulation, and iii) Proctolin - a pentapeptide released both from motor neuron terminals and into circulation, I was able to investigate not only the capacity of these various substances to work in a cell-selective manner, but also examine the different mechanisms of action and how modulatory substances work in concert to execute systemic functionality . The results support the idea that modulatory substances act in a circuit-selective manner in the central nervous system and in the periphery in order to coordinate and synchronize physiologically and behaviourally relevant outputs. The findings contribute as to why the nervous system encodes so many modulatory substances.