Logo des Repositoriums

Auflistung nach Autor:in "Steen, Alexander"

1 - 5 von 5
  • Zeitschriftenartikel
    Challenges for Non-Classical Reasoning in Contemporary AI Applications
    (KI - Künstliche Intelligenz: Vol. 38, No. 0, 2024) Steen, Alexander; Benzmüller, Christoph
    In knowledge representation and reasoning, a key area in artificial intelligence research, non-classical logics play a prominent double role: firstly, non-classical logic languages allow for a precise and transparent encoding of domain specific knowledge. Secondly, as the logical languages are equipped with custom-tailored rules of logical inference, they make available a principled approach to derive new knowledge from previous information. In practice, the first aspect addresses data storage and retrieval, the second aspect the utilization of available information. This article briefly surveys contemporary challenges of NCL research in AI.
  • Zeitschriftenartikel
    Extensional Paramodulation for Higher-Order Logic and Its Effective Implementation Leo-III
    (KI - Künstliche Intelligenz: Vol. 34, No. 1, 2020) Steen, Alexander
    Automation of classical higher-order logic faces various theoretical and practical challenges. On a theoretical level, powerful calculi for effective equality reasoning from first-order theorem proving cannot be lifted to the higher-order domain in a simple manner. Practically, implementations of higher-order reasoning systems have to incorporate procedures that often have high time complexity or are not decidable in general. In my dissertation, both the theoretical and the practical challenges of designing an effective higher-order reasoning system are studied. The resulting system, the automated theorem prover Leo-III, is one of the most effective and versatile systems, in terms of supported logical formalisms, to date.
  • Zeitschriftenartikel
    Higher-order theorem proving and its applications
    (it - Information Technology: Vol. 61, No. 4, 2019) Steen, Alexander
    Automated 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.
  • Zeitschriftenartikel
    Non-Classical Reasoning for Contemporary AI Applications
    (KI - Künstliche Intelligenz: Vol. 38, No. 0, 2024) Steen, Alexander; Benzmüller, Christoph
  • Zeitschriftenartikel
    What are Non-classical Logics and Why Do We Need Them? An Extended Interview with Dov Gabbay and Leon van der Torre
    (KI - Künstliche Intelligenz: Vol. 38, No. 0, 2024) Steen, Alexander; Benzmüller, Christoph