The reference manual tries to document the current status of CafeOBJ. It is generated from the in-system help.
The reference manual is also available as Wiki on Github.
A slightly outdated manual targeting new users, which introduces many of the concepts of CafeOBJ in more details.
This manual describes the PTcalc commands for automatic proof search.
- 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
Brief Introduction to CafeOBJ by Takahiro Seino in English and Japanese.
For further tutorial, please see the dedicated section Tutorials.
- 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.