Proof Infrastructure for HOL

Lists

I worked with Wai Wong on the HOL theory of lists. It makes heavy use of the higher-order fold functions. Conversions for automatically proving theorems about list operators are provided.

Proof Maintenance

I have examined the problems of maintaining large proof scripts, and implemented tools to ease some of the problems.

Publications

Virtual Theories: Paul Curzon. Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, eds E. Thomas Schubert, Phillip J. Windley and James Alves-Foss, Lecture Notes in Computer Science 971, pp 138-153, Springer-Verlag, 1995.
The Importance of Proof Maintenance and Reengineering: Paul Curzon. International Workshop on Higher Order Logic Theorem Proving and Its Applications: B-Track: Short Presentations, editor Jim Alves-Foss, pp 17-32, 1995.
A Theory of Lists for HOL Based on Higher-Order Functions: Paul Curzon and Wai Wong. In Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications , eds Tom Melham and Juanito Camilleri, 1994.

A Theory of Lists for HOL Based on Higher-Order Functions

Paul Curzon and Wai Wong. Supplementary Proceedings of the 7th International Workshop on Higher Order Logic Theorem Proving and its Applications, eds Tom Melham and Juanito Camilleri, 1994.

Abstract

We describe the new HOL theory of lists. A notable feature is that it is based largely on higher-order functions: `fold left' and `fold right'. By using general theorems about these functions we have been able to provide tools which can quickly prove theorems about both system and user-defined list constants avoiding the need of induction.

Obtaining the paper

An online version of this paper is here.

The poster presented at the conference is here.

Bibtex Entry


@InProceedings{CurzonWong94HUG,

  author = 	 "Paul Curzon and Wai Wong",

  title = 	 "A Theory of Lists for HOL Based on Higher-Order Functions",

  editor = 	 "Tom Melham and Juanito Camilleri",

  booktitle =	 "Supplementary Proceedings of the 7th International Workshop on Higher

		  Order Logic Theorem Proving and its Applications",

  year =	 "1994",

}

The Importance of Proof Maintenance and Reengineering

Paul Curzon. International Workshop on Higher Order Logic Theorem Proving and Its Applications: B-Track: Short Presentations, editor Jim Alves-Foss, pp 17-32, 1995.

Abstract

Our work on the verification of real hardware designs using HOL has resulted in very large proof scripts. Consequently, problems are encountered that are not an issue in smaller verification efforts. In particular, we have found that the maintainability of proofs is of paramount importance. There are many reasons why proof scripts in LCF style theorem provers may be reused. This can be in order to maintain and understand old proofs as well as to speed the creation of new ones. Consequently, proofs should be written in styles that ease their maintainability and make them easier to reuse. Furthermore, proof tools and interfaces should be designed with proof reuse as well as proof creation in mind. Many of the problems can be prevented from occurring in the first place with suitable tool support.

Obtaining the paper

An online version of this paper is here.

Bibtex Entry


@InProceedings{Curzon95HUGM,

  author = 	 "Paul Curzon",

  title = 	 "The Importance of Proof Maintenance and Reengineering",

  editor =	 "Jim Alves-Foss",

  pages =	 "17-32",

  booktitle =	 "International Workshop on Higher Order Logic Theorem Proving

		  and Its Applications: B-Track: Short Presentations",

  year =	 "1995"

}

Virtual Theories

Paul Curzon. Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, eds E. Thomas Schubert, Phillip J. Windley and James Alves-Foss, Lecture Notes in Computer Science 971, pp 138-153, Springer-Verlag, 1995.

Abstract

We present the notion of virtual HOL theories. These give the effect of multiple active theories in a HOL session, helping to correct a major deficiency of the HOL system. They allow the user to switch between different theories at will, proving theorems and making definitions in each virtual theory in turn. The system ensures that proofs only use resources available in the environment of the current virtual theory. The code has been implemented on top of the HOL90 system. A side effect is that a version of autoloading is obtained for HOL90. A more radical feature is the autoloading of tools. The system has been tested on part of a real hardware verification proof.

Obtaining the paper

An online version of this paper is here.

Bibtex Entry




@InProceedings{Curzon95HUGV,

  author = 	 "Paul Curzon",

  title = 	 "Virtual Theories",

  editor =	 "E. Thomas Schubert and Phillip J. Windley and James Alves-Foss",

  volume =	 "971",

 series =	 "Lecture Notes in Computer Science",

  pages =	 "138-153",

  booktitle =	 "Proceedings of the 8th

		  International Workshop on Higher Order Logic Theorem Proving

		  and Its Applications",

  year =	 "1995",

  publisher =	 "Springer-Verlag"

}