Theory Extension in ACL2(r)

ACL2(r) is a modified version of the theorem prover ACL2 that adds support for the irrational numbers using nonstandard analysis. It has been used to prove basic theorems of analysis, as well as the correctness of the implementation of transcendental functions in hardware. This paper presents the logical foundations of ACL2(r). These foundations are also used to justify significant enhancements to ACL2(r).      

A New Approach for Automatic Theorem Proving in Real Geometry

We present a new method for proving geometric theorems in the real plane or higher dimension. The method is derived from elimination set ideas for quantifier elimination in linear and quadratic formulas over the reals. In contrast to other approaches, our method can also prove theorems whose complex analogues fail. Moreover, the problem formulation may involve order inequalities. After specification of independent variables, nondegeneracy conditions are generated automatically. Moreover, when trying to prove conjectures that – apart from nondegeneracy conditions – do not hold in the claimed generality, missing premises are found automatically. We demonstrate the applicability of our method to nontrivial examples.     

Formal Proofs About Rewriting Using ACL2

We present an application of the ACL2 theorem prover to reason about rewrite systems theory. We describe the formalization and representation aspects of our work using the first-order, quantifier-free logic of ACL2 and we sketch some of the main points of the proof effort. First, we present a formalization of abstract reduction systems and then we show how this abstraction can be instantiated to establish results about term rewriting. The main theorems we mechanically proved are Newman's lemma (for abstract reductions) and Knuth–Bendix critical pair theorem (for term rewriting).     

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.     

The CADE-17 ATP System Competition

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

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.     

Induction using term orders

We present a procedure for proving inductive theorems which is based on explicit induction, yet supports mutual induction. Mutual induction allows the postulation of lemmas whose proofs use the theorems ex hypothesi while the theorems themselves use the lemmas. This feature has always been supported by induction procedures based on Knuth-Bendix completion, but these procedures are limited by the use of rewriting (or rewriting-like) inferences. Our procedure avoids this limitation by making explicit the implicit induction realized by these procedures. As a result, arbitrary deduction mechanisms can be used while still allowing mutual induction. A preliminary version of this paper appeared in the proceedings of the 12th Conference on Automated Deduction, A. Bundy, editor. This author was supported by a grant from the Ministère des Affaires Etrangères, France.     

Termination of Nested and Mutually Recursive Algorithms

This paper deals with automated termination analysis for functional programs. Previously developed methods for automated termination proofs of functional programs often fail for algorithms with nested recursion and they cannot handle algorithms with mutual recursion.We show that termination proofs for nested and mutually recursive algorithms can be performed without having to prove the correctness of the algorithms simultaneously. Using this result, nested and mutually recursive algorithms do no longer constitute a special problem and the existing methods for automated termination analysis can be extended to nested and mutual recursion in a straightforward way. We give some examples of algorithms whose termination can now be proved automatically (including well-known challenge problems such as McCarthys f_91 function).     

Conclusions about the CADE-13 ATP System Competition

The CADE-13 ATP System Competition was the first large-scale controlled competition for first-order ATP systems. Many people have commented on various aspects of the competition, including some suggestions for future improvement. These comments, and some discussion of them, are contained in this article. An overview of the major issues that will affect future competitions is given.     

The Procedures of the CADE-13 ATP System Competition

This article describes the practical procedures that were used to run the CADE-13 ATP System Competition. The article describes the hardware and software environments, the system installation, the soundness testing performed, the preparation of problems for the competition, the choice of the number of problems and the time limit, and the execution of the systems.     

The Results - of the CADE-13 ATP System Competition

The CADE-13 ATP System Competition tested 18 ATP systems on 50 theorems, in five competition categories, with a time limit of 300 seconds imposed on each system run. This article records the results of the competition. Some analysis of these results is given, and interesting points are highlighted.     

Set theory in first-order logic: Clauses for Gödel's axioms

In this paper we present a set of clauses for set theory, thus developing a foundation for the expression of most theorems of mathematics in a form acceptable to a resolution-based automated theoren prover. Because Gödel's formulation of set theory permits presentation in a finite number of first-orde formulas, we employ it rather than that of Zermelo-Fraenkel. We illustrate the expressive power of thi formulation by providing statements of some well-known open questions in number theory, and give some intuition about how the axioms are used by including some sample proofs. A small set of challeng problems is also given.     

The Design of the CADE-13 ATP System Competition

Running a competition for automated theorem proving (ATP) systems is a difficult and arguable venture. However, the potential benefits of such an event by far outweigh the controversial aspects. The motivations for running the CADE-13 ATP System Competition were to contribute to the evaluation of ATP systems, to stimulate ATP research and system development, and to expose ATP systems to researchers both within and outside the ATP community. This article identifies and discusses the issues that determine the nature of such a competition. Choices and motivated decisions for the CADE-13 competition, with respect to the issues, are given.     

Ordered Semantic Hyper-Linking

The ordered semantic hyper-linking strategy is complete for first-order logic and accepts a user-specified natural semantics that guides the search for a proof. Any semantics in which the meanings of the function and predicate symbols are computable on ground terms may be used. This instance-based strategy is efficient on near-propositional problems, is goal sensitive, and has an extension to equality and term rewriting. However, it sometimes has difficulty generating large terms. We compare this strategy with some others that use semantic information, and present a proof of soundness and completeness. We also give some theoretical results about the search efficiency of the strategy. Some examples illustrate the performance of the strategy.     

Proof strategies in linear logic

Linear logic, introduced by J.-Y. Girard, is a refinement of classical logic providing means for controlling the allocation of resources. It has aroused considerable interest from both proof theorists and computer scientists. In this paper we investigate methods for automated theorem proving in propositional linear logic. Both the bottom-up (tableaux) and top-down (resolution) proof strategies are analyzed. Various modifications of sequent rules and efficient search strategies are presented along with the experiments performed with the implemented theorem provers.     

A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers

Because of the inherent NP-completeness of SAT, many SAT problems currently cannot be solved in a reasonable time. Usually, in order to tackle a new class of SAT problems, new ad hoc algorithms must be designed. Another way to solve a new problem is to use a generic solver and employ parallelism to reduce the solve time. In this paper we propose a parallelization scheme for a class of SAT solvers based on the DPLL procedure. The scheme uses a dynamic load-balancing mechanism based on work-stealing techniques to deal with the irregularity of SAT problems. We parallelize Satz, one of the best generic SAT solvers, with our scheme to obtain a parallel solver called PSatz. The first experimental results on random 3-SAT problems and a set of well-known structured problems show the efficiency of PSatz. PSatz is freely available and runs on any networked workstations under Unix/Linux.     

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.