[mod.ai] Seminar - Automata Theory, Nuprl Proof Development System

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.
-------