Special issue: Formal proof (Q1961912)

This special issue is devoted to papers describing the implementation of a significant proof or theory within a theorem prover. Each contribution consists of two parts: (1) the paper published in this issue, which outlines definitions, proofs, formalization techniques, and so forth in informal mathematical language and (2) the code of the implementation, which is available electronically via the Kluwer Academic Publisher's Web site at \url{http://www.kluweronline.com/issn/0168-7433}. Further references are provided within each individual paper. The articles of this volume will be reviewed individually.