Constructive automata theory implemented with the
NuPRL proof development system. 

Christoph Kreitz  
Technical Report TR 86779, Cornell University, Department of Computer Science, Ithaca, NY, 1986. 

Abstract 

The Nuprl proof development system was designed for the
computerassisted problem solving in mathematics and programming. In
particular it can be used for the development of mathematical proofs
and of programs which are guaranteed to meet their specifications. The
implementation of the theory of finite automata gave lots of insights
into its strengths and weaknesses and shows that Nuprl is indeed
powerful enough now to obtain nontrivial results within reasonable
amounts of time. Its success shall encourage people to actually use
the system and build theories within it. This report describes the
techniques and the userdefined extensions to the Nuprl object
language which were necessary to formulate and prove theorems from the
theory of finite automata. It also describes the experiences which
came from actually working with the current Nuprl system and gave some
useful insights into its strengths and weaknesses. A complete
Nuprlproof of the pumping lemma and its computational evaluation are
presented and an outline for future development is given.

Back to overview of papers 

Bibtex Entry 

@Techreport{tr:Kreitz86a, author = "Christoph Kreitz", title = "Constructive automata theory implemented with the {NuPRL} Proof Development System", institution = "Cornell University. Department of Computer Science", year = 1986, month = "August", number = "TR 86779" } 