(19) A Proof Assistant with Commutative Diagram Interface

[Software Features]

Diagrams are often used in category theory.
Diagrams are intuitive and easily understandable.
Direct manipulation of diagrams are helpful to users.
So, we consider we use diagrams in a proof assistant system.

In this software, diagrams represent equations of morphisms.
Users can prove an equation of morphisms by "paste the diagrams".
Diagrams can be reshaped.

[Required Environment]

This software is written in Java.
This software can work on any Java executable browser.

[File Configuration]

welcome.html    Start file for this software.
                Please open this file on a java executable browser.
                You can execute this software.
                You can look at source files, usages and examples.(in Japanese)
example2.html   Main applet.
usage.html      Usage. (in Japanese)
nougaki.html    Purpose of this software. (in Japanese)
lists.html      List of source files.
cell.gif, fuse1.gif, fuse2.gif pictures for welcome.html.
Readme-E        File configuration.
Readme-J        Japanese version of file configuration.
specification   Specification of this software.
*.java          source files.
*.class         compiled files.

[FTP]

• README
• Program and Documents in Japanese 81[K]