Documentation

Reference Manual

The reference manual tries to document the current status of CafeOBJ. It is generated from the in-system help.

PDF Version – HTML Version.

The reference manual is also available as Wiki on Github.

User Manual

A slightly outdated manual targeting new users, which introduces many of the concepts of CafeOBJ in more details.

PDF Version

PTcalc Manual

This manual describes the PTcalc commands for automatic proof search.

PDF Version

Other documents

• CITP manual (in Japanese): PDF Version
• Search predicates (in Japanese): PDF Version
• PigNose manual (in Japanese): the manual of the first-order theorem prover PDF Version
• Syntax Quick Reference: PDF Version
• Commands Quick Reference: PDF Version
• Lemma finding guide (in Japanese): PDF Version
• CafeOBJ namespace (in Japanese): PDF Version

Tutorials

Brief Introduction to CafeOBJ by Takahiro Seino in English and Japanese.

For further tutorial, please see the dedicated section Tutorials.

Publication

• CafeOBJ Report
  The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification
  Amast Series in Computing, Vol.6, World Scientific, 1998
  by Razen Diaconescu and Kokichi Futatsugi
• Other publication can be found at the respective members pages.