Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

A factor model of seasonality in stock returns

Published as an article in: The Quarterly Review of Economics and Finance, 2004, vol. 44, issue 2, pages 224-236.

La influencia del factor dimensión en la pertenencia a centrales de compra por parte del pequeño comercio

[ES] Desde hace varios años, el pequeño comercio en España y en otros países europeos viene enfrentándose a un entorno de creciente concurrencia, con la irrupción de nuevas formas comerciales más integradas vertical u horizontalmente, y mejor preparadas para competir en precio y variedad. Ante este hecho, las centrales de compra se ofrecen como una alternativa tendente a acortar distancias en estas dos cuestiones, a la vez que buscan la prestación de ciertos servicios que ayuden al pequeño comerciante a gestionar más eficaz y eficientemente su negocio.

The reverse self-dual serial cost-sharing rule

In this study we define a cost sharing rule for cost sharing problems. This rule is related to the serial cost-sharing rule defined by Moulin and Shenker (1992). We give some formulas and axiomatic characterizations for the new rule. The axiomatic characterizations are related to some previous ones provided by Moulin and Shenker (1994) and Albizuri (2010).

Repensando la confianza como factor crítico en la gestión organizativa

[ES] La confianza en el mundo de los negocios es un factor esencial que viene siendo estudiado por la literatura del Management desde hace décadas. Partiendo de la propuesta seminal de Mayer et al. (1995), acerca de qué es la confianza y cómo se desarrolla en el seno de las organizaciones, proponemos trazar una crítica constructiva al modelo descrito a partir de las aportaciones de Spaemann, autor de dilatada trayectoria en el marco de la denominada “Filosofía Moral de la Europa Continental”.

La gestión empresarial como factor clave de desarrollo de las spin-offs universitarias. Análisis organizativo y financiero

[ES] En las últimas décadas el número de spin-offs universitarias creadas en el Sistema Universitario Español ha aumentado considerablemente; sin embargo, estas empresas tienen que hacer frente a problemas como la falta de financiación o de capacidades empresariales por parte de los fundadores. A partir de los datos extraídos de una encuesta a 72 spin-offs creadas en España, tratamos de detectar y analizar cuáles son los problemas más habituales con los que se encuentran estas empresas, y proponemos posibles vías de solución.

Multiple table factor analysis applied to the higher education competences

Due to the recent implantation of the Bologna process, the definition of competences in Higher Education is an important matter that deserves special attention and requires a detailed analysis. For that reason, we study the importance given to severa! competences for the professional activity and the degree to which these competences have been achieved through the received education. The answers include also competences observed in two periods of time given by individuals of multiple characteristics. In this context and in order to obtain synthesized results, we propose the use of Multiple Table Factor Analysis. Through this analysis, individuals are described by severa! groups, showing the most important variability factors of the individuals and allowing the analysis of the common structure ofthe different data tables. The obtained results will allow us finding out the existence or absence of a common structure in the answers of the various data tables, knowing which competences have similar answer structure in the groups of variables, as well as characterizing those answers through the individuals.

Plasma brain-derived neurotrophic factor levels, learning capacity and cognition in patients with first episode psychosis

Background: Cognitive impairments are seen in first psychotic episode (FEP) patients. The neurobiological underpinnings that might underlie these changes remain unknown. The aim of this study is to investigate whether Brain Derived Neurotrophic Factor (BDNF) levels are associated with cognitive impairment in FEP patients compared with healthy controls. Methods: 45 FEP patients and 45 healthy controls matched by age, gender and educational level were selected from the Basque Country area of Spain. Plasma BDNF levels were assessed in healthy controls and in patients. A battery of cognitive tests was applied to both groups, with the patients being assessed at 6 months after the acute episode and only in those with a clinical response to treatment. Results: Plasma BDNF levels were altered in patients compared with the control group. In FEP patients, we observed a positive association between BDNF levels at six months and five cognitive domains (learning ability,immediate and delayed memory, abstract thinking and processing speed) which persisted after controlling for medications prescribed, drug use, intelligence quotient (IQ) and negative symptoms. In the healthy control group, BDNF levels were not associated with cognitive test scores. Conclusion: Our results suggest that BDNF is associated with the cognitive impairment seen after a FEP. Further investigations of the role of this neurotrophin in the symptoms associated with psychosis onset are warranted.

Terapia celular para el tratamiento de la enfermedad de Alzheimer: angiogénesis terapéutica inducida por células microencapsuladas secretoras del factor de crecimiento del endotelio vascular

197 p. (Bibliogr. 189-197)

Vascular endothelial growth factor regulates melanoma cell adhesion and growth in the bone marrow microenvironment via tumor cyclooxygenase-2

Background: Human melanoma frequently colonizes bone marrow (BM) since its earliest stage of systemic dissemination, prior to clinical metastasis occurrence. However, how melanoma cell adhesion and proliferation mechanisms are regulated within bone marrow stromal cell (BMSC) microenvironment remain unclear. Consistent with the prometastatic role of inflammatory and angiogenic factors, several studies have reported elevated levels of cyclooxygenase-2 (COX-2) in melanoma although its pathogenic role in bone marrow melanoma metastasis is unknown. Methods: Herein we analyzed the effect of cyclooxygenase-2 (COX-2) inhibitor celecoxib in a model of generalized BM dissemination of left cardiac ventricle-injected B16 melanoma (B16M) cells into healthy and bacterial endotoxin lipopolysaccharide (LPS)-pretreated mice to induce inflammation. In addition, B16M and human A375 melanoma (A375M) cells were exposed to conditioned media from basal and LPS-treated primary cultured murine and human BMSCs, and the contribution of COX-2 to the adhesion and proliferation of melanoma cells was also studied. Results: Mice given one single intravenous injection of LPS 6 hour prior to cancer cells significantly increased B16M metastasis in BM compared to untreated mice; however, administration of oral celecoxib reduced BM metastasis incidence and volume in healthy mice, and almost completely abrogated LPS-dependent melanoma metastases. In vitro, untreated and LPS-treated murine and human BMSC-conditioned medium (CM) increased VCAM-1-dependent BMSC adherence and proliferation of B16M and A375M cells, respectively, as compared to basal medium-treated melanoma cells. Addition of celecoxib to both B16M and A375M cells abolished adhesion and proliferation increments induced by BMSC-CM. TNF alpha and VEGF secretion increased in the supernatant of LPS-treated BMSCs; however, anti-VEGF neutralizing antibodies added to B16M and A375M cells prior to LPS-treated BMSC-CM resulted in a complete abrogation of both adhesion-and proliferation-stimulating effect of BMSC on melanoma cells. Conversely, recombinant VEGF increased adherence to BMSC and proliferation of both B16M and A375M cells, compared to basal medium-treated cells, while addition of celecoxib neutralized VEGF effects on melanoma. Recombinant TNFa induced B16M production of VEGF via COX-2-dependent mechanism. Moreover, exogenous PGE2 also increased B16M cell adhesion to immobilized recombinant VCAM-1. Conclusions: We demonstrate the contribution of VEGF-induced tumor COX-2 to the regulation of adhesion-and proliferation-stimulating effects of TNFa, from endotoxin-activated bone marrow stromal cells, on VLA-4-expressing

Dual-path methods for propagating quantum microwaves

We study quantum state tomography, entanglement detection and channel noise reconstruction of propagating quantum microwaves via dual-path methods. The presented schemes make use of the following key elements: propagation channels, beam splitters, linear amplifiers and field quadrature detectors. Remarkably, our methods are tolerant to the ubiquitous noise added to the signals by phase-insensitive microwave amplifiers. Furthermore, we analyse our techniques with numerical examples and experimental data, and compare them with the scheme developed in Eichler et al (2011 Phys. Rev. Lett. 106 220503; 2011 Phys. Rev. Lett. 107 113601), based on a single path. Our methods provide key toolbox components that may pave the way towards quantum microwave teleportation and communication protocols.

RCeveierwamide and ceramide 1-phosphate in health and disease

Sphingolipids are essential components of cell membranes, and many of them regulate vital cell functions. In particular, ceramide plays crucial roles in cell signaling processes. Two major actions of ceramides are the promotion of cell cycle arrest and the induction of apoptosis. Phosphorylation of ceramide produces ceramide 1-phosphate (C1P), which has opposite effects to ceramide. C1P is mitogenic and has prosurvival properties. In addition, C1P is an important mediator of inflammatory responses, an action that takes place through stimulation of cytosolic phospholipase A2, and the subsequent release of arachidonic acid and prostaglandin formation. All of the former actions are thought to be mediated by intracellularly generated C1P. However, the recent observation that C1P stimulates macrophage chemotaxis implicates specific plasma membrane receptors that are coupled to Gi proteins. Hence, it can be concluded that C1P has dual actions in cells, as it can act as an intracellular second messenger to promote cell survival, or as an extracellular receptor agonist to stimulate cell migration.

The COMT Val158 Met polymorphism as an associated risk factor for Alzheimer disease and mild cognitive impairment in APOE 4 carriers

Background: The aim of this study is to examine the influence of the catechol-O-methyltranferase (COMT) gene (polymorphism Val158 Met) as a risk factor for Alzheimer's disease (AD) and mild cognitive impairment of amnesic type (MCI), and its synergistic effect with the apolipoprotein E gene (APOE). A total of 223 MCI patients, 345 AD and 253 healthy controls were analyzed. Clinical criteria and neuropsychological tests were used to establish diagnostic groups. The DNA Bank of the University of the Basque Country (UPV-EHU) (Spain) determined COMT Val158 Met and APOE genotypes using real time polymerase chain reaction (rtPCR) and polymerase chain reaction (PCR), and restriction fragment length polymorphism (RFLPs), respectively. Multinomial logistic regression models were used to determine the risk of AD and MCI. Results: Neither COMT alleles nor genotypes were independent risk factors for AD or MCI. The high activity genotypes (GG and AG) showed a synergistic effect with APOE epsilon 4 allele, increasing the risk of AD (OR = 5.96, 95% CI 2.74-12.94, p < 0.001 and OR = 6.71, 95% CI 3.36-13.41, p < 0.001 respectivily). In AD patients this effect was greater in women. In MCI patients such as synergistic effect was only found between AG and APOE epsilon 4 allele (OR = 3.21 95% CI 1.56-6.63, p = 0.02) and was greater in men (OR = 5.88 95% CI 1.69-20.42, p < 0.01). Conclusion: COMT (Val158 Met) polymorphism is not an independent risk factor for AD or MCI, but shows a synergistic effect with APOE epsilon 4 allele that proves greater in women with AD.

El clima de aula. Un factor decisivo en el aprendizaje de lenguas

[spa] Se ha propuesto una guía didáctica para realizar en sesiones de euskera que profundice en el conocimiento mutuo entre los alumnos para que se fomente así la creación de vinculos interpersonales basados en el diálogo, la negociación y la comprensión. Todo ello supone la generación de un ambiente de aula cálido en el que todos los alumnos (gitanos y no gitanos) se sientan respetados, reconocidos y valorados, lo que garantiza el desarrollo óptimo y el acercamiento de los alumnos a la segunda lengua

Optimizar una producción II. Estudio y Comparación de un Problema de Programación lineal y su Dual. Resolución y Valoración de un caso práctico y su programación usando Excel y Win QSB.

En este trabajo se va a explicar la relación que existe entre la optimización de un problema lineal y el problema dual correspondiente. Se usara la herramienta Solver del Microsoft Excel para resolver los el problema de programación lineal planteado. Se analizaran los resultados obtenidos tanto del problema primal como del problema dual y se explicara el significado de los resultados obtenidos. Se finalizara con unas conclusiones donde se expondría lo aprendido durante este trabajo y el significado económico de este tipo de problemas.