Refine
Has Fulltext
- yes (2)
Year of publication
- 2023 (2) (remove)
Document Type
- Bachelor Thesis (2) (remove)
Language
- English (2) (remove)
Is part of the Bibliography
- yes (2)
Keywords
- Arctic aerosol (1)
- Arctic haze (1)
- Fernerkundung (1)
- Gleichheit (1)
- Konnektionskalkül (1)
- Lidar (1)
- Omega (1)
- TPTP (1)
- aerosol: hygroscopic growth (1)
- aerosol: hygroskopisches Wachstum (1)
Institute
In this bachelor’s thesis I implement the automatic theorem prover nanoCoP-Ω. This system is the result of porting arithmetic and equality handling procedures first introduced in the automatic theorem prover with arithmetic leanCoP-Ω into the similar system nanoCoP 2.0. To understand these procedures, I first introduce the mathematical background to both automatic theorem proving and arithmetic expressions. I present the predecessor projects leanCoP, nanoCoP and leanCoP-Ω, out of which nanCoP-Ω was developed. This is followed by an extensive description of the concepts the non-clausal connection calculus needed to be extended by, to allow for proving arithmetic expressions and equalities, as well as of their implementation into nanoCoP-Ω. An extensive comparison between both the runtimes and the number of solved problems of the systems nanoCoP-Ω and leanCoP-Ω was made. I come to the conclusion, that nanoCoP-Ω is considerably faster than leanCoP-Ω for small problems, though less well suited for larger problems. Additionally, I was able to construct a non-theorem that nanoCoP-Ω generates a false proof for. I discuss how this pressing issue could be resolved, as well as some possible optimizations and expansions of the system.
Properties of Arctic aerosol in the transition between Arctic haze to summer season derived by lidar
(2023)
During the Arctic haze period, the Arctic troposphere consists of larger, yet fewer, aerosol particles than during the summer (Tunved et al., 2013; Quinn et al., 2007). Interannual variability (Graßl and Ritter, 2019; Rinke et al., 2004), as well as unknown origins (Stock et al., 2014) and properties of aerosol complicate modeling these annual aerosol cycles. This thesis investigates the modification of the microphysical properties of Arctic aerosols in the transition from Arctic haze to the summer season. Therefore, lidar measurements of Ny-Ålesund from April 2021 to the end of July 2021 are evaluated based on the aerosols’ optical properties. An overview of those properties will be provided. Furthermore, parallel radiosonde data is considered for indication of hygroscopic growth.
The annual aerosol cycle in 2021 differs from expectations based on previous studies from Tunved et al. (2013) and Quinn et al. (2007). Developments of backscatter, extinction, aerosol depolarisation, lidar ratio and color ratio show a return of the Arctic haze in May. The haze had already reduced in April, but regrew afterwards.
The average Arctic aerosol displays hygroscopic behaviour, meaning growth due to water uptake. To determine such a behaviour is generally laborious because various meteorological circumstances need to be considered. Two case studies provide further information on these possible events. In particular, a day with a rare ice cloud and with highly variable water cloud layers is observed.