First dynamic kinetic resolution of selenium-containing chiral amines catalyzed by palladium (Pd/BaSO(4)) and Candida antartica lipase (CAL-B)

An efficient method for chemoenzymatic dynamic kinetic resolution of selenium-containing chiral amines (organoselenium-1-phenylethanamines) has been developed, leading to the corresponding amides in excellent enantioselectivities and high isolated yields. This one-pot procedure employs two different types of catalysts: Pd on barium sulphate (Pd/BaSO(4)) as racemization catalyst and lipase (CAL-B) as the resolution catalyst. (C) 2009 Elsevier Ltd. All rights reserved.

Lipase-Catalyzed Highly Enantioselective Kinetic Resolution of Boron-Containing Chiral Alcohols

The first application of enzymes as catalysts to obtain optically pure boron compounds is described. The kinetic resolution of boron-containing chiral alcohols via enantioselective transesterification catalyzed by lipases was studied. Aromatic, allylic, and aliphatic secondary alcohols containing a boronate ester or boronic acid group were resolved by lipase from Candida antartica (CALB), and excellent E values (E > 200) and high enantiomeric excesses (up to >99%) of both remaining substrates and acetylated product were obtained.

Enzymatic kinetic resolution of organochalcogenides in supercritical CO(2)

1-(Phenylthio)-, 1-(phenylseleno)- and 1-(phenyltelluro)-propan-2-ol were efficiently resolved by CAL-B in sc-CO(2). (C) 2011 Elsevier Ltd. All rights reserved.

Kinetic resolution of iodophenylethanols by Candida antarctica lipase and their application for the synthesis of chiral biphenyl compounds

The kinetic resolution of (+/-)-iodophenylethanols was carried out using lipase from Candida antarctica and in some cases the enantiomeric excesses were high (up to >98%). Enantiomerically enriched (S)-iodophenylethanols produced by the enzymatic resolution process were used in the synthesis of chiral biphenyl compounds by the Suzuki reaction with good yields (63-65%). (C) 2010 Elsevier Ltd. All rights reserved.

Limits to phase resolution in matter-wave interferometry

We study the quantum dynamics of a two-mode Bose-Einstein condensate in a time-dependent symmetric double-well potential using analytical and numerical methods. The effects of internal degrees of freedom on the visibility of interference fringes during a stage of ballistic expansion are investigated varying particle number, nonlinear interaction sign and strength, as well as tunneling coupling. Expressions for the phase resolution are derived and the possible enhancement due to squeezing is discussed. In particular, the role of the superfluid-Mott insulator crossover and its analog for attractive interactions is recognized.

Monodic temporal resolution

Until recently, First-Order Temporal Logic (FOTL) has been only partially understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a breakthrough by Hodkinson et al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for this monodic fragment.In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for monodic formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL can be established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.

Mechanising first-order temporal resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. Although a complete and correct resolution-style calculus has already been suggested for this specific fragment, this calculus involves constructions too complex to be of practical value. In this paper, we develop a machine-oriented clausal resolution method which features radically simplified proof search. We first define a normal form for monodic formulae and then introduce a novel resolution calculus that can be applied to formulae in this normal form. By careful encoding, parts of the calculus can be implemented using classical first-order resolution and can, thus, be efficiently implemented. We prove correctness and completeness results for the calculus and illustrate it on a comprehensive example. An implementation of the method is briefly discussed.

Monodic Temporal Resolution

First-order temporal logic is a coincise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness result, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.

Handling Equality in Monodic Temporal Resolution

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments including the guarded fragment with equality. In this paper, we specialise the monodic resolution method to the guarded monodic fragment with equality and first-order temporal logic over expanding domains. We introduce novel resolution calculi that can be applied to formulae in the normal form associated with the clausal resolution method, and state correctness and completeness results.

Towards the Implementation of First-Order Temporal Resolution: the Expanding Domain Case

First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics has identified important enumerable and even decidable fragments. In this paper, we develop a clausal resolution method for the monodic fragment of first-order temporal logic over expanding domains. We first define a normal form for monodic formulae and then introduce novel resolution calculi that can be applied to formulae in this normal form. We state correctness and completeness results for the method. We illustrate the method on a comprehensive example. The method is based on classical first-order resolution and can, thus, be efficiently implemented.

Stratified resolution

We introduce a calculus of stratified resolution, in which special attention is paid to clauses that "define" relations. If such clauses are discovered in the initial set of clauses, they are treated using the rule of definition unfolding, i.e. the rule that replaces defined relations by their definitions. Stratified resolution comes with a powerful notion of redundancy: a clause to which definition unfolding has been applied can be removed from the search space. To prove the completeness of stratified resolution with redundancies, we use a novel combination of Bachmair and Ganzingerâ??s model construction technique and a hierarchical construction of orderings and least fixpoints.

Searching for Invariants Using Temporal Resolution

In this paper, we show how the clausal temporal resolution technique developed for temporal logic provides an effective method for searching for invariants, and so is suitable for mechanising a wide class of temporal problems. We demonstrate that this scheme of searching for invariants can be also applied to a class of multi-predicate induction problems represented by mutually recursive definitions. Completeness of the approach, examples of the application of the scheme, and overview of the implementation are described.

A Simplified Clausal Resolution Procedure for Propositional Linear-Time Temporal Logic

The clausal resolution method for propositional linear-time temporal logic is well known and provides the basis for a number of temporal provers. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules. In this paper, we show how the normal form can be radically simplified, and consequently, how a simplified clausal resolutioin method can be defined for this impoprtant variety of logics.