Report on the Tatami System

by Rod Burstall
Professor Emeritus of Computer Science, Edinburgh
December 2000

It is clear that the creation of systematic bodies of mathematical knowledge on computing systems requires the cooperation of a large number of researchers. Let us call such a body including definitions, theorems and proofs a "theory"; the components of a theory may be formal or partly informal and the subject matter may be purely mathematical or refer to some area of computing such as a programming language or a collection of related algorithms. A number of projects have tried to build up theories as a "library" for a particular prover, and the Mizar project originating in Poland has collected machine checked proofs from a considerable number of contributors. The Tatami project aims to take this a step further by allowing theories to be built up using the World Wide Web. It has to address several problems, as follows:

• Proofs may be developed in different logic systems.
• Proofs may be developed by different tools.
• Proofs by one contributor should be intelligible to other contributors.
• Proofs may be a mixture of formal and informal reasoning.

• Tatami provides two logic systems: equational logic based on behavioral equivalence and first order logic with induction. But it provides a general mechanism, the Duck language to define other logics in the same way as first order logic and it provides a Java interface to enable interfacing to other theorem provers using XML.
• Tatami provides a sophisticated web-based browsing system to support documentation of theories. The web pages for proofs can be generated from a script in the Duck language, making the proofs appear in stylised natural language. The application of the rules in Duck ensures that the proof is correct provided that the Duck rules themselves are a proper formulation of the logic. The proof pages generated from Duck scripts incorporate links to specification pages and to an explanatory page for each problem.
• The use of the web and Java makes it possible for a user to follow existing proofs easily and to understand the system by working through examples.

An impressive aspect of Tatami, not discussed above is the BOBJ proof system for behavioural equivalence. It includes an efficient and easy to use algorithm for coinduction, with a more general version of coinduction available through Duck. The behavioral equivalence and hidden algebra features enable one to handle infinite data types such as streams in a natural way, as well as treating objects as in object oriented programming. The induction facilities of OBJ are also available. The system is small and efficient.

In summary, Tatami is an attractive, well designed and well implemented system, making excellent use of the world wide web and the Java programming language. It has a number of ideas which are substantial contributions to the state of the art, and it is unusual in the pains taken to make it accessible over the web to anyone concerned with cooperative development of mathematical theories.