Some of the characters used in the BAN logic encoding aren't in widely-available Unicode fonts, and one of them ('says' -- looks a bit like |~) doesn't correspond a single Unicode glyph. This has a severe effect in Linux, Solaris and Windows, and a mild effect in MacOS X (but watch this space :-)).
All the machines we have used are missing or not correctly displaying at least the symbols used in the first four menus (believes, sees, says, and whatever the bar-with-double-arrow is called).
The panels and menus in MacOS X Jape at present use the Konstanz font used in MacOS (Classic) Jape, so they work properly. The menu and window titles are rendered in Unicode, however, and that means that the first four menu titles at least (believes, sees, says, and whatever the bar-with-double-arrow is called) look a bit wonky. (If you're missing more than that, OpenType fonts with lots of characters are available semi-piratically on the web: we aren't telling you where ...)
These problems won't be permanently fixed until there is a widely available freeware universal Unicode font. One's coming, we believe, from ESSTIX. Watch the skies!
If you are desperate to work in BAN logic on Linux or Solaris, the v5 distribution of Jape, available from the Oxford Jape site still works fine. If you need to work in Windows, we've included a BAN_ASCII.jt encoding that uses multi-character sequences to represent the BAN glyphs (but look out: proofs you produce with it won't be readable under the normal BAN encoding). 'Believes' is |=-; 'sees' is <|; 'says' is |~; and the other thing is |=>.
If the BAN_ASCII encoding is still a bit too rich for your machine, send a screenshot to bugs@www.jape.org.uk, and we'll go the extra mile for you. But no complaints about split infinitives, if you want a helpful reply.
Richard Bornat 23.ii.2003