Search

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. [ABSTRACT FROM AUTHOR]

This paper reports on an exploration of Boolos' Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos' and related examples now seems to be within reach of higher-order ATPs. [ABSTRACT FROM AUTHOR]

We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools. This enables the formal analysis and verification of meta-theoretical properties as well as the flexible generation of extensions and labellings with respect to well-known argumentation semantics. [ABSTRACT FROM AUTHOR]

Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with multiple external specialist reasoning systems such as first-order provers and SMT solvers. Leo-III is compatible with the TPTP/TSTP framework for input formats, reporting results and proofs, and standardized communication between reasoning systems, enabling, e.g., proof reconstruction from within proof assistants such as Isabelle/HOL. Leo-III supports reasoning in polymorphic first-order and higher-order logic, in many quantified normal modal logics, as well as in different deontic logics. Its development had initiated the ongoing extension of the TPTP infrastructure to reasoning within non-classical logics. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]