Steen, Alexander2021-06-212021-06-212019https://dl.gi.de/handle/20.500.12116/36658Automated theorem proving systems validate or refute whether a conjecture is a logical consequence of a given set of assumptions. Higher-order provers have been successfully applied in academic and industrial applications, such as planning, software and hardware verification, or knowledge-based systems. Recent studies moreover suggest that automation of higher-order logic, in particular, yields effective means for reasoning within expressive non-classical logics, enabling a whole new range of applications, including computer-assisted formal analysis of arguments in metaphysics. My work focuses on the theoretical foundations, effective implementation and practical application of higher-order theorem proving systems. This article briefly introduces higher-order reasoning in general and presents an overview of the design and implementation of the higher-order theorem prover Leo-III. In the second part, some example applications of Leo-III are discussed.enTheorem ProvingAutomated ReasoningHigher-Order LogicNon-Classical LogicsModal LogicsText/Journal Article10.1515/itit-2019-00012196-7032