Dependence Logic: Investigations into Higher-Order Semantics Defined on Teams

This thesis is a study of a rather new logic called dependence logic and its closure under classical negation, team logic. In this thesis, dependence logic is investigated from several aspects. Some rules are presented for quantifier swapping in dependence logic and team logic. Such rules are among the basic tools one must be familiar with in order to gain the required intuition for using the logic for practical purposes. The thesis compares Ehrenfeucht-Fraïssé (EF) games of first order logic and dependence logic and defines a third EF game that characterises a mixed case where first order formulas are measured in the formula rank of dependence logic. The thesis contains detailed proofs of several translations between dependence logic, team logic, second order logic and its existential fragment. Translations are useful for showing relationships between the expressive powers of logics. Also, by inspecting the form of the translated formulas, one can see how an aspect of one logic can be expressed in the other logic. The thesis makes preliminary investigations into proof theory of dependence logic. Attempts focus on finding a complete proof system for a modest yet nontrivial fragment of dependence logic. A key problem is identified and addressed in adapting a known proof system of classical propositional logic to become a proof system for the fragment, namely that the rule of contraction is needed but is unsound in its unrestricted form. A proof system is suggested for the fragment and its completeness conjectured. Finally, the thesis investigates the very foundation of dependence logic. An alternative semantics called 1-semantics is suggested for the syntax of dependence logic. There are several key differences between 1-semantics and other semantics of dependence logic. 1-semantics is derived from first order semantics by a natural type shift. Therefore 1-semantics reflects an established semantics in a coherent manner. Negation in 1-semantics is a semantic operation and satisfies the law of excluded middle. A translation is provided from unrestricted formulas of existential second order logic into 1-semantics. Also game theoretic semantics are considerd in the light of 1-semantics.

Integrative functional genomics analysis of sustained polyploidy phenotypes in breast cancer cells identifies an oncogenic profile for GINS2

Aneuploidy is among the most obvious differences between normal and cancer cells. However, mechanisms contributing to development and maintenance of aneuploid cell growth are diverse and incompletely understood. Functional genomics analyses have shown that aneuploidy in cancer cells is correlated with diffuse gene expression signatures and that aneuploidy can arise by a variety of mechanisms, including cytokinesis failures, DNA endoreplication and possibly through polyploid intermediate states. Here, we used a novel cell spot microarray technique to identify genes with a loss-of-function effect inducing polyploidy and/or allowing maintenance of polyploid cell growth of breast cancer cells. Integrative genomics profiling of candidate genes highlighted GINS2 as a potential oncogene frequently overexpressed in clinical breast cancers as well as in several other cancer types. Multivariate analysis indicated GINS2 to be an independent prognostic factor for breast cancer outcome (p = 0.001). Suppression of GINS2 expression effectively inhibited breast cancer cell growth and induced polyploidy. In addition, protein level detection of nuclear GINS2 accurately distinguished actively proliferating cancer cells suggesting potential use as an operational biomarker.

The International Large Detector: Letter of Intent

The International Large Detector (ILD) is a concept for a detector at the International Linear Collider, ILC. The ILC will collide electrons and positrons at energies of initially 500 GeV, upgradeable to 1 TeV. The ILC has an ambitious physics program, which will extend and complement that of the Large Hadron Collider (LHC). A hallmark of physics at the ILC is precision. The clean initial state and the comparatively benign environment of a lepton collider are ideally suited to high precision measurements. To take full advantage of the physics potential of ILC places great demands on the detector performance. The design of ILD is driven by these requirements. Excellent calorimetry and tracking are combined to obtain the best possible overall event reconstruction, including the capability to reconstruct individual particles within jets for particle ow calorimetry. This requires excellent spatial resolution for all detector systems. A highly granular calorimeter system is combined with a central tracker which stresses redundancy and efficiency. In addition, efficient reconstruction of secondary vertices and excellent momentum resolution for charged particles are essential for an ILC detector. The interaction region of the ILC is designed to host two detectors, which can be moved into the beam position with a push-pull scheme. The mechanical design of ILD and the overall integration of subdetectors takes these operational conditions into account.

Snow cover models in operational watershed forecasting

Yhteenveto: Lumimallit vesistöjen ennustemalleissa