Jape is a program which supports the step-by-step interactive development of proofs in formal logics, in the style of proofs-on-paper. It is uncommitted to any particular logic and is customized by a description of a collection of inference rules and the syntax of judgements. It works purely at the surface syntactic level, as a person working on paper might. In that spirit it makes use of explicit visible provisos rather than a conventional encoding of logical properties. Its principal mechanism is unification, employed as a search tool to defer decisions about how to proceed at difficult points in a proof. The design aim is to produce a tool which makes step-by-step proof calculations so straightforward that novices can learn by exploring the use of a pre-encoded logic. Examples of proof development are given in several small logics.

Abstract. GUI design isn't simply a matter of putting a nice front-end on a capable program. It requires thought about the way in which people might be expected to use a system, and investigation of the ways that they actually use it. Jape's GUI has been designed to be as simple as possible, so that it will not get in the way of the business of proof. It is designed to be minimal in the information that it displays and the gestures that it requires from the user. In this paper we introduce and give a rationale for the design of Jape's user interface, then note some of its drawbacks.

A specification of the UNIX filing system is given using a notation based on elementary mathematical set theory. The notation used involves very few special constructs of its own. The specification is detailed enough to capture the filing system's behavior at the system call level, yet abstracts from issues of data representation, whether in programs or on the storage medium, and from the description of any algorithms which might be used to implement the system. The presentation of the specification is in several stages, each new stage building on its predecessors; major concepts are introduced separately so that they may be easily understood. The notation used allows these separate stages to be joined together to give a complete description of each filing system operation-including its error conditions. Features of the specification notation are explained as they are used, and the Appendix gives the definitions of the symbols drawn from set theory.