Search

This article celebrates with obvious joy the role automated reasoning now plays for mathematics and logic. Simultaneously, this article evidences the realization of a dream thought impossible just four decades ago by almost all. But there were believers, including Joerg Siekmann to whom this article is dedicated in honor of his sixtieth birthday. Indeed, today (in the year 2001) a researcher can enlist the aid of an automated reasoning program often with the reward of a new proof or a better proof in some significant aspect. The contributions to mathematics and logic made with an automated reasoning assistant are many, diverse, often significant, and of the type Hilbert would indeed have found most pleasurable. The proofs discovered by W. McCune's OTTER (as well as other programs) are Hilbert-style axiomatic. Further, some of them address Hilbert's twenty-fourth problem (recently unearthed by Rudiger Thiele), which focuses on the completion of simpler proofs. In that regard, as well as others, I offer challenges and open questions, frequently providing appropriate clauses to provide a beginning. [ABSTRACT FROM AUTHOR]

This article focuses on an esoteric but practical use of automated reasoning that may indeed be new to many, especially those concerned primarily with verification of both hardware and software. Specifically, featured are a discussion and some methodology for taking an existing design—of a circuit, a chip, a program, or the like—and refining and improving it in various ways. (Although the methodology is general and does not require the use of a specific program, McCune's program OTTER does offer what is needed. OTTER has played and continues to play the key role in my research, and an interested person can gain access to this program in various ways, not the least of which is through the included CD-ROM in [3].) When success occurs, the result is a new design that may require fewer components, avoid the use of certain costly components, offer more reliability and ease of verification, and, perhaps most important, be more efficient in the contexts of speed and heat generation. Although I have minimal experience in circuit design, circuit validation, program synthesis, program verification, and similar concerns, (at the encouragement of colleagues based on successes to be cited) I present material that might indeed be of substantial interest to manufacturers and programmers. [ABSTRACT FROM AUTHOR]

This article provides evidence for the arrival of automated reasoning. Indeed, one of its primary goals of the early 1960s has been reached: The use of an automated reasoning program frequently leads to significant contributions to mathematics and to logic. In addition, although not clearly an original objective, the use of such a program now plays an important role for chip design and for program verification. That importance can be sharply increased; indeed, in this article we discuss the possible value of automated reasoning to finding better designs of chips, circuits, and computer code. We also provide insight into the mechanisms—in particular, strategy—that have led to numerous successes. To complement the evidence we present and to encourage further research, we offer challenges and open questions for consideration. We include a glimpse of the future and some commentary on the possibly unexpected benefits of automating the search for answers to open questions. [ABSTRACT FROM AUTHOR]

In this chapter we discuss how the correctness of our implementation of Piton is proved. We do not give a complete account of the proof but do give the main lemmas and explain how they are put together. The reader interested in obtaining the mechanically checked Nqthm proof script should see page 16. [ABSTRACT FROM AUTHOR]

To implement Piton on FM9001 we define ‘load'. ‘Load' takes a p-state, a list of natural numbers, boot-lst, and a load address, load-addr, as its input and produces an FM9001 state as its output. ‘Load' carries out four successive transformations starting with the initial p-state and ending with an FM9001 state. Each such transformation is described by a function and ‘load' is the composition of those four functions. The four functions have names that suggest they are transforms from one state space to another. For example, the function ‘p⇒r' transforms p-states to what we call "r-states." We explain these intermediate forms later. [ABSTRACT FROM AUTHOR]

The implementation of Piton on FM9001 is via what we call a "downloader" defined as the function ‘load' in the logic. The function takes a Piton state, a list of natural numbers, called boot-lst, and a number, called load-addr. It generates an FM9001 state or "binary image." [ABSTRACT FROM AUTHOR]

We wish to implement Piton on FM9001. In this chapter we explain how FM9001 works and the sense in which it has been implemented correctly in hardware. This chapter is necessarily only a sketch of a large body of work by Brock and Hunt and reported by them in [7]. [ABSTRACT FROM AUTHOR]

In this chapter we consider an example programming problem and its solution in Piton. The problem is to specify, implement, and verify a program for doing "big number addition." This chapter is a rather long but instructive detour from our main goal of implementing Piton on FM9001 and proving the implementation correct. [ABSTRACT FROM AUTHOR]

Piton is a high-level assembly language for a stack machine. Among the features provided by Piton are: execute-only program spacenamed read/write global data spaces randomly accessed as one-dimensional arraysrecursive subroutine call and returnprovision of named formal parameters and stack-based parameter passingprovision of named temporary variables allocated and initialized to constants on calla user-visible temporary stackseven abstract data types:integersnatural numbersbit vectorsBooleansdata addressesprogram addresses (labels)subroutine namesstack-based instructions for manipulating the various abstract objectsstandard flow-of-control instructionsinstructions for determining resource limitations [ABSTRACT FROM AUTHOR]

In order to specify Piton formally we need a formally defined language. The language must permit us to discuss such concepts as n-tuples, stacks, variable symbols, assignments or bindings, etc. With such a language we could define the semantics of Piton operationally. Such a definition would take the form of a function ‘p' taking two arguments, a formal Piton state, s, and a natural number, n, such that p(s, n) is the result of running the Piton machine n steps starting from s. [ABSTRACT FROM AUTHOR]

Piton is a simple assembly-level programming language for a microprocessor called the FM9001 described at the machine code level. The correctness of the implementation has been proved by a mechanical theorem prover. [ABSTRACT FROM AUTHOR]