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.

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.

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.

Investigation of single tryptophan proteins encapsulated in TEOS-derived sol-gel matrices by fluorescence spectroscopy /

In the work reported here, optically clear, ultrathin TEOS derived sol-gel slides which were suitable for studies of tryptophan (Trp) fluorescence from entrapped proteins were prepared by the sol-gel technique and characterized. The monitoring of intrinsic protein fluorescence provided information about the structure and environment of the entrapped protein, and about the kinetics of the interaction between the entrapped protein and extemal reagents. Initial studies concentrated on the single Trp protein monellin which was entrapped into the sol-gel matrices. Two types of sol-gel slides, termed "wet aged", in which the gels were aged in buffer and "dry-aged", in which the gels were aged in air , were studied in order to compare the effect of the sol-gel matrix on the structure of the protein at different aging stages. Fluorescence results suggested that the mobility of solvent inside the slides was substantially reduced. The interaction of the entrapped protein with both neutral and charged species was examined and indicated response times on the order of minutes. In the case of the neutral species the kinetics were diffusion limited in solution, but were best described by a sum of first order rate constants when the reactions occurred in the glass matrix. For charged species, interactions between the analytes and the negatively charged glass matrix caused the reaction kinetics to become complex, with the overall reaction rate depending on both the type of aging and the charge on the analyte. The stability and conformational flexibility of the entrapped monellin were also studied. These studies indicated that the encapsulation of monellin into dry-aged monoliths caused the thermal unfolding transition to broaden and shift upward by 14°C, and causedthe long-term stability to improve by 12-fold (compared to solution). Chemical stability studies also showed a broader transition for the unfolding of the protein in dry-aged monoliths, and suggested that the protein was present in a distribution of environments. Results indicated that the entrapped proteins had a smaller range of conformational motions compared to proteins in solution, and that entrapped proteins were not able to unfold completely. The restriction of conformational motion, along with the increased structural order of the internal environment of the gels, likely resulted in the improvements in themial and long-term stability that were observed. A second protein which was also studied in this work is the metal binding protein rat oncomodulin. Initially, the unfolding behavior of this protein in aqueous solution was examined. Several single tryptophan mutants of the metal-binding protein rat oncomodulin (OM) were examined; F102W, Y57W, Y65W and the engineered protein CDOM33 which had all 12 residues of the CD loop replaced with a higher affinity binding loop. Both the thermal and the chemical stability were improved upon binding of metal ions with the order apo < Ca^^ < Tb^"^. During thermal denaturation, the transition midpoints (Tun) of Y65W appeared to be the lowest, followed by Y57W and F102W. The placement of the Trp residue in the F-helix in F102W apparently made the protein slightly more thermostable, although the fluorescence response was readily affected by chemical denaturants, which probably acted through the disruption of hydrogen bonds at the Cterminal end of the F-helix. Under both thermal and chemical denaturation, the engineered protein showed the highest stability. This indicated that increasing the number of metal ligating oxygens in the binding site, either by using a metal ion with a higher coordinatenumber (i.e. Tb^*) which binds more carboxylate ligands, or by providing more ligating groups, as in the CDOM33 replacement, produces notable improvements in protein stability. Y57W and CE)OM33 OM were chosen for further studies when encapsulated into sol-gel derived matrices. The kinetics of interaction of terbium with the entrapped proteins, the ability of the entrapped protein to binding terbium, as well as thermal stability of these two entrapped protein were compared with different levels of Ca^"*^ present in the matrix and in solution. Results suggested that for both of the proteins, the response time and the ability to bind terbium could be adjusted by adding excess calcium to the matrix before gelation. However, the less stable protein Y57W only retained at most 45% of its binding ability in solution while the more stable protein CDOM33 was able to retain 100% binding ability. Themially induced denaturation also suggested that CDOM33 showed similar stability to the protein in solution while Y57W was destabilized. All these results suggested that "hard" proteins (i.e. very stable) can easily survive the sol-gel encapsulation process, but "soft" proteins with lower thermodynamic stability may not be able to withstand the sol-gel process. However, it is possible to control many parameters in order to successfully entrap biological molecules into the sol-gel matrices with maxunum retention of activity.

The kinetics and induced decomposition on the thermal decomposition of hydroperoxides /

This project is focussed on the thermsLl decomposition of t-butyl hydroperoxide and sec-butyl hydroperoxide at 120°C to 160°C in three alcohol solvents. These are methanol, ethajiol and isopropyl alcohol. The aim of the project was to examine the process of induced decomposition. Thermal decomposition of t-hutyl hydroperoxide and sec-butyl hydroperoxide indicate that these reactions have first-order kinetics with activation energies on the order of 20 to 28 K cal/mole, Styrene was used as a free radical trap to inhibit the induced decomposition. The results permitted calculation of how much induced decomposition occurred in its absence. The experimental resvilts indicate that the induced decomposition is important for t-butyl hydroperoxide in alcohol solvents, as shown by both the reaction rate suid product studies. But sec-butyl hydroperoxide results show that the concerted mechanism for the interaction of two sec-butylperoxy radicals occurs in addition to the induced decomposition. Di-sodium E.D,T.A. was added to reduce possible effects of trace transition metal ion .impurities. The result of this experiment were not as expected. The rate of hydroperoxide decomposition was about the same but was zero-order in hydroperoxide concentration.

A study of the thermal decomposition of allyl t-butyl peroxide and 3-hydroperoxy-1-propene (allyl hydroperoxide) in toluene /|nby Krishnankutty Nair V. G. -- 260 St. Catharines [Ont. : s. n.],

Kinetics and product studies of the decompositions of allyl-t-butyl peroxide and 3-hydroperoxy- l-propene (allyl hydroperoxide ) in tolune were investigated. Decompositions of allyl-t-butyl peroxide in toluene at 130-1600 followed first order kinetics with an activation energy of 32.8 K.cals/mol and a log A factor of 13.65. The rates of decomposition were lowered in presence of the radical trap~methyl styrene. By the radical trap method, the induced decomposition at 1300 is shown to be 12.5%. From the yield of 4-phenyl-l,2- epoxy butane the major path of induced decomposition is shown to be via an addition mechanism. On the other hand, di-t-butYl peroxyoxalate induced decomposition of this peroxide at 600 proceeded by an abstraction mechanism. Induced decomposition of peroxides and hydroperoxides containing the allyl system is proposed to occur mainly through an addition mechanism at these higher temperatures. Allyl hydroperoxide in toluene at 165-1850 decomposes following 3/2 order kinetics with an Ea of 30.2 K.cals per mole and log A of 10.6. Enormous production of radicals through chain branching may explain these relatively low values of E and log A. The complexity of the reaction is indicated a by the formation of various products of the decomposition. A study of the radical attack of the hydro peroxide at lower temperatures is suggested as a further work to throw more light on the nature of decomposition of this hydroperoxide.

Kinetic and mechanistic studies for the molybdenum- catalyzed oxidation of organic sulfides and olefins by t- DuO2H

This research was focussed on the effects of light, solvent and substituents in the molybdenum-catalyzed oxidation of phenylmethyl sulfides with t-Bu02H and on the effect of light in the molybdenum-catalyzed epoxidation of l-octene with t-Bu02H. It was shown that the Mo(CO)6-catalyzed oxidation of phenylmethyl sulfide with t-Bu02H~ at 35°C, proceeds 278 times faster underUV light than under laboratory lighting, whereas the Mo02(acac)2-catalyzed oxidation proceeds only 1.7 times faster under UV light than under normal laboratory lighting. The difference between the activities of both catalysts was explained by the formation of the catalytically active species, Mo(VI). The formation of the Mo(VI) species, from Mo(CO)6 was observed from the IR spectrum of Mo(CO)6 in the carbonyl region. The Mo(CO)6-catalyzed epoxidation of l-octene with t-Bu02H showed that the reaction proceeded 4.6 times faster under UV light than in the dark or under normal laboratory lighting; the rates of epoxidations were found to be the same in the dark and under normal laboratory lighting. The kinetics of the epoxidations of l-octene with t-Bu02H, catalyzed by Mo02(acac)2 were found to be complicated; after fast initial rates, the epoxidation rates decreased with time. The effect of phenylmethyl sulfide on the Mo(CO)6-catalyzed epoxidation of l-octene waS studied. It was shown that instead of phenylmethyl sulfide, phenylmethyl sulfone, which formed rapidly at 85°C, lowered the reaction rate. The epoxidation of l-octene was found to be 2.5 times faster in benzene than in ethanol. The substituent effect on the Mo02(acac)2-catalyzed oxidations of p-OH, p-CHgO, P-CH3' p-H, p-Cl, p-Br, p-CHgCO, p-HCO and P-N02 substituted phenylmethyl sulfides were studied. The oxidations followed second order kinetics for each case; first order dependency on catalyst concentration was also observed in the oxidation of p-CHgOPhSMeand PhSMe. It was found that electron-donating groups on the para position of phenylmethyl sulfide increased the rate of reaction, while electronwithdrawing groups caused the reaction rate to decrease. The reaction constants 0 were determined by using 0, 0- and 0* constants. The rate effects were paralleled by the activation energies for oxidation. The decomposition of t-Bu02H in the presence of M.o (CO)6, Mo02 (acac)2 and VO(acac)2 was studied. The rates of decomposition were found to be very small compared to the oxidation rates at high concentration of catalysis. The relative rates of the Mo02(acac)2-catalyzed oxidation of p-N02PhSMe by t-Bu02H in the presence of either p-CH30PhSMe or PhSMe clearly show that PhSMe and p-CHgOPhSMe act as co-catalysts in the oxidation of p-N02PhSMe. Benzene, mesity1ene and cyclohexane were used to determine the effect of solvent in the Mo02 (acac)2 and Mo(CO)6-catalyzed oxidation of phenylmethyl sulfide. The results showed that in the absence of hydroxylic solvent, a second molecule of t-Bu02H was involved in the transition state. The complexation of the solvent with the catalyst could not be explained.The oxidations of diphenyl sulfoxide catalyzed by VO(acac)2, Mo(CO)6 and Mo02(acac)2 showed that VO(acac)2 catalyzed the oxidation faster than Mo(CO)6 and Mo02 (acac)2_ Moreover, the Mo(CO)6-catalyzed oxidation of diphenyl sulfoxide proceeded under UV light at 35°C.

The determination of sinigrin in Brassica, and investigations into the use of allyl-isothiocyanate as a nematicide

The goal of this thesis was to study factors related to the development of Brassica juncea as a sustainable nematicide. Brassica juncea is characterized by the glycoside (glucosinolate) sinigrin. Various methods were developed for the determination of sinigrin in Brassica juncea tissue extracts. Sinigrin concentrations in plant tissues at various stages of growth were monitored. Sinigrin enzymatically breaks down into allylisothiocyanate (AITC). AITC is unstable in aqueous solution and degradation was studied in water and in soil. Finally, the toxicity of AITC against the root-lesion nematode (Pratylenchus penetrans) was determined. A method was developed to extract sinigrin from whole Brassica j uncea tissues. The optimal time of extraction wi th boiling phosphate buffer (0.7mM, pH=6.38) and methanol/water (70:30 v/v) solutions were both 25 minutes. Methanol/water extracted 13% greater amount of sinigrin than phosphate buffer solution. Degradation of sinigrin in boiling phosphate buffer solution (0.13%/minute) was similar to the loss of sinigrin during the extraction procedure. The loss of sinigrin from boiling methanol/water was estimated to be O.Ol%/minute. Brassica juncea extract clean up was accomplished by an ion-pair solid phase extraction (SPE) method. The recovery of sinigrin was 92.6% and coextractive impurities were not detected in the cleaned up extract. Several high performance liquid chromatography (HPLC) methods were developed for the determination of sinigrin. All the developed methods employed an isocratic mobile phase system wi th a low concentration of phosphate buffer solution, ammonium acetate solution or an ion-pair reagent solution. A step gradient system was also developed. The method involved preconditioning the analytical column with phosphate buffer solution and then switching the mobile phase to 100% water after sample injection.Sinigrin and benzyl-glucosinolate were both studied by HPLC particle beam negative chemical ionization mass spectrometry (HPLCPB- NCI-MS). Comparison of the mass spectra revealed the presence of fragments arising from the ~hioglucose moiety and glucosinolate side-chain. Variation in the slnlgrin concentration within Brassica juncea plants was studied (Domo and Cutlass cuItivars). The sinigrin concentration in the top three leaves was studied during growth of each cultivar. For Cutlass, the minimum (200~100~g/g) and maximum (1300~200~g/g) concentrations were observed at the third and seventh week after planting, respectively. For Domo, the minimum (190~70~g/g) and maximum (1100~400~g/g) concentrations were observed at the fourth and eighth week after planting, respectively. The highest sinigrin concentration was observed in flower tissues 2050±90~g/g and 2300±100~g/g for Cutlass and Domo cultivars, respectively. Physical properties of AITC were studied. The solubility of AITC in water was determined to be approximately 1290~g/ml at 24°C. An HPLC method was developed for the separation of degradation compounds from aqueous AITC sample solutions. Some of the degradation compounds identified have not been reported in the literature: allyl-thiourea, allyl-thiocyanate and diallyl-sulfide. In water, AITC degradation to' diallyl-thiourea was favored at basic pH (9.07) and degradation to diallyl-sulfide was favored at acidic pH (4 . 97). It wap necessary to amend the aqueous AITC sample solution with acetonitrile ?efore injection into the HPLC system. The acetonitrile amendment considerably improved AITC recovery and the reproducibility of the results. The half-life of aqueous AITC degradation at room temperature did not follow first-order kinetics. Beginning with a 1084~g/ml solution, the half-life was 633 hours. Wi th an ini tial AITC concentration of 335~g/ml the half-life was 865 hours. At 35°C the half-life AITC was 76+4 hours essentially independent of the iiisolution pH over the range of pH=4.97 to 9.07 (1000~g/ml). AITC degradation was also studied in soil at 35°C; after 24 hours approximately 75% of the initial AITC addition was unrecoverable by water extraction. The ECso of aqueous AITC against the root-lesion nematode (Pratylenchus penetrans) was determined to be approximately 20~g/ml at one hour exposure of the nematode to the test solution. The toxicological study was also performed with a myrosinase treated Brassica juncea extract. Myrosinase treatment of the Brassica juncea extract gave nearly quantitative conversion of sinigrin into AITC. The myrosinase treated extract was of the same efficacy as an aqueous AITC solution of equivalent concentration. The work of this thesis was focused upon understanding parameters relevant to the development of Brassica juncea as a sustainable nematicide. The broad range of experiments were undertaken in support of a research priority at Agriculture and Agri-Food Canada.

The kinetics and solvent effects on the thermal decomposition of isopropyl peroxide and 1, 2-dioxane

Rates of H2 formation have been determined for the thermal decomposition of isopropyl peroxide at l30o-l50oC in toluene and methanol and at l400C in isopropyl alcohol and water. Product studies have been carried out at l400C in these solvents. The decomposition of isopropyl peroxide was shown to be unimolecular with energies of activation in toluene, and methanol of 39.1, 23.08 Kcal/mole respectively. It has been shown that the rates of H2 formation in decomposition of isopropyl peroxide are solvent dependent and that the ~ vs "'2';' values (parameters for solvent polarity) givesastraight line. Mechanisms for hydrogen production are discussed which satisfactorily explain the stabilization of the six-centered transition state by the solvent. One possibility is that of conformation stabilization by solvent and the other, a transition state with sufficient ionic character to be stabilized by a polar solvent. Rates of thermal decomposition of 1,2-dioxane in tert-butylbenzene at l40o-l70oC have been determined. The activation energy was found to be 33.4 Kcal/mole. This lower activation energy, compared to that for the decomposition of isopropyl peroxide in toluene (39.1 Kcal/mole) has been explained in terms of ring strain. Decomposition of 1,2 dioxane in MeOH does not follow a first order reaction. Several mechanisms have been suggested for the products observed for decomposition of 1;2-dioxane in toluene and methanol.

Generating Relation Algebras for Qualitative Spatial Reasoning

Basic relationships between certain regions of space are formulated in natural language in everyday situations. For example, a customer specifies the outline of his future home to the architect by indicating which rooms should be close to each other. Qualitative spatial reasoning as an area of artificial intelligence tries to develop a theory of space based on similar notions. In formal ontology and in ontological computer science, mereotopology is a first-order theory, embodying mereological and topological concepts, of the relations among wholes, parts, parts of parts, and the boundaries between parts. We shall introduce abstract relation algebras and present their structural properties as well as their connection to algebras of binary relations. This will be followed by details of the expressiveness of algebras of relations for region based models. Mereotopology has been the main basis for most region based theories of space. Since its earliest inception many theories have been proposed for mereotopology in artificial intelligence among which Region Connection Calculus is most prominent. The expressiveness of the region connection calculus in relational logic is far greater than its original eight base relations might suggest. In the thesis we formulate ways to automatically generate representable relation algebras using spatial data based on region connection calculus. The generation of new algebras is a two pronged approach involving splitting of existing relations to form new algebras and refinement of such newly generated algebras. We present an implementation of a system for automating aforementioned steps and provide an effective and convenient interface to define new spatial relations and generate representable relational algebras.