Towards Proof Planning for ω

This paper describes the proof planning system _ω⁺ for the meta theorem prover for LF implemented in Twelf. The main contributions include a formal system that approximates the flow of information between assumptions and goals within a meta proof, a set of inference rules to reason about those approximations, and a soundness proof that guarantees that the proof planner does not reject promising proof states. Proof planning in _ω⁺ is decidable.     

A Mechanization of Unity in PC-NQTHM-92

This paper presents in detail how the Unity logic for reasoning about concurrent programs was formalized within the mechanized theorem prover PC-NQTHM-92. Most of Unitys proof rules were formalized in the unquantified logic of NQTHM, and the proof system has been used to mechanically verify several concurrent programs. The mechanized proof system is sound by construction, since Unitys proof rules were proved about an operational semantics of concurrency, also presented here. Skolem functions are used instead of quantifiers, and the paper describes how proof rules containing Skolem function are used instead of Unitys quantified proof rules when verifying concurrent programs. This formalization includes several natural extensions to Unity, including nondeterministic statements. The paper concludes with a discussion of the cost and value of mechanization.     

Uniqueness of Normal Proofs in Implicational Intuitionistic Logic

A minimal theorem in a logic L is an L-theorem which is not a non-trivial substitution instance of another L-theorem. Komori (1987) raised the question whether every minimal implicational theorem in intuitionistic logic has a unique normal proof in the natural deduction system NJ. The answer has been known to be partially positive and generally negative. It is shown here that a minimal implicational theorem A in intuitionistic logic has a unique -normal proof in NJ whenever A is provable without non-prime contraction. The non-prime contraction rule in NJ is the implication introduction rule whose cancelled assumption differs from a propositional variable and appears more than once in the proof. Our result improves the known partial positive solutions to Komori's problem. Also, we present another simple example of a minimal implicational theorem in intuitionistic logic which does not have a unique -normal proof in NJ.     

Conquering the Meredith Single Axiom

For more than three and one-half decades, beginning in the early 1960s, a heavy emphasis on proof finding has been a key component of the Argonne paradigm, whose use has directly led to significant advances in automated reasoning and important contributions to mathematics and logic. The theorems studied range from the trivial to the deep, even including some that corresponded to open questions. Often the paradigm asks for a theorem whose proof is in hand but that cannot be obtained in a fully automated manner by the program in use. The theorem whose hypothesis consists solely of the Meredith single axiom for two-valued sentential (or propositional) calculus and whose conclusion is the ukasiewicz three-axiom system for that area of formal logic was just such a theorem. Featured in this article is the methodology that enabled the program OTTER to find the first fully automated proof of the cited theorem, a proof with the intriguing property that none of its steps contains a term of the form n(n(t)) for any term t. As evidence of the power of the new methodology, the article also discusses OTTER's success in obtaining the first known proof of a theorem concerning a single axiom of ukasiewicz.     

Ordinals II: Some applications and a functorial approach

The first part of this paper is a presentation of some common applications of ordinals: definition of a system of ordinal notations for ordinals less than ₀, direct connection between Kruskal's theorem and ₀, consistency proofs in proof theory (such as the consistency of Peano arithmetic by means of transfinite induction up to ₀). In the second part of the paper, a functorial construction of ordinals and in particular of the Veblen hierarchy is explained. This approach, introduced by Girard (theory of dilators), allows the construction of ordinals greater than ₀ to be pursued in a more natural way than if the Bachmann hierarchy is used.     

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.     

Discovering applications of higher order functions through proof planning

The close association between higher order functions (HOFs) and algorithmic skeletons is a promising source of automatic parallelisation of programs. A theorem proving approach to discovering HOFs in functional programs is presented. Our starting point is proof planning, an automated theorem proving technique in which high-level proof plans are used to guide proof search. We use proof planning to identify provably correct transformation rules that introduce HOFs. The approach has been implemented in the Clam proof planner and tested on a range of examples. The work was conducted within the context of a parallelising compiler for Standard ML.Received February 2001Revised March 2004 and November 2004Accepted November 2004 by D. J. Cooke     

The Heine–Borel Challenge Problem. In Honor of Woody Bledsoe

Woody Bledsoes last challenge problem is the analogical transfer of the Heine–Borel theorem for real intervals to the two-dimensional case. This could not be solved by the up-to-then-known techniques of analogical theorem proving. The Heine–Borel theorem is a widely known result in mathematics. It is usually stated in the field of real numbers R¹, and similar versions are also true in R², in topology, and in metric spaces. This article shows how analogy-driven proof plan construction is applicable to this genuinely mathematical problem. Our goal here was to use a source proof plan of HB1 (the Heine–Borel theorem in R¹) as a guide to automatically produce a proof plan of HB2 (the Heine–Borel theorem in R²). We were able to accomplish our goal by generating the target proof plan of HB2 by reformulation and analogical replay.     

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.     

Convergence of fuzzy-pyramid algorithms

Pyramid linking is an important technique for segmenting images and has many applications in image processing and computer vision. The algorithm is closely related to the ISODATA clustering algorithm and shares some of its properties. This paper investigates this relationship and presents a proof of convergence for the pyramid linking algorithm. The convergence of the hard-pyramid linking algorithm has been shown in the past; however, there has been no proof of the convergence of fuzzy-pyramid linking algorithms. The proof of convergence is based on Zangwill's theorem, which describes the convergence of an iterative algorithm in terms of a descent function of the algorithm. We show the existence of such a descent function of the pyramid algorithm and, further, show that all the conditions of Zangwill's theorem are met; hence the algorithm converges.This research was supported by the U.S. Army Research Office under contract DAAL 03-91-G0050.     

Computers,Justification, and Mathematical Knowledge

The original proof of the four-color theorem by Appel and Haken sparked a controversy when Tymoczko used it to argue that the justification provided by unsurveyable proofs carried out by computers cannot be a priori. It also created a lingering impression to the effect that such proofs depend heavily for their soundness on large amounts of computation-intensive custom-built software. Contra Tymoczko, we argue that the justification provided by certain computerized mathematical proofs is not fundamentally different from that provided by surveyable proofs, and can be sensibly regarded as a priori. We also show that the aforementioned impression is mistaken because it fails to distinguish between proof search (the context of discovery) and proof checking (the context of justification). By using mechanized proof assistants capable of producing certificates that can be independently checked, it is possible to carry out complex proofs without the need to trust arbitrary custom-written code. We only need to trust one fixed, small, and simple piece of software: the proof checker. This is not only possible in principle, but is in fact becoming a viable methodology for performing complicated mathematical reasoning. This is evinced by a new proof of the four-color theorem that appeared in 2005, and which was developed and checked in its entirety by a mechanical proof system.

A mechanical proof of Quadratic Reciprocity

We describe the use of the Boyer-Moore theorem prover in mechanically generating a proof of the Law of Quadratic Reciprocity: for distinct odd primes p and q, the congruences x ² q (mod p) and x ² p (mod q) are either both solvable or both unsolvable, unless pq3 (mod 4). The proof is a formalization of an argument due to Eisenstein, based on a lemma of Gauss. The input to the theorem prover consists of nine function definitions, thirty conjectures, and various hints for proving them. The proofs are derived from a library of lemmas that includes Fermat's Theorem and the Gauss Lemma.     

A mechanically verified code generator

We describe the specification, implementation and proof of correctness of a code generator for a subset of Gypsy 2.05. The code generator is specified in the Boyer-Moore logic; its proof is fully machine-checked using the Kaufmann-enhanced Boyer-Moore theorem prover. Our code generator sits atop a stack of verified system components providing a prototype development environment for constructing highly reliable application Programs.     

On the base-dependence of sets of numbers recognizable by finite automata

It is known that the set of powers of two is recognizable by a finite automaton if the notational base used for representing numbers is itself a power of two but is unrecognizable in all other bases. On the other hand, the set of multiples of two is recognizable no matter what the notational base. It is shown that the latter situation is the exception, the former the rule: the only sets recognizable independently of base are those which are ultimately periodic; others, if recognizable at all, are recognizable only in bases which are powers of some fixed positive integer.A somewhat weaker theorem, namely, that a set which is recognizable inn-ary notation for alln 2 is necessarily ultimately periodic, has been established independently by J. Nievergelt using arguments which are simpler than those used here. The proof of the stated theorem given here is itself a substantial simplification over an earlier proof of mine which appeared as IBM Research Note NC-577, Sets Definable by Finite Automata-III, Jan. 1966. The second formulation of the theorem was pointed out by the referee.     

A time-varying Beurling-Lax theorem and a related interpolation problem

This article concerns linear time-varying interpretations of the Beurling-Lax-Ball-Helton theorem and of Sarason's interpolation problem. The former characterizes shift-invariantH ₂ (Krein) subspaces. Unilateral shift invariance reflects both causality and time invariance. Removing the stationarity requirement, a generalized theorem provides a characterization of certain causal subspace families M_t L₂(t, ), t . Sarason's interpolation problem is interpreted here as a search for a (close to) minimal induced norm system, given causal input-output specifications. The Beurling-Lax theorem helps in identifying admissible specification classes. The problem is then reduced to and solved in terms of a linear time-varying Nehari problem. Technically, developments are based on timedomain, state-space methods.This research was supported by the National Science Foundation and by the Army Research Office.     

The notion of proof in hardware verification

Recent advances in the field of hardware verification have raised some fresh (and some familiar) issues concerning the scope and limitations of formal proof. In this article, we discuss in detail some of these issues. We focus particularly on which aspects of hardware and software one can verify, in contrast to the claims that are sometimes made in that regard. Since we consider verification to be one of the more important and promising applications of automated theorem proving — our research has been concerned with this application for a number of years — a precise understanding of verification must be addressed. Although the context for our discussion is the Viper verification project, our remarks apply generally. Viper is a microprocessor designed by W. J. Cullyer, C. Pygott, and J. Kershaw of the Royal Signals and Radar Establishment of the U.K. Ministry of Defence, for use in safety-critical applications. Much to their credit, the designers intended from the start that Viper be formally verified; they presented Viper's more abstract specifications in a language suitable for formal reasoning, and they placed the design in the public domain. Since Viper microprocessors are currently being marketed as verified chips, the need exists to identify precisely to what extent verification is possible. The formal proof aspects of the verification work have been carried out at the Computer Laboratory of the University of Cambridge. To date, some important properties of a register-transfer level model of Viper, relative to a more abstract functional specification, have been proved (by the author) using the HOL proof generating system. Verified systems such as Viper seem likely to become commonplace in the near future. While proofs about the abstract models of such systems are obviously a vital contribution to our trust in them, it is also important (not least in safety-critical applications) that the limitations of the approach be understood.     

Proof movie — A proof with the Boyer-Moore prover

This paper uses the Boyer-Moore prover for developing a proof of correctness for the implementation of a very small compiler. The polished version of the proof is included as an appendix. The major intent of the paper is to describe the process of proving using an automatic theorem prover.This paper presents work done when the author was employed at the University of Kiel, Germany. The research was partially funded by the Commission of the European Communities (CEC) under the ESPRIT programme in the field of Basic Research Action proj. no. 3104, ProCoS: Provably Correct Systems     

Propositional truth maintenance systems: Classification and complexity analysis

Truth maintenance (TM) has been an active area of artificial intelligence (AI) research in recent years. In particular, truth maintenance systems (TMSs) in many variant types have become popular mechanisms for implementing nonmonotonic inference systems. Knowledge about the computational foundations of a TMS is indispensable for their use. We present a classification of computational complexity of tasks performed by basic existing TMS types. Our results include the proof ₂ ^p -completeness of the clause maintenance system's computation task. This is the first problem in AI proved to be ₂ ^p -complete. It is likely to provide a basis for proving ₂ ^p -completeness of other problems in logic and AI. As part of the proof, we prove the ₂ ^p -completeness of the generalized node deletion problem, one of the first natural graph problems to be complete for any one of the classes _i ^p , forp>1. We also prove the polynomial equivalence of Boolean Constraint Propagation-based (logic-based) approaches (LTMSs) and justification-based approaches (JTMSs) to TM, and exhibit efficient algorithms for transforming an LTMS into a JTMS and vice versa.     

A Mechanized Proof Environment for the Convenient Computations Proof Method

A mechanized verification environment made up of theories over the deductive mechanized theorem prover PVS is presented, which allows taking advantage of the convenient computations method. This method reduces the conceptual difficulty of proving a given property for all the possible computations of a system by separating two different concerns: (1) proving that special convenient computations satisfy the property, and (2) proving that every computation is related to a convenient one by a relation which preserves the property. The approach is especially appropriate for applications in which the first concern is trivial once the second has been shown, e.g., where the specification itself is that every computation reduces to a convenient one. Two examples are the serializability of transactions in distributed databases, and sequential consistency of distributed shared memories. To reduce the repetition of effort, a clear separation is made between infrastructural theories to be supplied as a proof environment PVS library to users, and the specification and proof of particular examples. The provided infrastructure formally defines the method in its most general way. It also defines a computation model and a reduction relation—the equivalence of computations that differ only in the order of finitely many independent operations. One way to prove that this relation holds between every computation and some convenient one involves the definition of a measure function from computations into a well-founded set. Two possible default measures, which can be applied in many cases, are also defined in the infrastructure, along with useful lemmas that assist in their usage. We show how the proof environment can be used, by a step-by-step explanation of an application example.