TY - JOUR A1 - Frank, Mario T1 - Axiom relevance decision engine : technical report N2 - 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. N2 - Dieser technische Report beschreibt die Konzeption, Implementierung und Evaluation eines Verfahrens zur Auswahl von logischen Formeln bezüglich derer Relevanz für den Beweis einer logischen Formel. Das Verfahren wird ausschließlich für die Prädikatenlogik erster Ordnung angewandt, wenngleich es auch für höherstufige Prädikatenlogiken geeignet ist. Das Verfahren nutzt eine unifikationsbasierte Breitensuche im Graphen wobei jeder Knoten im Graphen ein Prädikat und jede existierende Kante eine Unifizierbarkeitsrelation ist. Ziel des Verfahrens ist die Reduktion einer gegebenen Menge von Formeln auf eine für aktuelle Theorembeweiser handhabbare Größe. Daher ist das Verfahren als Präprozess-Schritt für das automatische Theorembeweisen geeignet. Zur Beschleunigung der Suche wird neben der Standard-Unifikation eine abgeschwächte Unifikation verwendet. Das System wurde während der Weltmeisterschaft der Theorembeweiser im Jahre 2014 (CASC J6) in Manchester zusammen mit dem Theorembeweiser leanCoP eingereicht und konnte leanCoP dabei unterstützen, Probleme zu lösen, die leanCoP alleine nicht handhaben kann. Die Tests mit leanCoP und dem Theorembeweiser E im Nachgang zu der Weltmeisterschaft zeigen, dass das Verfahren unabhängig von dem verwendeten Kalkül ist und bei beiden Theorembeweisern positive Auswirkungen auf die Beweisbarkeit von Problemen mit großen Formelmengen hat. KW - Relevanz KW - Graphensuche KW - Theorembeweisen KW - Preprocessing KW - Unifikation KW - relevance KW - graph-search KW - preprocessing KW - unification KW - theorem Y1 - 2012 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-72128 ER - TY - THES A1 - Frank, Mario T1 - TEMPLAR : efficient determination of relevant axioms in big formula sets for theorem proving N2 - 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. N2 - Dieses Dokument stellt ein System vor, das aus einer (großen) gegebenen Menge von Formeln der klassischen Prädikatenlogik eine Teilmenge auswählt, die für den Beweis einer logischen Formel relevant sind. Ziel des Systems ist, die Beweisbarkeit von Formeln in einer festen Zeitschranke zu ermöglichen oder die Beweissuche durch die eingeschränkte Formelmenge zu beschleunigen. Das Dokument beschreibt die Konzeption, Implementierung und Evaluation des Systems und geht dabei auf die zwei verschiedenen Ansätze zur Auswahl ein. Während das eine Konzept eine Graphensuche wahlweise auf den Negations-Normalformen oder Skolem-Normalformen der Formeln durchführt, indem Pfade von einer Formel zu einer anderen durch Unifikation von Prädikaten gebildet werden, analysiert das andere Konzept die Häufigkeiten von Lexemen und bildet einen Relevanzwert durch Anwendung des in der Computerlinguistik bekannten tf-idf-Maßes. Es werden die Ergebnisse der Weltmeisterschaft der automatischen Theorembeweiser (CADE ATP Systems Competition, CASC-24) vorgestellt und der Effekt des Systems für die Beweissuche analysiert. Weiterhin werden die Ergebnisse der Tests des Systems auf den Problemen der Weltmeisterschaft aus dem Jahre 2012 (CASC-J6) vorgestellt. Es wird darauf basierend evaluiert, inwieweit die Einschränkungen die Theorembeweiser bei dem Beweis komplexer Probleme unterstützen. Letztendlich wird gezeigt, dass das System einerseits positive Effekte für die Theorembeweiser hat und andererseits unabhängig von dem Kalkül ist, den die Theorembeweiser nutzen. Ferner ist der Ansatz unabhängig von der genutzten Logik und kann prinzipiell für alle Stufen der Prädikatenlogik und Aussagenlogik sowie Modallogik genutzt werden. Dieser Aspekt macht den Ansatz universell im automatischen Theorembeweisen nutzbar. Es zeigt sich, dass beide Ansätze zur Auswahl für verschiedene Formelmengen geeignet sind. Es wird auch gezeigt, dass die Kombination beider Ansätze eine signifikante Erhöhung der beweisbaren Formeln zur Folge hat und dass die Auswahl durch die Ansätze mit den Fähigkeiten eines anderen Auswahl-Systems mithalten kann. KW - Theorembeweisen KW - Relevanz KW - Selektion KW - Liguistisch KW - Unifikation KW - relevance KW - selection KW - proving KW - linguistic KW - theorem Y1 - 2013 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus-72112 ER - TY - GEN A1 - Frank, Mario A1 - Kreitz, Christoph T1 - A theorem prover for scientific and educational purposes T2 - Electronic proceedings in theoretical computer science N2 - We present a prototype of an integrated reasoning environment for educational purposes. The presented tool is a fragment of a proof assistant and automated theorem prover. We describe the existing and planned functionality of the theorem prover and especially the functionality of the educational fragment. This currently supports working with terms of the untyped lambda calculus and addresses both undergraduate students and researchers. We show how the tool can be used to support the students' understanding of functional programming and discuss general problems related to the process of building theorem proving software that aims at supporting both research and education. Y1 - 2018 U6 - https://doi.org/10.4204/EPTCS.267.4 SN - 2075-2180 IS - 267 SP - 59 EP - 69 PB - Open Publishing Association CY - Sydney ER - TY - BOOK A1 - Fuhrmann, Michaela A1 - Schubarth, Wilfried A1 - Schulze-Reichelt, Friederike A1 - Mauermeister, Sylvi A1 - Seidel, Andreas A1 - Hartmann, Nina A1 - Erdmann, Melinda A1 - Apostolow, Benjamin A1 - Wagner, Laura A1 - Berndt, Sarah A1 - Wippermann, Melanie A1 - Ratzlaff, Olaf A1 - Lumpe, Matthias A1 - Kirjuchina, Ljuba A1 - Rost, Sophia A1 - Zurek, Peter Paul A1 - Faaß, Marcel A1 - Schellhorn, Sebastian A1 - Frank, Mario A1 - Kreitz, Christoph A1 - Wagner, Nelli A1 - Jenneck, Julia A1 - Kleemann, Katrin A1 - Vock, Miriam A1 - Schröder, Christian A1 - Erdmann, Kathrin A1 - Koziol, Matthias A1 - Meißner, Marlen A1 - Dibiasi, Anna A1 - Unger, Martin A1 - Piskunova, Elena V. A1 - Bahmutskiy, Andrey E. A1 - Bessonova, Ekatarina A. A1 - Borovik, Ludmila K. ED - Schubarth, Wilfried ED - Mauermeister, Sylvi ED - Schulze-Reichelt, Friederike ED - Seidel, Andreas T1 - Alles auf Anfang! BT - Befunde und Perspektiven zum Studieneingang T3 - Potsdamer Beiträge zur Hochschulforschung N2 - Im Zuge der Bologna-Reform ist an Hochschulen vieles in Bewegung gekommen. Studium und Lehre sind stärker ins Blickfeld gerückt. Dabei kommt der Studieneingangsphase besondere Bedeutung zu, werden doch hier die Weichen für ein erfolgreiches Studium gestellt. Deshalb ist es verständlich, dass die Hauptanstrengungen der Hochschulen auf den Studieneingang gerichtet sind – ganz nach dem Motto: „Auf den Anfang kommt es an!“. Konsens herrscht dahingehend, dass der Studieneingang neu zu gestalten ist, doch beim „Wie?“ gibt es unterschiedliche Antworten. Zugleich wird immer deutlicher, dass eine wirksame Neugestaltung der Eingangsphase nur mit einer umfassenden Reform des Studiums gelingen kann. Ziel des vierten Bandes der Potsdamer Beiträge zur Hochschulforschung ist es, eine Zwischenbilanz der Debatte zum Studieneingang zu ziehen. Auf der Basis empirischer Studien werden unterschiedliche Perspektiven auf den Studieneingang eingenommen und Empfehlungen zur Optimierung des Studieneingangs abgeleitet. Die zahlreichen Untersuchungsergebnisse Potsdamer Forschergruppen werden durch weitere nationale sowie internationale Perspektiven ergänzt. Der Band richtet sich an alle, die sich für die Entwicklung an Hochschulen interessieren. T3 - Potsdamer Beiträge zur Hochschulforschung - 4 Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-422965 SN - 978-3-86956-452-4 SN - 2192-1075 SN - 2192-1083 IS - 4 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Kärcher, Oskar A1 - Filstrup, Christopher T. A1 - Brauns, Mario A1 - Tasevska, Orhideja A1 - Patceva, Suzana A1 - Hellwig, Niels A1 - Walz, Ariane A1 - Frank, Karin A1 - Markovic, Danijela T1 - Chlorophyll a relationships with nutrients and temperature, and predictions for lakes across perialpine and Balkan mountain regions JF - Inland Waters N2 - 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. KW - chlorophyll a KW - nutrients KW - Ohrid-Prespa region KW - perialpine lakes KW - water temperature Y1 - 2020 U6 - https://doi.org/10.1080/20442041.2019.1689768 SN - 2044-2041 SN - 2044-205X VL - 10 IS - 1 SP - 29 EP - 41 PB - Taylor & Francis CY - London ER - TY - GEN A1 - Kärcher, Oskar A1 - Filstrup, Christopher T. A1 - Brauns, Mario A1 - Tasevska, Orhideja A1 - Patceva, Suzana A1 - Hellwig, Niels A1 - Walz, Ariane A1 - Frank, Karin A1 - Markovic, Danijela T1 - Chlorophyll a relationships with nutrients and temperature, and predictions for lakes across perialpine and Balkan mountain regions T2 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe N2 - 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. T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 1443 KW - chlorophyll a KW - nutrients KW - Ohrid-Prespa region KW - perialpine lakes KW - water temperature Y1 - 2020 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-515271 SN - 1866-8372 IS - 1 ER - TY - JOUR A1 - Postberg, Frank A1 - Grün, Eberhard A1 - Horanyi, Mihaly A1 - Kempf, Sascha A1 - Krueger, Harald A1 - Schmidt, Jürgen A1 - Spahn, Frank A1 - Srama, Ralf A1 - Sternovsky, Zoltan A1 - Trieloff, Mario T1 - Compositional mapping of planetary moons by mass spectrometry of dust ejecta JF - Planetary and space science N2 - 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. KW - Moon KW - Europa KW - Ganymede KW - Dust KW - Surface composition KW - Spectrometry Y1 - 2011 U6 - https://doi.org/10.1016/j.pss.2011.05.001 SN - 0032-0633 VL - 59 IS - 14 SP - 1815 EP - 1825 PB - Elsevier CY - Oxford ER - TY - BOOK A1 - Rana, Kaushik A1 - Mohapatra, Durga Prasad A1 - Sidorova, Julia A1 - Lundberg, Lars A1 - Sköld, Lars A1 - Lopes Grim, Luís Fernando A1 - Sampaio Gradvohl, André Leon A1 - Cremerius, Jonas A1 - Siegert, Simon A1 - Weltzien, Anton von A1 - Baldi, Annika A1 - Klessascheck, Finn A1 - Kalancha, Svitlana A1 - Lichtenstein, Tom A1 - Shaabani, Nuhad A1 - Meinel, Christoph A1 - Friedrich, Tobias A1 - Lenzner, Pascal A1 - Schumann, David A1 - Wiese, Ingmar A1 - Sarna, Nicole A1 - Wiese, Lena A1 - Tashkandi, Araek Sami A1 - van der Walt, Estée A1 - Eloff, Jan H. P. A1 - Schmidt, Christopher A1 - Hügle, Johannes A1 - Horschig, Siegfried A1 - Uflacker, Matthias A1 - Najafi, Pejman A1 - Sapegin, Andrey A1 - Cheng, Feng A1 - Stojanovic, Dragan A1 - Stojnev Ilić, Aleksandra A1 - Djordjevic, Igor A1 - Stojanovic, Natalija A1 - Predic, Bratislav A1 - González-Jiménez, Mario A1 - de Lara, Juan A1 - Mischkewitz, Sven A1 - Kainz, Bernhard A1 - van Hoorn, André A1 - Ferme, Vincenzo A1 - Schulz, Henning A1 - Knigge, Marlene A1 - Hecht, Sonja A1 - Prifti, Loina A1 - Krcmar, Helmut A1 - Fabian, Benjamin A1 - Ermakova, Tatiana A1 - Kelkel, Stefan A1 - Baumann, Annika A1 - Morgenstern, Laura A1 - Plauth, Max A1 - Eberhard, Felix A1 - Wolff, Felix A1 - Polze, Andreas A1 - Cech, Tim A1 - Danz, Noel A1 - Noack, Nele Sina A1 - Pirl, Lukas A1 - Beilharz, Jossekin Jakob A1 - De Oliveira, Roberto C. L. A1 - Soares, Fábio Mendes A1 - Juiz, Carlos A1 - Bermejo, Belen A1 - Mühle, Alexander A1 - Grüner, Andreas A1 - Saxena, Vageesh A1 - Gayvoronskaya, Tatiana A1 - Weyand, Christopher A1 - Krause, Mirko A1 - Frank, Markus A1 - Bischoff, Sebastian A1 - Behrens, Freya A1 - Rückin, Julius A1 - Ziegler, Adrian A1 - Vogel, Thomas A1 - Tran, Chinh A1 - Moser, Irene A1 - Grunske, Lars A1 - Szárnyas, Gábor A1 - Marton, József A1 - Maginecz, János A1 - Varró, Dániel A1 - Antal, János Benjamin ED - Meinel, Christoph ED - Polze, Andreas ED - Beins, Karsten ED - Strotmann, Rolf ED - Seibold, Ulrich ED - Rödszus, Kurt ED - Müller, Jürgen T1 - HPI Future SOC Lab – Proceedings 2018 N2 - 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. N2 - Das Future SOC Lab am HPI ist eine Kooperation des Hasso-Plattner-Instituts mit verschiedenen Industriepartnern. Seine Aufgabe ist die Ermöglichung und Förderung des Austausches zwischen Forschungsgemeinschaft und Industrie. Am Lab wird interessierten Wissenschaftler:innen eine Infrastruktur von neuester Hard- und Software kostenfrei für Forschungszwecke zur Verfügung gestellt. Dazu zählen Systeme, die im normalen Hochschulbereich in der Regel nicht zu finanzieren wären, bspw. Server mit bis zu 64 Cores und 2 TB Hauptspeicher. Diese Angebote richten sich insbesondere an Wissenschaftler:innen in den Gebieten Informatik und Wirtschaftsinformatik. Einige der Schwerpunkte sind Cloud Computing, Parallelisierung und In-Memory Technologien. In diesem Technischen Bericht werden die Ergebnisse der Forschungsprojekte des Jahres 2018 vorgestellt. Ausgewählte Projekte stellten ihre Ergebnisse am 17. April und 14. November 2018 im Rahmen des Future SOC Lab Tags vor. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 151 KW - Future SOC Lab KW - research projects KW - multicore architectures KW - in-memory technology KW - cloud computing KW - machine learning KW - artifical intelligence KW - Future SOC Lab KW - Forschungsprojekte KW - Multicore Architekturen KW - In-Memory Technologie KW - Cloud Computing KW - maschinelles Lernen KW - künstliche Intelligenz Y1 - 2022 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-563712 SN - 978-3-86956-547-7 SN - 1613-5652 SN - 2191-1665 IS - 151 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Schellhorn, Sebastian A1 - Frank, Mario A1 - Kreitz, Christoph T1 - Brückenkurse für mathematische und informatiknahe Studiengänge JF - Alles auf Anfang! Befunde und Perspektiven zum Studieneingang Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-428538 SN - 978-3-86956-452-4 SN - 2192-1075 SN - 2192-1083 SP - 257 EP - 271 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Semenyshyn, Rostyslav A1 - Hentschel, Mario A1 - Stanglmair, Christoph A1 - Teutsch, Tanja A1 - Tarin, Cristina A1 - Pacholski, Claudia A1 - Giessen, Harald A1 - Neubrech, Frank T1 - In vitro monitoring conformational changes of polypeptide monolayers using infrared plasmonic nanoantennas JF - Nano letters : a journal dedicated to nanoscience and nanotechnology N2 - 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. KW - Plasmonics KW - surface-enhanced infrared absorption spectroscopy KW - proteins KW - conformational changes KW - biosensing Y1 - 2019 U6 - https://doi.org/10.1021/acs.nanolett.8b02372 SN - 1530-6984 SN - 1530-6992 VL - 19 IS - 1 SP - 1 EP - 7 PB - American Chemical Society CY - Washington ER -