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.

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.

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.

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.

Towards First-Order Temporal Resolution

In this paper we show how to extend clausal temporal resolution to the ground eventuality fragment of monodic first-order temporal logic, which has recently been introduced by Hodkinson, Wolter and Zakharyaschev. While a finite Hilbert-like axiomatization of complete monodic first order temporal logic was developed by Wolter and Zakharyaschev, we propose a temporal resolution-based proof system which reduces the satisfiability problem for ground eventuality monodic first-order temporal formulae to the satisfiability problem for formulae of classical first-order logic.

Screening The Life Cycle Of Schistosoma Mansoni Using High-resolution Mass Spectrometry.

Schistosomiasis is a common tropical disease caused by Schistosoma species Schistosomiasis' pathogenesis is known to vary according to the worms' strain. Moreover, high parasitical virulence is directly related to eggs release and granulomatous inflammation in the host's organs. This virulence might be influenced by different classes of molecules, such as lipids. Therefore, better understanding of the metabolic profile of these organisms is necessary, especially for an increased potential of unraveling strain virulence mechanisms and resistance to existing treatments. In this report, direct-infusion electrospray high-resolution mass spectrometry (ESI(+)-HRMS) along with the lipidomic platform were employed to rapidly characterize and differentiate two Brazilian S. mansoni strains (BH and SE) in three stages of their life cycle: eggs, miracidia and cercariae, with samples from experimental animals (Swiss/SPF mice). Furthermore, urine samples of the infected and uninfected mice were analyzed to assess the possibility of direct diagnosis. All samples were differentiated using multivariate data analysis, PCA, which helped electing markers from distinct lipid classes; phospholipids, diacylglycerols and triacylglycerols, for example, clearly presented different intensities in some stages and strains, as well as in urine samples. This indicates that biochemical characterization of S. mansoni may help narrowing-down the investigation of new therapeutic targets according to strain composition and aggressiveness of disease. Interestingly, lipid profile of infected mice urine varies when compared to control samples, indicating that direct diagnosis of schistosomiasis from urine may be feasible.

High-resolution Transcript Profiling Of The Atypical Biotrophic Interaction Between Theobroma Cacao And The Fungal Pathogen Moniliophthora Perniciosa.

Witches' broom disease (WBD), caused by the hemibiotrophic fungus Moniliophthora perniciosa, is one of the most devastating diseases of Theobroma cacao, the chocolate tree. In contrast to other hemibiotrophic interactions, the WBD biotrophic stage lasts for months and is responsible for the most distinctive symptoms of the disease, which comprise drastic morphological changes in the infected shoots. Here, we used the dual RNA-seq approach to simultaneously assess the transcriptomes of cacao and M. perniciosa during their peculiar biotrophic interaction. Infection with M. perniciosa triggers massive metabolic reprogramming in the diseased tissues. Although apparently vigorous, the infected shoots are energetically expensive structures characterized by the induction of ineffective defense responses and by a clear carbon deprivation signature. Remarkably, the infection culminates in the establishment of a senescence process in the host, which signals the end of the WBD biotrophic stage. We analyzed the pathogen's transcriptome in unprecedented detail and thereby characterized the fungal nutritional and infection strategies during WBD and identified putative virulence effectors. Interestingly, M. perniciosa biotrophic mycelia develop as long-term parasites that orchestrate changes in plant metabolism to increase the availability of soluble nutrients before plant death. Collectively, our results provide unique insight into an intriguing tropical disease and advance our understanding of the development of (hemi)biotrophic plant-pathogen interactions.

Profile Of Phenolic Compounds Of Brazilian Virgin Olive Oils By Rapid Resolution Liquid Chromatography Coupled To Electrospray Ionisation Time-of-flight Mass Spectrometry (rrlc-esi-tof-ms).

In recent years, agronomical researchers began to cultivate several olive varieties in different regions of Brazil to produce virgin olive oil (VOO). Because there has been no reported data regarding the phenolic profile of the first Brazilian VOO, the aim of this work was to determine phenolic contents of these samples using rapid-resolution liquid chromatography coupled to electrospray ionisation time-of-flight mass spectrometry. 25 VOO samples from Arbequina, Koroneiki, Arbosana, Grappolo, Manzanilla, Coratina, Frantoio and MGS Mariense varieties from three different Brazilian states and two crops were analysed. It was possible to quantify 19 phenolic compounds belonging to different classes. The results indicated that Brazilian VOOs have high total phenolic content because the values were comparable with those from high-quality VOOs produced in other countries. VOOs from Coratina, Arbosana and Grappolo presented the highest total phenolic content. These data will be useful in the development and improvement of Brazilian VOO.

Application Of Laser Microdissection Icp-ms For High Resolution Elemental Mapping In Mouse Brain Tissue: A Comparative Study With Laser Ablation Icp-ms.

Mapping of elements in biological tissue by laser induced mass spectrometry is a fast growing analytical methodology in life sciences. This method provides a multitude of useful information of metal, nonmetal, metalloid and isotopic distribution at major, minor and trace concentration ranges, usually with a lateral resolution of 12-160 µm. Selected applications in medical research require an improved lateral resolution of laser induced mass spectrometric technique at the low micrometre scale and below. The present work demonstrates the applicability of a recently developed analytical methodology - laser microdissection associated to inductively coupled plasma mass spectrometry (LMD ICP-MS) - to obtain elemental images of different solid biological samples at high lateral resolution. LMD ICP-MS images of mouse brain tissue samples stained with uranium and native are shown, and a direct comparison of LMD and laser ablation (LA) ICP-MS imaging methodologies, in terms of elemental quantification, is performed.

High resolution study of 104Pd(d,t)103Pd

Information collected in the present high resolution study of 104Pd(d,t)103Pd is interpreted within the systematics of the A ~ 100 region. The paper complements data previously presented by the S.Paulo Group, which were taken with the Pelletron-Enge-Spectrograph facility. A one-to-one correspondence to gamma ray results for 103Pd, collected by the Nuclear Data Sheets (NDS), was achieved and at least four open questions were settled. More reliable spectroscopic strengths were extracted in the present study.

Enzymatic kinetic resolution of (RS)-1-(Phenyl)ethanols by Burkholderia cepacia lipase immobilized on magnetic nanoparticles

Lipase from Burkholderia cepacia immobilized on superparamagnetic nanoparticles using adsorption and chemisorption methodologies was efficiently applied as recyclable biocatalyst in the enzymatic kinetic resolution of (RS)-1-(phenyl)ethanols via transesterification reactions. (R)-Esters and the remaining (S)-alcohols were obtained with excellent enantiomeric excess (> 99%), which corresponds to a perfect process of enzymatic kinetic resolution (conversion 50%, E > 200). The transesterification reactions catalysed with B. cepacia lipase immobilized by the glutaraldehyde method showed the best results in terms of reusability, preserving the enzyme activity (conversion 50%, E > 200) for at least 8 successive cycles.

Sudan Black B treatment reduces autofluorescence and improves resolution of in situ hybridization specific fluorescent signals of brain sections

Interference by autofluorescence is one of the major concerns of immunofluorescence analysis of in situ hybridization-based diagnostic assays. We present a useful technique that reduces autofluorescent background without affecting the tissue integrity or direct immunofluorescence signals in brain sections. Using six different protocols, such as ammonia/ethanol, Sudan Black B (SBB) in 70% ethanol, photobleaching with UV light and different combinations of them in both formalin-fixed paraffin-embedded and frozen human brain tissue sections, we have found that tissue treatment of SBB in a concentration of 0.1% in 70% ethanol is the best approach to reduce/eliminate tissue autofluorescence and background, while preserving the specific fluorescence hybridization signals. This strategy is a feasible, non-time consuming method that provides a reasonable compromise between total reduction of the tissue autofluorescence and maintenance of specific fluorescent labels.

High spatial resolution spectroscopy of W51IRS 2E and IRS 2W: Two very massive young stars in early formation stages

We present K-band spectra of the near infrared counterparts to IRS 2E and IRS 2W which is associated with the ultracompact H II region W51d, both of them embedded sources in the Galactic compact H II region W51 IRS 2. The high spatial resolution observations were obtained with the laser guide star facility and Near-infrared Integral Field Spectrograph (NIFS) mounted at the Gemini-North observatory. The spectrum of the ionizing source of W51d shows the photospheric features N III ( 21155 angstrom) in emission and He II ( 21897 angstrom) in absorption which lead us to classify it as a young O3 type star. We detected CO overtone in emission at 23000 angstrom in the spectrum of IRS 2E, suggesting that it is a massive young object still surrounded by an accretion disk, probably transitioning from the hot core phase to an ultracompact H II region.