98 research outputs found
Cut-elimination, substitution and normalisation
No full textDate of Acceptance: 01/2015We present a proof (of the main parts of which there is a formal version, checked with the Isabelle proof assistant) that, for a G3-style calculus covering all of intuitionistic zero-order logic, with an associated term calculus, and with a particular strongly normalising and confluent system of cut-reduction rules, every reduction step has, as its natural deduction translation, a sequence of zero or more reduction steps (detour reductions, permutation reductions or simplifications). This complements and (we believe) clarifies earlier work by (e.g.) Zucker and Pottinger on a question raised in 1971 by Kreisel.Peer reviewe
Antiproliferative efficacies but minor drug transporter inducing effects of paclitaxel, cisplatin, or 5-fluorouracil in a murine xenograft model for head and neck squamous cell carcinoma
No full textDrug-induced multidrug resistance (MDR) has been linked to overexpression of drug transporting proteins in head and neck squamous cell carcinoma (HNSCC) in vitro. The aim of this work was to reassess these findings in a murine xenograft model. NOD-SCID mice xenotransplanted with 106 HNO97 cells were treated for four consecutive weeks with weekly paclitaxel, biweekly cisplatin (both intraperitoneal), or 5-fluorouracil (5-FU, administered by osmotic pump). Tumor volume and body weight were weekly documented. Expression of drug transporters and Ki-67 marker were examined using quantitative real-time polymerase chain reaction and/or immunohistochemistry. Both paclitaxel and cisplatin significantly reduced tumor volumes after 2–3 weeks. 5-FU-treated animals had significantly lower body weights after 2 or 4 weeks of chemotherapy. None of the drugs affected expression of drug transporters at the mRNA level. However, P-glycoprotein (Pgp) protein expression was increased by paclitaxel (P < 0.01). Ki-67 expression did not change during treatment irrespective of the drug applied. Paclitaxel and cisplatin are effectively tumor volume reducing drugs in a murine xenograft model of HNSCC. Paclitaxel enhanced Pgp expression at the protein level, but not at the mRNA level suggesting transcriptional induction to be of minor relevance. In contrast, posttranscriptional mechanisms or Darwinian selection of intrinsically drug transporter overexpressing MDR cells might lead to iatrogenic chemotherapy resistance in HNSCC.Fil: Theile, Dirk. Universität Heidelberg; AlemaniaFil: Gal, Zoltan. Universität Heidelberg; AlemaniaFil: Warta, Rolf. Universität Heidelberg; AlemaniaFil: Rigalli, Juan Pablo. Universität Heidelberg; Alemania. Consejo Nacional de Investigaciones Científicas y Técnicas; ArgentinaFil: Lahrmann, Bernd. Universität Heidelberg; AlemaniaFil: Grabe, Niels. Universität Heidelberg; AlemaniaFil: Herold Mende, Christel. Universität Heidelberg; AlemaniaFil: Dyckhoff, Gerhard. Universität Heidelberg; AlemaniaFil: Weiss, Johanna. Universität Heidelberg; Alemani
Tools and techniques for formalising structural proof theory
No full textWhilst results from Structural Proof Theory can be couched in many formalisms, it is
the sequent calculus which is the most amenable of the formalisms to metamathematical
treatment. Constructive syntactic proofs are filled with bureaucratic details; rarely are
all cases of a proof completed in the literature. Two intermediate results can be used to
drastically reduce the amount of effort needed in proofs of Cut admissibility: Weakening
and Invertibility. Indeed, whereas there are proofs of Cut admissibility which do not use
Invertibility, Weakening is almost always necessary. Use of these results simply shifts the
bureaucracy, however; Weakening and Invertibility, whilst more easy to prove, are still not
trivial. We give a framework under which sequent calculi can be codified and analysed,
which then allows us to prove various results: for a calculus to admit Weakening and for a
rule to be invertible in a calculus. For the latter, even though many calculi are investigated,
the general condition is simple and easily verified. The results have been applied to G3ip,
G3cp, G3s, G3-LC and G4ip.
Invertibility is important in another respect; that of proof-search. Should all rules in
a calculus be invertible, then terminating root-first proof search gives a decision procedure
for formulae without the need for back-tracking. To this end, we present some results
about the manipulation of rule sets. It is shown that the transformations do not affect the
expressiveness of the calculus, yet may render more rules invertible. These results can guide
the design of efficient calculi.
When using interactive proof assistants, every case of a proof, however complex, must be
addressed and proved before one can declare the result formalised. To do this in a human readable
way adds a further layer of complexity; most proof assistants give output which is
only legible to a skilled user of that proof assistant. We give human-readable formalisations
of Cut admissibility for G3cp and G3ip, Contraction admissibility for G4ip and Craig's
Interpolation Theorem for G3i using the Isar vernacular of Isabelle. We also formalise the
new invertibility results, in part using the package for reasoning about first-order languages,
Nominal Isabelle. Examples are given showing the effectiveness of the formalisation. The
formal proof of invertibility using the new methods is drastically shorter than the traditional,
direct method
Vertrauen in die Gerichtsbarkeit und Unternehmenserfolg in einer Transformationswirtschaft
No full textThe number of publications in the area of Cutting and Packing (C & P) has increased considerably over the last two decades. The typology of C & P problems introduced by Dyckhoff (1990) initially provided an excellent instrument for the organisation and categorisation of existing and new literature. However, over the years also some deficiencies of this typology became evident, which created problems in dealing with recent developments and prevented it from being accepted more generally. In this paper, the authors present an improved typology, which is partially based on Dyckhoff\u27s original ideas, but introduces new categorisation criteria, which define problem categories different from those of Dyckhoff. Furthermore, a new, consistent system of names is suggested for these problem categories. Finally, the practicability of the new scheme is demonstrated by using it as a basis for a categorisation of the C & P literature from the years between 1995 and 2004
Totale Laryngektomie: Wundinfektionen sind bei Diabetespatienten häufiger
No full textFilimonov A et al. Postoperative Complications of Total Laryngectomy in Diabetic Patients. Laryngoscope 2017; 127: 2247–2251
Diabetes Mellitus gilt als Risikofaktor vieler Komorbiditäten und Komplikationen. Ob sich die Stoffwechselerkrankung ebenso negativ auf das Ergebnis einer
totalen Laryngektomie auswirken kann, haben Filimonov und Kolleginnen/Kollegen jetzt anhand einer retrospektiven Datenanalyse genauer betrachtet.
</jats:p
Monolayerkulturen von bovinen Chondrozyten : immunzytochemische Charakterisierung des Phänotyps im zeitlichen Verlauf der Kultur
No full textMonolayerkulturen von bovinen Chondrozyten : immunzytochemische Charakterisierung des Phänotyps im zeitlichen Verlauf der Kultur
No full textPhosphorylation of AKT(Ser473) serves as an independent prognostic marker for radiosensitivity in advanced head and neck squamous cell carcinoma
No full textHead and neck squamous cell carcinoma (HNSCC) is frequently characterized by high resistance to radiotherapy, which critically depends on both altered signaling pathways within tumor cells and their dynamic interaction with the tumor microenvironment. This study evaluated the prognostic value of the phosphorylation status of AKT on Ser473 and Thr308 for the clinical outcome of patients with advanced HNSCC on radiotherapy. Furthermore, we investigated the impact of AKT(Ser473) phosphorylation [p-AKT(Ser473)] in the context of radioresistance using ex vivo tissue cultures that resemble the complex tissue architecture and paracrine interaction with the tumor microenvironment. In a cohort of 120 patients with advanced HNSCC, who were treated with primary or adjuvant radiotherapy, a significant association was found between relative p-AKT(Ser473) levels and overall survival (p = 0.006) as well as progression-free survival (p = 0.021), while no significant correlation was revealed for relative p-AKT(Thr308) levels. In ex vivo tissue cultures p-AKT(Ser473) levels were increased upon irradiation and treatment with the PI3K inhibitor LY294002 inhibited both basal and irradiation induced AKT(Ser473) phosphorylation. Strikingly, pretreatment with LY294002 sensitized tissue cultures derived from primary and recurrent tumors to radiotherapy as determined by impaired tumor cell proliferation and enhanced DNA damage. In conclusion, phosphorylation status of AKT(Ser473) in tumor specimens serves as a novel biomarker to identify patients with advanced HNSCC at high risk for treatment failure following radiotherapy, and our data from ex vivo tissue cultures support the assumption that pharmacological inhibition of AKT(Ser473) phosphorylation might circumvent radioresistance to improve efficiency and reduce toxicity of current treatment modalities
- …
