CafeOBJ 1.5.5 released

We have released a new version of CafeOBJ, which incorporates besides other fixes the following changes:

• Enhancemets of a family of Bool term inspector commands:
  • binspect [ in : <Modexpr> ] <bool-term> . converts given <bool-term> into abstracted xor-and normal form
  • bshow [ tree | grind ] shows abstracted Bool term
  • bresolve [ <num1> [ { <num2> | all } ] ] shows assignments which make abstracted Bool term true
  • bguess { imply | and | or } tries with some heuristics to solve the abstracted Bool term
• bug fix in ACZ rewriting
• CITP changes
  • :ctf [ <term> ] accepts constructors with arguments
  • new command :imply to make instantiated lhs of existing equation of the form eq lhs = true a premise of a goal sentence
  • new tactic rd- which is similar to rd but cancels the normalization of the goal sentence if the sentence is not satisfied
• new switch tree horizontal. if on show term tree displays the term tree structure horizontally (default off).

Please see the [download page for the source release, binary packages, and installation instructions.

CafeOBJ 1.5.5 has already been uploaded to Debian, see http://packages.debian.org/cafeobj. The MacPort is also updated.

Please report bugs to our bug tracker.