On Automating Diagrammatic Proofs of Arithmetic Arguments

Theorems in automated theorem proving are usually proved by formal logical proofs. However, there is a subset of problems which humans can prove by the use of geometric operations on diagrams, so called diagrammatic proofs. Insight is often more clearly perceived in these proofs than in the corresponding algebraic proofs; they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are investigating and automating such diagrammatic reasoning about mathematical theorems. Concrete, rather than general diagrams are used to prove particular concrete instances of the universally quantified theorem. The diagrammatic proof is captured by the use of geometric operations on the diagram. These operations are the inference steps of the proof. An abstracted schematic proof of the universally quantified theorem is induced from these proof instances. The constructive -rule provides the mathematical basis for this step from schematic proofs to theoremhood. In this way we avoid the difficulty of treating a general case in a diagram. One method of confirming that the abstraction of the schematic proof from the proof instances is sound is proving the correctness of schematic proofs in the meta-theory of diagrams. These ideas have been implemented in the system, called Diamond, which is presented here.     

RRTP - A Replacement Rule Theorem Prover

The Replacement Rule Theorem Prover (RRTP) is an instance-based, refutational, first-order clausal theorem prover. The prover is motivated by the idea of selectively replacing predicates by their definitions, and operates by selecting relevant instances of the input clauses. The relevant instances are grounded, if necessary, and tested for unsatisfiability by using a fast propositional calculus decision procedure.     

Induction Proofs with Partial Functions

In this paper we present a method for automated induction proofs about partial functions. We show that most well-known techniques developed for (explicit) induction theorem proving are unsound when dealing with partial functions. But surprisingly, by slightly restricting the application of these techniques, it is possible to develop a calculus for automated induction proofs with partial functions. In particular, under certain conditions one may even generate induction schemes from the recursions of nonterminating algorithms. The need for such induction schemes and the power of our calculus have been demonstrated on a large collection of nontrivial theorems (including Knuth and Bendix's critical pair lemma). In this way, existing induction theorem provers can be directly extended to partial functions without major changes of their logical framework.     

命题时态逻辑定理证明新方法

本文通过对近１０年命题时态逻辑定理证明方法的研究,提出了一种新的证明方法,前人的工作基于对公式的现时部分和后时部分的分解,本文的工作是基于语义反驳树构造。这种新方法为计算机自动证明命题时态逻辑定理,提供了比较好的理论框架．最后还证明了该方法的可靠性和完全性．     

Automated development of Tarski's geometry

Tarski's geometry, a complete first-order axiomatization of Euclidean plane geometry, is developed within the automated reasoning system OTTER. Proofs are obtained and performance statistics supplied for most of the challenge problems appearing in the literature. Few of these problems have been previously solved by any clause-based reasoning system. Further challenges are offered.     

Ascertaining Mathematical Theorems

Whereas to most logicians, the word “theorem” refers to any statement which has been shown to be true, to mathematicians, the word “Theorem” is, relatively speaking, rarely applied, and denotes something far more special. In this paper, we examine some of the underlying reasons behind this difference in terminology, and we show how this discrepancy might be exploited, in order to build a computer system which automatically selects the latter type of “Theorems” from amongst the former. Indeed, we have begun building the automated discovery system MATHsAiD, the design of which is based upon our research. We provide some preliminary results produced by this system, and compare these results to Theorems appearing in various mathematics textbooks.     

Automated reasoning about elementary point-set topology

In this paper we present first-order formulas for basic point-set topology, in an attempt to extend the mathematical range available for exploration with automated theorem-proving programs. We present topology definitions and sample lemmas both in first-order logic and in clausal form. We then illustrate some of the difficulties of these sample lemmas through a proof of a basic lemma in five parts.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38, and by the Division of Educational Programs, Argonne National Laboratory.     

CLIN-E - Smallest Instance First Hyper-Linking

Hyper-linking is an instance-based automated theorem proving strategy that uses unification to generate instances of the input clauses. Lee implemented hyper-linking in the automated theorem prover CLIN, which uses a breadth-first strategy for generating instances of clauses via the hyper-link operation. In attempting to add equality support to CLIN, a number of inefficiencies with Lee's breadth-first strategy for generating instances were encountered. An alternative depth-first strategy, referred to as smallest-instance-first hyper-linking, for generating instances via the hyper-link operation was developed to address these inefficiencies. Smallest-instance-first hyper-linking is implemented in the automated theorem prover CLIN-E.     

出具证明编译器中线性整数命题证明的自动生成

近年来,出具证明编译器作为构建高可信软件的重要途径,逐渐成为编译器理论和形式化验证的研究热点.在其理论框架中,编译器需要借助自动定理证明技术,自动地证明验证条件并生成机器可检查的证明项,因此好的自动定理证明器对出具证明编译器至关重要.本文基于Simplex算法在出具证明编译器的框架内设计并实现了一个支持线性整数命题求解的自动定理证明器,并且提出一套证明项构造方法,将其应用于自动定理证明器中可生成Coq可检查的证明.     

Unsolved problems in elementary number theory

Thirty-two unsolved problems in elementary number theory are listed as challenge problems for automated reasoning systems. The clausal forms of the conjectures and of their negations are given, suitable as input to resolution theorem provers versed in Peano arithmetic.     

Robbins algebra: Conditions that make a near-boolean algebra boolean

Some problems posed years ago remain challenging today. In particular, the Robbins problem, which is still open and which is the focus of attention in this paper, offers interesting challenges for attack with the assistance of an automated reasoning program; for the study presented here, we used the program OTTER. For example, when one submits this problem, which asks for a proof that every Robbins algebra is a Boolean algebra, a large number of deduced clauses results. One must, therefore, consider the possibility that there exists a Robbins algebra that is not Boolean; such an algebra would have to be infinite. One can instead search for properties that, if adjoined to those of a Robbins algebra, guarantee that the algebra is Boolean. Here we present a number of such properties, and we show how an automated reasoning program was used to obtain the corresponding proofs. Additional properties have been identified, and we include here examples of using such a program to check that the corresponding hand-proofs are correct. We present the appropriate input for many of the examples and also include the resulting proofs in clause notation.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The CADE-15 ATP System Competition

The results of the CADE-15 ATP System Competition (CASC-15) are presented.     

The CADE-16 ATP System Competition

The results of the CADE-16 ATP System Competition (CASC-16) are presented.     

Mechanical verification of strategies

This paper presents a method of representing planning domains in the Boyer-Moore logic so that we can prove mechanically whether a strategy solves a problem. Current approaches require explicit frame axioms and state constraints to be included as part of a domain specification and use a programming language for expressing strategies. These make it difficult to specify domains and verify plans efficiently. Our method avoids explicit frame axioms, since domains are specified by programming an interpreter for sequences of actions in the Boyer-Moore logic. Strategies are represented as planners, Lisp programs that take an initial state and other arguments as input and return a sequence of actions that, when executed in the given initial state, will bring about a goal state. Mechanical verification of a strategy is accomplished by proving that the corresponding planner solves all instances of the given problem. We illustrate our approach by verifying strategies in some variations of the blocks world.The work described here was supported in part by NSF Grant MIP-9017499.     

The CADE-17 ATP System Competition

The results of the CADE-17 ATP System Competition (CASC-17) are presented.     

Meeting the challenge of fifty years of logic

In this article, we tell a story of good fortune. The good fortune concerns the discovery of a systematic approach to compress 50 years of excellent research in logic into a single day's use of an automated reasoning program. The discovery resulted from a colleague's experiment with a new representation and a new use of the weighting strategy. The experiment focused on an attempt—which I knew would fail—to prove one of the benchmark theorems that had eluded us for years. Fortunately, I was wrong; my colleague's attempt was successful, and a proof was found. The proof led to proving in one day 13 theorems, theorems that resulted from 50 years of excellent research in logic. We present these theorems as intriguing problems to test the power of a reasoning program or to evaluate the effectiveness of a new idea. In addition to the challenge problems, we discuss a possible approach to finding short proofs and the results achieved with it.This work was supported by the Applied Mathematical Sciences subprogram of the Office of Energy Research, U.S. Department of Energy, under Contract W-31-109-Eng-38.     

The CADE-18 ATP System Competition

The CADE ATP System Competition (CASC) is an annual evaluation of fully automatic, first-order automated theorem-proving (ATP) systems. CASC-18 was the seventh competition in the CASC series. Twenty-four ATP system variants competed in the various competition and demonstration divisions. An outline of the design and a commentated summary of the results are presented. This revised version was published online in August 2006 with corrections to the Cover Date.     

The CADE-14 ATP System Competition

This paper documents the design, competing systems, results, and conclusions of the CADE-14 ATP System Competition (CASC-14).     

The IJCAR ATP System Competition

The results of the IJCAR ATP System Competition are presented.