@misc{Frank2013, type = {Master Thesis}, author = {Frank, Mario}, title = {TEMPLAR : efficient determination of relevant axioms in big formula sets for theorem proving}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus-72112}, school = {Universit{\"a}t Potsdam}, year = {2013}, abstract = {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.}, 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} } @article{WarringtonBeaumontHorikoshietal.2019, author = {Warrington, Nicole and Beaumont, Robin and Horikoshi, Momoko and Day, Felix R. and Helgeland, {\O}yvind and Laurin, Charles and Bacelis, Jonas and Peng, Shouneng and Hao, Ke and Feenstra, Bjarke and Wood, Andrew R. and Mahajan, Anubha and Tyrrell, Jessica and Robertson, Neil R. and Rayner, N. William and Qiao, Zhen and Moen, Gunn-Helen and Vaudel, Marc and Marsit, Carmen and Chen, Jia and Nodzenski, Michael and Schnurr, Theresia M. and Zafarmand, Mohammad Hadi and Bradfield, Jonathan P. and Grarup, Niels and Kooijman, Marjolein N. and Li-Gao, Ruifang and Geller, Frank and Ahluwalia, Tarunveer Singh and Paternoster, Lavinia and Rueedi, Rico and Huikari, Ville and Hottenga, Jouke-Jan and Lyytik{\"a}inen, Leo-Pekka and Cavadino, Alana and Metrustry, Sarah and Cousminer, Diana L. and Wu, Ying and Thiering, Elisabeth Paula and Wang, Carol A. and Have, Christian Theil and Vilor-Tejedor, Natalia and Joshi, Peter K. and Painter, Jodie N. and Ntalla, Ioanna and Myhre, Ronny and Pitk{\"a}nen, Niina and van Leeuwen, Elisabeth M. and Joro, Raimo and Lagou, Vasiliki and Richmond, Rebecca C. and Espinosa, Ana and Barton, Sheila J. and Inskip, Hazel M. and Holloway, John W. and Santa-Marina, Loreto and Estivill, Xavier and Ang, Wei and Marsh, Julie A. and Reichetzeder, Christoph and Marullo, Letizia and Hocher, Berthold and Lunetta, Kathryn L. and Murabito, Joanne M. and Relton, Caroline L. and Kogevinas, Manolis and Chatzi, Leda and Allard, Catherine and Bouchard, Luigi and Hivert, Marie-France and Zhang, Ge and Muglia, Louis J. and Heikkinen, Jani and Morgen, Camilla S. and van Kampen, Antoine H. C. and van Schaik, Barbera D. C. and Mentch, Frank D. and Langenberg, Claudia and Scott, Robert A. and Zhao, Jing Hua and Hemani, Gibran and Ring, Susan M. and Bennett, Amanda J. and Gaulton, Kyle J. and Fernandez-Tajes, Juan and van Zuydam, Natalie R. and Medina-Gomez, Carolina and de Haan, Hugoline G. and Rosendaal, Frits R. and Kutalik, Zolt{\´a}n and Marques-Vidal, Pedro and Das, Shikta and Willemsen, Gonneke and Mbarek, Hamdi and M{\"u}ller-Nurasyid, Martina and Standl, Marie and Appel, Emil V. R. and Fonvig, Cilius Esmann and Trier, Caecilie and van Beijsterveldt, Catharina E. M. and Murcia, Mario and Bustamante, Mariona and Bon{\`a}s-Guarch, S{\´i}lvia and Hougaard, David M. and Mercader, Josep M. and Linneberg, Allan and Schraut, Katharina E. and Lind, Penelope A. and Medland, Sarah Elizabeth and Shields, Beverley M. and Knight, Bridget A. and Chai, Jin-Fang and Panoutsopoulou, Kalliope and Bartels, Meike and S{\´a}nchez, Friman and Stokholm, Jakob and Torrents, David and Vinding, Rebecca K. and Willems, Sara M. and Atalay, Mustafa and Chawes, Bo L. and Kovacs, Peter and Prokopenko, Inga and Tuke, Marcus A. and Yaghootkar, Hanieh and Ruth, Katherine S. and Jones, Samuel E. and Loh, Po-Ru and Murray, Anna and Weedon, Michael N. and T{\"o}njes, Anke and Stumvoll, Michael and Michaelsen, Kim Fleischer and Eloranta, Aino-Maija and Lakka, Timo A. and van Duijn, Cornelia M. and Kiess, Wieland and Koerner, Antje and Niinikoski, Harri and Pahkala, Katja and Raitakari, Olli T. and Jacobsson, Bo and Zeggini, Eleftheria and Dedoussis, George V. and Teo, Yik-Ying and Saw, Seang-Mei and Montgomery, Grant W. and Campbell, Harry and Wilson, James F. and Vrijkotte, Tanja G. M. and Vrijheid, Martine and de Geus, Eco J. C. N. and Hayes, M. Geoffrey and Kadarmideen, Haja N. and Holm, Jens-Christian and Beilin, Lawrence J. and Pennell, Craig E. and Heinrich, Joachim and Adair, Linda S. and Borja, Judith B. and Mohlke, Karen L. and Eriksson, Johan G. and Widen, Elisabeth E. and Hattersley, Andrew T. and Spector, Tim D. and Kaehoenen, Mika and Viikari, Jorma S. and Lehtimaeki, Terho and Boomsma, Dorret I. and Sebert, Sylvain and Vollenweider, Peter and Sorensen, Thorkild I. A. and Bisgaard, Hans and Bonnelykke, Klaus and Murray, Jeffrey C. and Melbye, Mads and Nohr, Ellen A. and Mook-Kanamori, Dennis O. and Rivadeneira, Fernando and Hofman, Albert and Felix, Janine F. and Jaddoe, Vincent W. V. and Hansen, Torben and Pisinger, Charlotta and Vaag, Allan A. and Pedersen, Oluf and Uitterlinden, Andre G. and Jarvelin, Marjo-Riitta and Power, Christine and Hypponen, Elina and Scholtens, Denise M. and Lowe, William L. and Smith, George Davey and Timpson, Nicholas J. and Morris, Andrew P. and Wareham, Nicholas J. and Hakonarson, Hakon and Grant, Struan F. A. and Frayling, Timothy M. and Lawlor, Debbie A. and Njolstad, Pal R. and Johansson, Stefan and Ong, Ken K. and McCarthy, Mark I. and Perry, John R. B. and Evans, David M. and Freathy, Rachel M.}, title = {Maternal and fetal genetic effects on birth weight and their relevance to cardio-metabolic risk factors}, series = {Nature genetics}, volume = {51}, journal = {Nature genetics}, number = {5}, publisher = {Nature Publ. Group}, address = {New York}, organization = {EGG Consortium}, issn = {1061-4036}, pages = {804 -- +}, year = {2019}, abstract = {Birth weight variation is influenced by fetal and maternal genetic and non-genetic factors, and has been reproducibly associated with future cardio-metabolic health outcomes. In expanded genome-wide association analyses of own birth weight (n = 321,223) and offspring birth weight (n = 230,069 mothers), we identified 190 independent association signals (129 of which are novel). We used structural equation modeling to decompose the contributions of direct fetal and indirect maternal genetic effects, then applied Mendelian randomization to illuminate causal pathways. For example, both indirect maternal and direct fetal genetic effects drive the observational relationship between lower birth weight and higher later blood pressure: maternal blood pressure-raising alleles reduce offspring birth weight, but only direct fetal effects of these alleles, once inherited, increase later offspring blood pressure. Using maternal birth weight-lowering genotypes to proxy for an adverse intrauterine environment provided no evidence that it causally raises offspring blood pressure, indicating that the inverse birth weight-blood pressure association is attributable to genetic effects, and not to intrauterine programming.}, language = {en} } @article{SemenyshynHentschelStanglmairetal.2018, author = {Semenyshyn, Rostyslav and Hentschel, Mario and Stanglmair, Christoph and Teutsch, Tanja and Tarin, Cristina and Pacholski, Claudia and Giessen, Harald and Neubrech, Frank}, title = {In vitro monitoring conformational changes of polypeptide monolayers using infrared plasmonic nanoantennas}, series = {Nano letters : a journal dedicated to nanoscience and nanotechnology}, volume = {19}, journal = {Nano letters : a journal dedicated to nanoscience and nanotechnology}, number = {1}, publisher = {American Chemical Society}, address = {Washington}, issn = {1530-6984}, doi = {10.1021/acs.nanolett.8b02372}, pages = {1 -- 7}, year = {2018}, abstract = {Proteins and peptides play a predominant role in biochemical reactions of living cells. In these complex environments, not only the constitution of the molecules but also their three-dimensional configuration defines their functionality. This so-called secondary structure of proteins is crucial for understanding their function in living matter. Misfolding, for example, is suspected as the cause of neurodegenerative diseases such as Alzheimer's and Parkinson's disease. Ultimately, it is necessary to study a single protein and its folding dynamics. Here, we report a first step in this direction, namely ultrasensitive detection and discrimination of in vitro polypeptide folding and unfolding processes using resonant plasmonic nanoantennas for surface-enhanced vibrational spectroscopy. We utilize poly-l-lysine as a model system which has been functionalized on the gold surface. By in vitro infrared spectroscopy of a single molecular monolayer at the amide I vibrations we directly monitor the reversible conformational changes between α-helix and β-sheet states induced by controlled external chemical stimuli. Our scheme in combination with advanced positioning of the peptides and proteins and more brilliant light sources is highly promising for ultrasensitive in vitro studies down to the single protein level.}, language = {en} } @book{RanaMohapatraSidorovaetal.2022, author = {Rana, Kaushik and Mohapatra, Durga Prasad and Sidorova, Julia and Lundberg, Lars and Sk{\"o}ld, Lars and Lopes Grim, Lu{\´i}s Fernando and Sampaio Gradvohl, Andr{\´e} Leon and Cremerius, Jonas and Siegert, Simon and Weltzien, Anton von and Baldi, Annika and Klessascheck, Finn and Kalancha, Svitlana and Lichtenstein, Tom and Shaabani, Nuhad and Meinel, Christoph and Friedrich, Tobias and Lenzner, Pascal and Schumann, David and Wiese, Ingmar and Sarna, Nicole and Wiese, Lena and Tashkandi, Araek Sami and van der Walt, Est{\´e}e and Eloff, Jan H. P. and Schmidt, Christopher and H{\"u}gle, Johannes and Horschig, Siegfried and Uflacker, Matthias and Najafi, Pejman and Sapegin, Andrey and Cheng, Feng and Stojanovic, Dragan and Stojnev Ilić, Aleksandra and Djordjevic, Igor and Stojanovic, Natalija and Predic, Bratislav and Gonz{\´a}lez-Jim{\´e}nez, Mario and de Lara, Juan and Mischkewitz, Sven and Kainz, Bernhard and van Hoorn, Andr{\´e} and Ferme, Vincenzo and Schulz, Henning and Knigge, Marlene and Hecht, Sonja and Prifti, Loina and Krcmar, Helmut and Fabian, Benjamin and Ermakova, Tatiana and Kelkel, Stefan and Baumann, Annika and Morgenstern, Laura and Plauth, Max and Eberhard, Felix and Wolff, Felix and Polze, Andreas and Cech, Tim and Danz, Noel and Noack, Nele Sina and Pirl, Lukas and Beilharz, Jossekin Jakob and De Oliveira, Roberto C. L. and Soares, F{\´a}bio Mendes and Juiz, Carlos and Bermejo, Belen and M{\"u}hle, Alexander and Gr{\"u}ner, Andreas and Saxena, Vageesh and Gayvoronskaya, Tatiana and Weyand, Christopher and Krause, Mirko and Frank, Markus and Bischoff, Sebastian and Behrens, Freya and R{\"u}ckin, Julius and Ziegler, Adrian and Vogel, Thomas and Tran, Chinh and Moser, Irene and Grunske, Lars and Sz{\´a}rnyas, G{\´a}bor and Marton, J{\´o}zsef and Maginecz, J{\´a}nos and Varr{\´o}, D{\´a}niel and Antal, J{\´a}nos Benjamin}, title = {HPI Future SOC Lab - Proceedings 2018}, number = {151}, editor = {Meinel, Christoph and Polze, Andreas and Beins, Karsten and Strotmann, Rolf and Seibold, Ulrich and R{\"o}dszus, Kurt and M{\"u}ller, J{\"u}rgen}, publisher = {Universit{\"a}tsverlag Potsdam}, address = {Potsdam}, isbn = {978-3-86956-547-7}, issn = {1613-5652}, doi = {10.25932/publishup-56371}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-563712}, publisher = {Universit{\"a}t Potsdam}, pages = {x, 277}, year = {2022}, abstract = {The "HPI Future SOC Lab" is a cooperation of the Hasso Plattner Institute (HPI) and industry partners. Its mission is to enable and promote exchange and interaction between the research community and the industry partners. The HPI Future SOC Lab provides researchers with free of charge access to a complete infrastructure of state of the art hard and software. This infrastructure includes components, which might be too expensive for an ordinary research environment, such as servers with up to 64 cores and 2 TB main memory. The offerings address researchers particularly from but not limited to the areas of computer science and business information systems. Main areas of research include cloud computing, parallelization, and In-Memory technologies. This technical report presents results of research projects executed in 2018. Selected projects have presented their results on April 17th and November 14th 2017 at the Future SOC Lab Day events.}, language = {en} } @article{PostbergGruenHoranyietal.2011, author = {Postberg, Frank and Gr{\"u}n, Eberhard and Horanyi, Mihaly and Kempf, Sascha and Krueger, Harald and Schmidt, J{\"u}rgen and Spahn, Frank and Srama, Ralf and Sternovsky, Zoltan and Trieloff, Mario}, title = {Compositional mapping of planetary moons by mass spectrometry of dust ejecta}, series = {Planetary and space science}, volume = {59}, journal = {Planetary and space science}, number = {14}, publisher = {Elsevier}, address = {Oxford}, issn = {0032-0633}, doi = {10.1016/j.pss.2011.05.001}, pages = {1815 -- 1825}, year = {2011}, abstract = {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.}, language = {en} } @article{KaercherFilstrupBraunsetal.2020, author = {K{\"a}rcher, Oskar and Filstrup, Christopher T. and Brauns, Mario and Tasevska, Orhideja and Patceva, Suzana and Hellwig, Niels and Walz, Ariane and Frank, Karin and Markovic, Danijela}, title = {Chlorophyll a relationships with nutrients and temperature, and predictions for lakes across perialpine and Balkan mountain regions}, series = {Inland Waters}, volume = {10}, journal = {Inland Waters}, number = {1}, publisher = {Taylor \& Francis}, address = {London}, issn = {2044-2041}, doi = {10.1080/20442041.2019.1689768}, pages = {29 -- 41}, year = {2020}, abstract = {Model-derived relationships between chlorophyll a (Chl-a) and nutrients and temperature have fundamental implications for understanding complex interactions among water quality measures used for lake classification, yet accuracy comparisons of different approaches are scarce. Here, we (1) compared Chl-a model performances across linear and nonlinear statistical approaches; (2) evaluated single and combined effects of nutrients, depth, and temperature as lake surface water temperature (LSWT) or altitude on Chl-a; and (3) investigated the reliability of the best water quality model across 13 lakes from perialpine and central Balkan mountain regions. Chl-a was modelled using in situ water quality data from 157 European lakes; elevation data and LSWT in situ data were complemented by remote sensing measurements. Nonlinear approaches performed better, implying complex relationships between Chl-a and the explanatory variables. Boosted regression trees, as the best performing approach, accommodated interactions among predictor variables. Chl-a-nutrient relationships were characterized by sigmoidal curves, with total phosphorus having the largest explanatory power for our study region. In comparison with LSWT, utilization of altitude, the often-used temperature surrogate, led to different influence directions but similar predictive performances. These results support utilizing altitude in models for Chl-a predictions. Compared to Chl-a observations, Chl-a predictions of the best performing approach for mountain lakes (oligotrophic-eutrophic) led to minor differences in trophic state categorizations. Our findings suggest that both models with LSWT and altitude are appropriate for water quality predictions of lakes in mountain regions and emphasize the importance of incorporating interactions among variables when facing lake management challenges.}, language = {en} } @misc{KaercherFilstrupBraunsetal.2020, author = {K{\"a}rcher, Oskar and Filstrup, Christopher T. and Brauns, Mario and Tasevska, Orhideja and Patceva, Suzana and Hellwig, Niels and Walz, Ariane and Frank, Karin and Markovic, Danijela}, title = {Chlorophyll a relationships with nutrients and temperature, and predictions for lakes across perialpine and Balkan mountain regions}, series = {Zweitver{\"o}ffentlichungen der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe}, journal = {Zweitver{\"o}ffentlichungen der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe}, number = {1}, issn = {1866-8372}, doi = {10.25932/publishup-51527}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-515271}, pages = {15}, year = {2020}, abstract = {Model-derived relationships between chlorophyll a (Chl-a) and nutrients and temperature have fundamental implications for understanding complex interactions among water quality measures used for lake classification, yet accuracy comparisons of different approaches are scarce. Here, we (1) compared Chl-a model performances across linear and nonlinear statistical approaches; (2) evaluated single and combined effects of nutrients, depth, and temperature as lake surface water temperature (LSWT) or altitude on Chl-a; and (3) investigated the reliability of the best water quality model across 13 lakes from perialpine and central Balkan mountain regions. Chl-a was modelled using in situ water quality data from 157 European lakes; elevation data and LSWT in situ data were complemented by remote sensing measurements. Nonlinear approaches performed better, implying complex relationships between Chl-a and the explanatory variables. Boosted regression trees, as the best performing approach, accommodated interactions among predictor variables. Chl-a-nutrient relationships were characterized by sigmoidal curves, with total phosphorus having the largest explanatory power for our study region. In comparison with LSWT, utilization of altitude, the often-used temperature surrogate, led to different influence directions but similar predictive performances. These results support utilizing altitude in models for Chl-a predictions. Compared to Chl-a observations, Chl-a predictions of the best performing approach for mountain lakes (oligotrophic-eutrophic) led to minor differences in trophic state categorizations. Our findings suggest that both models with LSWT and altitude are appropriate for water quality predictions of lakes in mountain regions and emphasize the importance of incorporating interactions among variables when facing lake management challenges.}, language = {en} } @article{SchellhornFrankKreitz2019, author = {Schellhorn, Sebastian and Frank, Mario and Kreitz, Christoph}, title = {Br{\"u}ckenkurse f{\"u}r mathematische und informatiknahe Studieng{\"a}nge}, series = {Alles auf Anfang! Befunde und Perspektiven zum Studieneingang}, journal = {Alles auf Anfang! Befunde und Perspektiven zum Studieneingang}, publisher = {Universit{\"a}tsverlag Potsdam}, address = {Potsdam}, isbn = {978-3-86956-452-4}, issn = {2192-1075}, doi = {10.25932/publishup-42853}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-428538}, pages = {257 -- 271}, year = {2019}, language = {de} } @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} }