@article{Frank2012, author = {Frank, Mario}, title = {Axiom relevance decision engine : technical report}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-72128}, year = {2012}, abstract = {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.}, language = {en} } @article{SzymanskiToenniesBecheretal.2012, author = {Szymanski, Kolja V. and T{\"o}nnies, Mario and Becher, Anne and Fatykhova, Diana and N'Guessan, Philippe D. and Gutbier, Birgitt and Klauschen, Frederick and Neusch{\"a}fer-Rube, Frank and Schneider, Paul and R{\"u}ckert, Jens and Neudecker, Jens and Bauer, Torsten T. and Dalhoff, Klaus and Droemann, Daniel and Gruber, Achim D. and Kershaw, Olivia and Temmesfeld-Wollbrueck, Bettina and Suttorp, Norbert and Hippenstiel, Stefan and Hocke, Andreas C.}, title = {Streptococcus pneumoniae-induced regulation of cyclooxygenase-2 in human lung tissue}, series = {The European respiratory journal : official journal of the European Society for Clinical Respiratory Physiology}, volume = {40}, journal = {The European respiratory journal : official journal of the European Society for Clinical Respiratory Physiology}, number = {6}, publisher = {European Respiratory Society}, address = {Sheffield}, issn = {0903-1936}, doi = {10.1183/09031936.00186911}, pages = {1458 -- 1467}, year = {2012}, abstract = {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.}, language = {en} }