### Refine

#### Document Type

- Article (3)
- Master's Thesis (1)

#### Language

- English (4) (remove)

#### Keywords

- Relevanz (2)
- Theorembeweisen (2)
- Unifikation (2)
- relevance (2)
- theorem (2)
- Alveolar epithelial cells (1)
- Dust (1)
- Europa (1)
- Ganymede (1)
- Graphensuche (1)

Classical methods to analyze the surface composition of atmosphereless planetary objects from an orbiter are IR and gamma ray spectroscopy and neutron backscatter measurements. The idea to analyze surface properties with an in-situ instrument has been proposed by Johnson et al. (1998). There, it was suggested to analyze Europa's thin atmosphere with an ion and neutral gas spectrometer. Since the atmospheric components are released by sputtering of the moon's surface, they provide a link to surface composition. Here we present an improved, complementary method to analyze rocky or icy dust particles as samples of planetary objects from which they were ejected. Such particles, generated by the ambient meteoroid bombardment that erodes the surface, are naturally present on all atmosphereless moons and planets. The planetary bodies are enshrouded in clouds of ballistic dust particles, which are characteristic samples of their surfaces. In situ mass spectroscopic analysis of these dust particles impacting onto a detector of an orbiting spacecraft reveals their composition. Recent instrumental developments and tests allow the chemical characterization of ice and dust particles encountered at speeds as low as 1 km/s and an accurate reconstruction of their trajectories. Depending on the sampling altitude, a dust trajectory sensor can trace back the origin of each analyzed grain with about 10 km accuracy at the surface. Since the detection rates are of the order of thousand per orbit, a spatially resolved mapping of the surface composition can be achieved. Certain bodies (e.g., Europa) with particularly dense dust clouds, could provide impact statistics that allow for compositional mapping even on single flybys. Dust impact velocities are in general sufficiently high at orbiters about planetary objects with a radius > 1000 km and with only a thin or no atmosphere. In this work we focus on the scientific benefit of a dust spectrometer on a spacecraft orbiting Earth's Moon as well as Jupiter's Galilean satellites. This 'dust spectrometer' approach provides key chemical and isotopic constraints for varying provinces or geological formations on the surfaces, leading to better understanding of the body's geological evolution.

The majority of cases of community-acquired pneumonia are caused by Streptococcus pneumoniae and most studies on pneumococcal host interaction are based on cell culture or animal experiments. Thus, little is known about infections in human lung tissue.
Cyclooxygenase-2 and its metabolites play an important regulatory role in lung inflammation. Therefore, we established a pneumococcal infection model on human lung tissue demonstrating mitogen-activated protein kinase (MAPK)-dependent induction of cyclooxygenase-2 and its related metabolites.
In addition to alveolar macrophages and the vascular endothelium, cyclooxygenase-2 was upregulated in alveolar type II but not type I epithelial cells, which was confirmed in lungs of patients suffering from acute pneumonia. Moreover, we demonstrated the expression profile of all four E prostanoid receptors at the mRNA level and showed functionality of the E prostanoid(4) receptor by cyclic adenosine monophosphate production. Additionally, in comparison to previous studies, cyclooxygenase-2/prostaglandin E-2 related pro- and anti-inflammatory mediator regulation was partly confirmed in human lung tissue after pneumococcal infection.
Overall, cell type-specific and MAPK-dependent cyclooxygenase-2 expression and prostaglandin E-2 formation in human lung tissue may play an important role in the early phase of pneumococcal infections.

This document presents an axiom selection technique for classic first order theorem proving based on the relevance of axioms for the proof of a conjecture. It is based on unifiability of predicates and does not need statistical information like symbol frequency. The scope of the technique is the reduction of the set of axioms and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the axiom set, it can be used as a preprocessor for automated theorem proving. This technical report describes the conception, implementation and evaluation of ARDE. The selection method, which is based on a breadth-first graph search by unifiability of predicates, is a weakened form of the connection calculus and uses specialised variants or unifiability to speed up the selection. The implementation of the concept is evaluated with comparison to the results of the world championship of theorem provers of the year 2012 (CASC J6). It is shown that both the theorem prover leanCoP which uses the connection calculus and E which uses equality reasoning, can benefit from the selection approach. Also, the evaluation shows that the concept is applyable for theorem proving problems with thousands of formulae and that the selection is independent from the calculus used by the theorem prover.

This document presents a formula selection system for classical first order theorem proving based on the relevance of formulae for the proof of a conjecture. It is based on unifiability of predicates and is also able to use a linguistic approach for the selection. The scope of the technique is the reduction of the set of formulae and the increase of the amount of provable conjectures in a given time. Since the technique generates a subset of the formula set, it can be used as a preprocessor for automated theorem proving. The document contains the conception, implementation and evaluation of both selection concepts. While the one concept generates a search graph over the negation normal forms or Skolem normal forms of the given formulae, the linguistic concept analyses the formulae and determines frequencies of lexemes and uses a tf-idf weighting algorithm to determine the relevance of the formulae. Though the concept is built for first order logic, it is not limited to it. The concept can be used for higher order and modal logik, too, with minimal adoptions. The system was also evaluated at the world championship of automated theorem provers (CADE ATP Systems Competition, CASC-24) in combination with the leanCoP theorem prover and the evaluation of the results of the CASC and the benchmarks with the problems of the CASC of the year 2012 (CASC-J6) show that the concept of the system has positive impact to the performance of automated theorem provers. Also, the benchmarks with two different theorem provers which use different calculi have shown that the selection is independent from the calculus. Moreover, the concept of TEMPLAR has shown to be competitive to some extent with the concept of SinE and even helped one of the theorem provers to solve problems that were not (or slower) solved with SinE selection in the CASC. Finally, the evaluation implies that the combination of the unification based and linguistic selection yields more improved results though no optimisation was done for the problems.