We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to Łukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of Łukasiewicz ’s problem was automatically discovered that is much shorter than any proof found before by man or machine.

This note generalizes factorization for formulas with multiplicities and conjectures that the connection method along with this feature is computationally as powerful as resolution, also seen from a complexity point of view.

We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to {\L}ukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of {\L}ukasiewicz's problem was automatically discovered that is much shorter than any proof found before by man or machine.

Noting that lemmas are a key feature of mathematics, we engage in an investigation of the role of lemmas in automated theorem proving. The paper describes experiments with a combined system involving learning technology that generates useful lemmas for automated theorem provers, demonstrating improvement for several representative systems and solving a hard problem not solved by any system for twenty years. By focusing on condensed detachment problems we simplify the setting considerably, allowing us to get at the essence of lemmas and their role in proof search.

ZusammenfassungVor dem Hintergrund der menschlichen Fähigkeit zur Erweiterung unseres Wissens durch logisches Schließen vermittelt dieser Beitrag einen Überblick der Automatischen Deduktion (AD), eines Teilgebiets der Disziplin der Künstlichen Intelligenz (KI). Er erläutert die Grundmerkmale sowohl der Resolutionsmethode als auch der Konnektionsmethode in der AD und umschreibt deren Varianten und Spezialisierungen sowie die aus der AD hervorgegangenen Beweissysteme, deren Leistungsfähigkeit und vielfältige Anwendungen. Der Text vermittelt zudem einen Einblick in die historische Entwicklung der AD sowie eine Vorstellung von ihrer Rolle, auch im Kontext von Lernverfahren, in der künftigen Entwicklung der KI.

ZusammenfassungDie Erfindung des universellen Komputers hat für die Naturwissenschaft insgesamt eine völlig neue Welt eröffnet, in der eine neue Naturwissenschaft entstanden ist, die vor allem von der Künstlichen Intelligenz (KI) als Disziplin repräsentiert wird. In dieser Arbeit wird sie inhaltlich genauer als Theoriebildung über repräsentierende Objekte (ROBs) charakterisiert, welche sich umfassend nur mit Komputern experimentell überprüfen läßt. Dies wird an unterschiedlichsten Beispielen illustriert, herausragende Aspekte ihrer historischen Entwicklung in den letzten hundert Jahren werden aufgezeigt und ihr aktueller Status wird problematisiert.

The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of “axiom(s) and rule(s) imply goal(s)”. The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by Łukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.

Academic Computer Science emerged in Germany at the end of the 1960s. In 2017, the Munich universities celebrated “50 Years of Computer Science in Munich”. To this occasion various events were held; also, there was a special issue in the Informatik Spektrum, the official journal of the Gesellschaft für Informatik e.V. (GI – the German Society for Computer Science) and of associated organizations, as well as an anthology on Computer Science in Munich [1]. One year later, the present authors published a tribute to the research group for Artificial Intelligence/Intellectics at the TUM in a volume of the Deutsche Museum’s Preprints series [2], of which the present article is a very brief summary—for much more detailed information and impressions of former group members please refer to this booklet. The Munich group for Artificial Intelligence/Intellectics came into being thanks to academic freedom at German universities, in this case the Technical University of Munich (TUM): A single young scientist is enthusiastic about an idea, a new idea, which has not yet been worked on or supported by any professor at the TUM: Artificial Intelligence or Intellectics. The scientist initiates relationships with other colleagues, nationally and internationally; he is successful, receives research funding, and establishes a research group that asserted itself over almost four decades and influenced and advanced the field. The present article provides a brief history of the group.

The article gives a brief account of the historical evolution of Artificial Intelligence in Germany, covering key steps from antiquity to the present state of the discipline. Its focus is on AI as a science and on organisational aspects rather than on technological ones or on specific AI subjects.

The paper envisions a scientific discipline of fundamental importance comparable to Physics or Biology, reminding that a discipline of such a contour was originally intended by the founders of Artificial Intelligence (AI). AI today, however, is far from such an encompassing discipline sharing the respective research interests with at least half a dozen of other disciplines. After the analysis of this situation and its background we discuss the consequences of this splintering by means of selected challenges. We deliberate thereby what could be done to alleviate the disadvantages resulting from the current state of affairs and to leverage AI's current prominence in the public attention to re-engage in the field's broader mission.

Automatic reasoning tools play an important role when developing provably correct software. Both main approaches, program verification and program synthesis employ automated reasoning tools, more specifically, automated theorem provers. Besides classical logic, non-classical logics are particularly relevant in this field. This chapter presents calculi to automate theorem proving in classical and some important non-classical logics, namely first-order intuitionistic and first-order modal logics. These calculi are based on the connection method, which permits a goal-oriented and, hence, a more efficient proof search. The connection calculi for these non-classical logics extend the calculus for classical logic in an elegant and uniform way by adding so-called prefixes to atomic formulae. The leanCoP theorem prover is a very compact PROLOG implementation of the connection calculus for classical logics. We present details of the implementation and describe some basic techniques to improve its efficiency. leanCoP is adapted to non-classical logics by integrating a prefix unification algorithm, which depends on the specific logic. This results in leading theorem provers for the aforementioned non-classical logics.

The paper presents an informal overview of the Connection Method in Automated Deduction. In particular, it points out its unique advantage over competing methods which consists in its formula-orientedness. Among the consequences of this unique feature are three striking advantages, viz. uniformity (over many logics), performance (due to its extreme compactness and goal-orientedness, evidenced by the leanCoP family of provers), and a global view over the proof process (enabling a higher-level guidance of the proof search). These aspects are discussed on the basis of the extensive work accumulated in the literature about this proof method. Along this line of research we envisage a bright future for the field and point out promising directions for future research.

This article explains the relevance of reasoning for prediction and explanation, i.e., for abilities which are fundamental for human survival. Since humans are prone to mistakes in their reasoning, reasoning systems offer desirable support. Deductive reasoning systems operate on a model of reasoning which results from a number of abstractions applied to human reasoning, which concern the language, the inferential relationship, and the syntactic nature of inference. By way of these abstractions, other modes of reasoning such as inductive reasoning are also covered. Basic issues concerning research in deductive systems, their performance and applications are summarized.