WALDINGER@SRI-WARBUCKS.ARPA.UUCP (07/14/86)
Title: Implementing Automata Theory within the Nuprl Proof Development System Speaker: Christoph Kreitz, Dept. of Computer Science, Cornell University Time: Wednesday, 16 July, 4:15pm (Visitors from outside please come to reception desk a little early. Coffee at 3:45 in Waldinger office) Place: EJ228 (New AI Center Conference Room) SRI International, Building E IMPLEMENTING AUTOMATA THEORY with the Nuprl Proof Development System by Christoph Kreitz Department of Computer Science Cornell University Problem solving is a significant part of science and mathematics and is the most intellectually significant part of programming. Nuprl is a computer system which provides assistance with solving a problem. It supports the creation of formulas, proofs and terms in a formal theory of mathematics; with it one can express concepts associated with definitions, theorems, theories, books and libraries. Moreover the formal theory behind it is sensitive to the computational meaning of terms, assertions and proofs, and the computer system is able to carry out the corresponding actions. Thus Nuprl includes computer-aided program development, but in a broader sense it is a system for proving theorems and implementing mathematics. The actual implementation of a mathematical theory, such as the theory of finite automata, with the Nuprl proof development system gives lots of insights into its strengths and weaknesses and shows that it is powerful enough to obtain nontrivial results within reasonable amounts of time. The talk will give a brief overview of Nuprl, its object language and inference rules (Type Theory), and of features of the computer system itself. These features support partial automatization of the problem solving process and extensions of the object language by a Nuprl user. Details of the implementation of automata theory will be shown afterwards. I will describe some of the techniques and extensions to Nuprl which were necessary to formulate and prove theorems from automata theory. In particular, these techniques keep Nuprl proofs small and understandable. I will present a complete Nuprl proof of the pumping lemma and an evaluation of its computational content as performed on a computer. Finally an outline for possible future developments is given. -------