Abstract 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.

Abstract 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.

Abstract 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.

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.

Presents a framework for efficiently solving logic formulations of combinatorial optimization problems using heuristic search techniques. In order to integrate cost, lower-bound and upper-bound specifications with conventional logic programming languages, we augment a constraint logic programming (CLP) language with embedded constructs for specifying the cost function and with a few higher-order predicates for specifying the lower and upper bound functions. We illustrate how this simple extension vastly enhances the ease with which optimization problems involving combinations of Min and Max can be specified in the extended language CLP* and we show that CSLDNF (Constraint SLD resolution with Negation as Failure) resolution schemes are not efficient for solving optimization problems specified in this language. Therefore, we describe how any problem specified using CLP* can be converted into an implicit AND/OR graph, and present an algorithm called GenSolve which can branch-and-bound using upper and lower bound estimates, thus exploiting the full pruning power of heuristic search techniques. A technical analysis of GenSolve is provided. We also provide experimental results comparing various control strategies for solving CLP* programs.

This paper addresses and answers a fundamental question about resolution. Informally, what is gained with respect to the search for a proof by performing a single resolution step? It is first shown that any unsatisfiable formula may be decomposed into regular formulas provable in linear time (by resolution). A relevant resolution step strictly reduces at least one of the formulas in the decomposition while an irrelevant one does not contribute to the proof in any way. the relevance of this insight into the nature of resolution and of the unsatisfiability problem for the development of proof strategies and for complexity considerations are briefly discussed. The decomposition also provides a technique for establishing completeness proofs for refinements of resolution. As a first application, connection-graph resolution is shown to be strongly complete. This settles a problem that remained open for two decades despite many proff attempts. The result is relevant for theorem proving because without strong completeness a connection graph resolution prover might run into an infinite loop even on the ground level.

article Free Access Share on On Matrices with Connections Author: Wolfgang Bibel Institut fur Informatik, Technische Universitat Munchen, Arcisstrasse, 8000 Munchen, W Germany and Universitat Karlsruhe, Karlsruhe, West Germany Institut fur Informatik, Technische Universitat Munchen, Arcisstrasse, 8000 Munchen, W Germany and Universitat Karlsruhe, Karlsruhe, West GermanyView Profile Authors Info & Claims Journal of the ACMVolume 28Issue 4Oct. 1981 pp 633–645https://doi.org/10.1145/322276.322277Published:01 October 1981Publication History 125citation490DownloadsMetricsTotal Citations125Total Downloads490Last 12 Months35Last 6 weeks8 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF