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.

Equality and Monodic First-Order Temporal Logic

It has been shown recently that monodic first-order temporal logic without functional symbols but with equality is incomplete, i.e., the set of the valid formulae of this logic is not recursively enumerable. In this paper we show that an even simpler fragment consisting of monodic monadic two-variable formulae is not recursively enumerable.

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.

Herbrand's Theorem and Equational Reasoning: Problems and Solutions

The famous Herbrand's theorem of mathematical logic plays an important role in automated theorem proving. In the first part of this article, we recall the theorem and formulate a number of natural decision problems related to it. Somewhat surprisingly, these problems happen to be equivalent. One of these problems is the so-called simultaneous rigid E-unification problem. In the second part, we survey recent result on the simultaneous rigid E-unification problem.

On the EA-style integrated processing of self-contained mathematical texts

A sound and complete first-order goal-oriented sequent-type calculus is developed with ``large-block'' inference rules. In particular, the calculus contains formal analogues of such natural proof-search techniques as handling definitions and applying auxiliary propositions.

Kanger's Choices in Automated Reasoning

This article explains these choices and their place in modern automated deduction.

Evidence Algorithm and Processing Formalized Mathematical Texts

The goal of a research programme Evidence Algorithm is a development of an open system of automated proving that is able to accumulate mathematical knowledge and to prove theorems in a context of a self-contained mathematical text. By now, the first version of such a system called a System for Automated Deduction, SAD, is implemented in software. The system SAD possesses the following main features: mathematical texts are formalized using a specific formal language that is close to a natural language of mathematical publications; a proof search is based on special sequent-type calculi formalizing natural reasoning style, such as application of definitions and auxiliary propositions. These calculi also admit a separation of equality handling from deduction that gives an opportunity to integrate logical reasoning with symbolic calculation.

Non-asymptotic confidence bounds for the optimal value of a stochastic program

We discuss a general approach to building non-asymptotic confidence bounds for stochastic optimization problems. Our principal contribution is the observation that a Sample Average Approximation of a problem supplies upper and lower bounds for the optimal value of the problem which are essentially better than the quality of the corresponding optimal solutions. At the same time, such bounds are more reliable than “standard” confidence bounds obtained through the asymptotic approach. We also discuss bounding the optimal value of MinMax Stochastic Optimization and stochastically constrained problems. We conclude with a small simulation study illustrating the numerical behavior of the proposed bounds.

Perspectivas de la cooperación industrial entre los países miembros del CAME y los países de América Latina

Incluye Bibliografía

Mundo da vida e intersubjetividade linguística à luz da teoria evolutiva de Habermas

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Pax6 is essential for establishing ventral-dorsal cell boundaries in pituitary gland development

Pax6, a highly conserved member of the paired homeodomain transcription factor family that plays essential roles in ocular, neural, and pancreatic development and effects asymmetric transient dorsal expression during pituitary development, with its expression extinguished before the ventral → dorsal appearance of specific cell types. Analysis of pituitary development in the Small eye and Pax6 −/− mouse mutants reveals that the dorsoventral axis of the pituitary gland becomes ventralized, with dorsal extension of the transcriptional determinants of ventral cell types, particularly PFrk. This ventralization is followed by a marked decrease in terminally differentiated dorsal somatotrope and lactotrope cell types and a marked increase in the expression of markers of the ventral thyrotrope cells and SF-1-expressing cells of gonadotrope lineage. We suggest that the transient dorsal expression of Pax6 is essential for establishing a sharp boundary between dorsal and ventral cell types, based on the inhibition of Shh ventral signals.

Tbx19, a tissue-selective regulator of POMC gene expression

Pituitary cell types arise in a temporally and spatially specific fashion, in response to combinatorial actions of transcription factors induced by transient signaling gradients. The critical transcriptional determinants of the two pituitary cell types that express the pro-opiomelanocortin (POMC) gene, the anterior lobe corticotropes, producing adrenocorticotropin, and the intermediate lobe melanotropes, producing melanocyte-stimulating hormone (MSHα), have remained unknown. Here, we report that a member of the T-box gene family, Tbx19, which is expressed only in the rostral ventral diencephalon and pituitary gland, commencing on e11.5, marks pituitary cells that will subsequently express the POMC gene and is capable of altering progression of ventral cell types and inducing adrenocorticotropin in rostral tip cells. It is suggested that Tbx19, depending on the presence of synergizing transcription factors, can activate POMC gene expression and repress the α glycoprotein subunit and thyroid-stimulating hormone β promoters.