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.
Here are some comments on how Tatami tackles the above problems:
- 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.
These facilities provide an innovative approach to distributed theory
production. The potential of the system is much greater than the present
system given the possibility of incorporating other proof tools. The Duck
language and its ability to generate web pages with readable proofs is
especially interesting, and the use of XML for transferring data between proof
systems without having to write parsers should be further explored.
Altogether the user interface encourages the user to work through the examples
and using the links to dig more deeply into aspects of the system which
interest her.
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.
To the Tatami project homepage
To the research projects homepage
Maintained by Joseph Goguen
Last modified: Wed Jan 3 16:32:28 PDT 2001