This table shows information about the rendering of the ProofPower special characters in HTML.

ProofPower uses a special 8-bit character set in which the characters below 128 are ascii and those above are a special encoding of a suitable selection of logical or mathematical characters, many of them to represent the characters used in the Z specification language.

ProofPower comes with support for editing documents encoded in this way suitable for providing specification and proof scripts which can be processed by ProofPower, and for processing these documents using LaTeX to give postscript or PDF files. It does not come with any support for rendering such documents in HTML. The RBJones.com web site does make use of documents which are prepared in XML for processing by ProofPower and for presentation via HTML. This was a hack supporting only the subset of characters which happen to have been needed for the material used at RBJones.com, rather than a full implementation of HTML support for ProofPower sources, however, it is gradually getting more comprehensive.

The following table has been prepared to assist in occasional enhancement of this hack and shows which of the ProofPower special characters can be rendered in HTML by each of three methods.

The three methods are:

It would also be possible to select characters from named fonts, but success would depend on what fonts were available on the machine on which the browser was running, so I didn't think this line worth investigating. The present translation algorithms use the first method whenever an image is available, because the other two methods work only on some browsers. If no image is available the bald UNICODE character code is used, because inspection of results on a random selection of browsers suggests that the UNICODE character codes are implemented whenever the corresponding HTML4 entity is but not always vice-versa. Below is also presented information from pp-symbol.ent which consists of the entitiy definitions required for processing XML files including ProofPower source used to generate this web site.
ProofPower Special Character Renderings
codegifentityunicode
200subesube2286subset of or equal to
201! ! 2A65range antirestriction
202! ! 228Emultiset union
203dsu! 1D54C𝕌double struck U
204udeltaDeltaΔ0394ΔGreek capital delta
205! ! ! [not in use?]
206upsiPhiΦ03A6ΦGreek capital phi
207utauGammaΓ0393ΓGreek capital gamma
210! ! ! bottom left corner
211! ! 22CEcurly logical or
212! ThetaΘ0398Θgreek capital theta
213! ! ! distributed concatenation
214ulambdaLambdaΛ039BΛgreek capital lambda
215isinisin2208element of
216notinnotin2209not an element of
217urarrtlRarrtl2916bijection space constructor
220upiPiΠ03A0Πgreek capital letter pi
221qqml! ! ML quote (left ceiling?)
222! ! 25B7range restriction (or x22B3 ⊳?)
223usigmaSigmaΣ03A3Σgreek capital letter sigma
224qqco! ! type quote (top left crop?)
225! upsihϒ03D2ϒgreek upsilon (with hook?)
226dsb! 1d539𝔹double struck B
227uomegaOmegaΩ03A9Ωgreek capital letter omega
230uchiXiΞ039EΞgreek capital letter Xi
231! PsiΨ03A8Ψgreek capital letter Psi
232emptyempty2205empty set
233! ! 22CFcurly logical and
234! ! 2550bold horizontal double line
235! ! ! top left corner with double horizontal
236nnrarrtl! 2915finite injection space constructor
237nnrarr! 21FBfinite function space constructor
240subsub2282subset of
241capcap2229intersecion
242! rang232Aright angled bracket (or x3009 〉?)
243! ! 2296circled minus
244equivhArr21D4equivalent to
245lcap! 22C2n-ary intersection (large cap)
246! ! ! defined as (equal + hat)
247! lang2329left angled bracket (or x3008 〈?)
250! ! 2987left half moon bracket
251! ! 2988right half moon bracket
252leftrightarrowharr2194relation space constructor
253! ! 2295relational override (o + +)
254qqtel! 231Ctop left quine corner
255rarrrarr2192rightwards arrow
256qqter! 231Dtop right quine corner
257dsr! 211Dthe set of real numbers
260! ! 220Eend of proof (black box)
261andand2227logical and
262oror2228logical or
263notnot¬00AC¬not
264ruarrrArr21D2implies
265forallforall2200universal quantification
266existexist2203existential quantification
267bullbull2022bullet (or x2981 ⦁?)
270crosscross00D7×runic cross punctuation
271! ! 24C8circled latin capital letter s
272! ! ! type constraint
273! fwsemico&fwsemico;2A1FZ schema composition (or x2A3E ⨾?)
274lele2264less than or equal to
275nene2260not equal to
276gege2265greater-than or equal to
277dss! 1D54A𝕊double struck S
300cupcup222Aunion
301alphaalphaα03B1αsmall greek alpha
302betabetaβ03B2βsmall greek beta
303! ! ! square less than or equal
304deltadeltaδ03B4δsmall greek delta
305epsilonepsilonε03B5εsmall greek epsilon
306phiphiφ03C6φsmall greek phi
307! gammaγ03B3γsmall greek gamma
310! etaη03B7ηsmall greek eta
311iotaiotaι03B9ιsmall greek iota
312thetathetaθ03B8θsmall greek theta
313! kappaκ03BAκsmall greek kappa
314lambdalambdaλ03BBλsmall greek lambda
315mumuμ03BCμsmall greek mu
316! nuν03BDνsmall greek nu
317nurarr! 2900partial surjection space constructor
320pipiπ03C0πsmall greek pi
321! chiχ03C7χsmall greek chi
322! rhoρ03C1ρsmall greek rho
323! sigmaσ03C3σsmall greek sigma
324tautauτ03C4τsmall greek tau
325! ! 03C5υsmall greek upsilon?
326dsc! 2102double struck C
327omegaomegaω03C9ωomega
330! xiξ03BEξsmall greek xi
331! psiψ03C8ψsmall greek psi
332! zetaζ03B6ζsmall greek zeta
333! ! ! left indexing bracket
334! ! 2577vertical bar
335! ! ! right indexing bracket
336lcup! 22C3distributed ("n-ary") union
337nrightarrow! 21F8partial function space constructor (or x219B ↛?)
340rarrtl! 21A3injection space constructor
341! ! 2A64domain co-restriction
342bottomperp22A5bottom or up tack
343! lArr21D0left double arrow
344! sup2283superset
345! supe2287superset or equal
346fset! 1D53D𝔽finite_subsets *fset
347! ! 2197superscript, north east arrow
350! ! 2198subscript, south east arrow
351equiv2equivalent&equivalent;2261*ppequiv
352! sboth&sboth;! endsubsupscript *ppesss
353! ! 2040concatenate, slur, character tie
354! ! 21BFsequence extraction, up harpoon with barb left
355mapsto! 21A6maplet, rightward arrow from bar
356natnat&nat;2115natural_number *ppnat
357urarrRarr21A0surjection
360pset! 2119powerset (entity should be dsP?)
361! ! ! leftquinecornerz *qqtelz
362dr! 25C1domain restriction (or x22B2 ⊲?)
363dsq! 211Adouble struck Q
364turnstil! 22A2turnstile (right tack)
365! ! ! [not in use?]
366! ! ! [not in use?]
366! ! ! [not in use?]
371! ! 21BEschema projection (or x2A21 ⨡?)
372dsz! 2124set of integers
373! ! ! double left square bracket
374! ! ! horizontal for box
375! ! ! double right square bracket
376nrarrtl! 2914partial injection space constructor
377qqtel! 250Fbox top left corner *qqtel

The following table shows the character entities used in XML source for ProofPower pages on this site. This is in fact the HTML4 entities plus entities for some of the ProofPower symbols which don't appear in HTML4. Not all of these have sensible values, when there is no corresponding UNICODE character or when I just havn't found it yet, and even where I have identified a UNICODE character it is likely not to display correctly in HTML. The ProofPower special entities come first, followed by the HTML4 entities (of which the first is "nbsp").

Listing of Entities in pp-symbol.ent
bbox#x220e black box - end of proof -->
circS#x24c8 circled capital S -->
cross#x00d7× circled capital S -->
dr#x22b2 domain restriction -->
cr#x22b3 codomain restriction -->
lcap#x22c2 distributed intersection -->
lcup#x22c3 distributed union -->
mapsto#x21a6 maplet or order pair constructor, right arrow from bar -->
qqco#x0020 left quine quote with colon (type quotation) -->
qqml#x0020 left quine quote with ML (ML quotation) -->
qqtel#x231C left quine quote (term quotation) -->
qqter#x231D right quine quote (end quotation) -->
turnstil#x22a2 turnstile -->
dsA#x1D538𝔸 double struck capital A -->
dsB#x1D539𝔹 double struck capital B -->
dsC#x2102 double struck capital C (the set of complex numbers) -->
dsF#8230 double struck capital F (finite sets) -->
fset#8230 double struck capital F (finite sets) -->
dsH#x210d double struck capital H (latin capital letter h) -->
nat#x2115 double struck capital N (the set of natural numbers) -->
dsP#x2119 double struck capital P (power set) -->
dsQ#x211a double struck capital Q (the set of rational numbers) -->
dsR#x211d double struck capital R (the set of real numbers) -->
dsS#x1D54A𝕊 double struck capital S -->
dsU#x1D54C𝕌 double struck capital U -->
dsZ#x2124 double struck capital Z (the set of integers) -->
nbsp#160  no-break space = non-breaking space,
iexcl#161¡ inverted exclamation mark, U+00A1 ISOnum -->
cent#162¢ cent sign, U+00A2 ISOnum -->
pound#163£ pound sign, U+00A3 ISOnum -->
curren#164¤ currency sign, U+00A4 ISOnum -->
yen#165¥ yen sign = yuan sign, U+00A5 ISOnum -->
brvbar#166¦ broken bar = broken vertical bar,
sect#167§ section sign, U+00A7 ISOnum -->
uml#168¨ diaeresis = spacing diaeresis,
copy#169© copyright sign, U+00A9 ISOnum -->
ordf#170ª feminine ordinal indicator, U+00AA ISOnum -->
laquo#171« left-pointing double angle quotation mark
not#172¬ not sign = angled dash,
shy#173­ soft hyphen = discretionary hyphen,
reg#174® registered sign = registered trade mark sign,
macr#175¯ macron = spacing macron = overline
deg#176° degree sign, U+00B0 ISOnum -->
plusmn#177± plus-minus sign = plus-or-minus sign,
sup2#178² superscript two = superscript digit two
sup3#179³ superscript three = superscript digit three
acute#180´ acute accent = spacing acute,
micro#181µ micro sign, U+00B5 ISOnum -->
para#182 pilcrow sign = paragraph sign,
middot#183· middle dot = Georgian comma
cedil#184¸ cedilla = spacing cedilla, U+00B8 ISOdia -->
sup1#185¹ superscript one = superscript digit one,
ordm#186º masculine ordinal indicator,
raquo#187» right-pointing double angle quotation mark
frac14#188¼ vulgar fraction one quarter
frac12#189½ vulgar fraction one half
frac34#190¾ vulgar fraction three quarters
iquest#191¿ inverted question mark
Agrave#192À latin capital letter A with grave
Aacute#193Á latin capital letter A with acute,
Acirc#194Â latin capital letter A with circumflex,
Atilde#195Ã latin capital letter A with tilde,
Auml#196Ä latin capital letter A with diaeresis,
Aring#197Å latin capital letter A with ring above
AElig#198Æ latin capital letter AE
Ccedil#199Ç latin capital letter C with cedilla,
Egrave#200È latin capital letter E with grave,
Eacute#201É latin capital letter E with acute,
Ecirc#202Ê latin capital letter E with circumflex,
Euml#203Ë latin capital letter E with diaeresis,
Igrave#204Ì latin capital letter I with grave,
Iacute#205Í latin capital letter I with acute,
Icirc#206Î latin capital letter I with circumflex,
Iuml#207Ï latin capital letter I with diaeresis,
ETH#208Ð latin capital letter ETH, U+00D0 ISOlat1 -->
Ntilde#209Ñ latin capital letter N with tilde,
Ograve#210Ò latin capital letter O with grave,
Oacute#211Ó latin capital letter O with acute,
Ocirc#212Ô latin capital letter O with circumflex,
Otilde#213Õ latin capital letter O with tilde,
Ouml#214Ö latin capital letter O with diaeresis,
times#215× multiplication sign, U+00D7 ISOnum -->
Oslash#216Ø latin capital letter O with stroke
Ugrave#217Ù latin capital letter U with grave,
Uacute#218Ú latin capital letter U with acute,
Ucirc#219Û latin capital letter U with circumflex,
Uuml#220Ü latin capital letter U with diaeresis,
Yacute#221Ý latin capital letter Y with acute,
THORN#222Þ latin capital letter THORN,
szlig#223ß latin small letter sharp s = ess-zed,
agrave#224à latin small letter a with grave
aacute#225á latin small letter a with acute,
acirc#226â latin small letter a with circumflex,
atilde#227ã latin small letter a with tilde,
auml#228ä latin small letter a with diaeresis,
aring#229å latin small letter a with ring above
aelig#230æ latin small letter ae
ccedil#231ç latin small letter c with cedilla,
egrave#232è latin small letter e with grave,
eacute#233é latin small letter e with acute,
ecirc#234ê latin small letter e with circumflex,
euml#235ë latin small letter e with diaeresis,
igrave#236ì latin small letter i with grave,
iacute#237í latin small letter i with acute,
icirc#238î latin small letter i with circumflex,
iuml#239ï latin small letter i with diaeresis,
eth#240ð latin small letter eth, U+00F0 ISOlat1 -->
ntilde#241ñ latin small letter n with tilde,
ograve#242ò latin small letter o with grave,
oacute#243ó latin small letter o with acute,
ocirc#244ô latin small letter o with circumflex,
otilde#245õ latin small letter o with tilde,
ouml#246ö latin small letter o with diaeresis,
divide#247÷ division sign, U+00F7 ISOnum -->
oslash#248ø latin small letter o with stroke,
ugrave#249ù latin small letter u with grave,
uacute#250ú latin small letter u with acute,
ucirc#251û latin small letter u with circumflex,
uuml#252ü latin small letter u with diaeresis,
yacute#253ý latin small letter y with acute,
thorn#254þ latin small letter thorn,
yuml#255ÿ latin small letter y with diaeresis,
quot#34" quotation mark, U+0022 ISOnum -->
gt#62> greater-than sign, U+003E ISOnum -->
apos#39' apostrophe = APL quote, U+0027 ISOnum -->
OElig#338Œ latin capital ligature OE,
oelig#339œ latin small ligature oe, U+0153 ISOlat2 -->
Scaron#352Š latin capital letter S with caron,
scaron#353š latin small letter s with caron,
Yuml#376Ÿ latin capital letter Y with diaeresis,
circ#710ˆ modifier letter circumflex accent,
tilde#732˜ small tilde, U+02DC ISOdia -->
ensp#8194 en space, U+2002 ISOpub -->
emsp#8195 em space, U+2003 ISOpub -->
thinsp#8201 thin space, U+2009 ISOpub -->
zwnj#8204 zero width non-joiner,
zwj#8205 zero width joiner, U+200D NEW RFC 2070 -->
lrm#8206 left-to-right mark, U+200E NEW RFC 2070 -->
rlm#8207 right-to-left mark, U+200F NEW RFC 2070 -->
ndash#8211 en dash, U+2013 ISOpub -->
mdash#8212 em dash, U+2014 ISOpub -->
lsquo#8216 left single quotation mark,
rsquo#8217 right single quotation mark,
sbquo#8218 single low-9 quotation mark, U+201A NEW -->
ldquo#8220 left double quotation mark,
rdquo#8221 right double quotation mark,
bdquo#8222 double low-9 quotation mark, U+201E NEW -->
dagger#8224 dagger, U+2020 ISOpub -->
Dagger#8225 double dagger, U+2021 ISOpub -->
permil#8240 per mille sign, U+2030 ISOtech -->
lsaquo#8249 single left-pointing angle quotation mark,
rsaquo#8250 single right-pointing angle quotation mark,
euro#8364 euro sign, U+20AC NEW -->
fnof#402ƒ latin small letter f with hook = function
Alpha#913Α greek capital letter alpha, U+0391 -->
Beta#914Β greek capital letter beta, U+0392 -->
Gamma#915Γ greek capital letter gamma,
Delta#916Δ greek capital letter delta,
Epsilon#917Ε greek capital letter epsilon, U+0395 -->
Zeta#918Ζ greek capital letter zeta, U+0396 -->
Eta#919Η greek capital letter eta, U+0397 -->
Theta#920Θ greek capital letter theta,
Iota#921Ι greek capital letter iota, U+0399 -->
Kappa#922Κ greek capital letter kappa, U+039A -->
Lambda#923Λ greek capital letter lamda,
Mu#924Μ greek capital letter mu, U+039C -->
Nu#925Ν greek capital letter nu, U+039D -->
Xi#926Ξ greek capital letter xi, U+039E ISOgrk3 -->
Omicron#927Ο greek capital letter omicron, U+039F -->
Pi#928Π greek capital letter pi, U+03A0 ISOgrk3 -->
Rho#929Ρ greek capital letter rho, U+03A1 -->
Sigma#931Σ greek capital letter sigma,
Tau#932Τ greek capital letter tau, U+03A4 -->
Upsilon#933Υ greek capital letter upsilon,
Phi#934Φ greek capital letter phi,
Chi#935Χ greek capital letter chi, U+03A7 -->
Psi#936Ψ greek capital letter psi,
Omega#937Ω greek capital letter omega,
alpha#945α greek small letter alpha,
beta#946β greek small letter beta, U+03B2 ISOgrk3 -->
gamma#947γ greek small letter gamma,
delta#948δ greek small letter delta,
epsilon#949ε greek small letter epsilon,
zeta#950ζ greek small letter zeta, U+03B6 ISOgrk3 -->
eta#951η greek small letter eta, U+03B7 ISOgrk3 -->
theta#952θ greek small letter theta,
iota#953ι greek small letter iota, U+03B9 ISOgrk3 -->
kappa#954κ greek small letter kappa,
lambda#955λ greek small letter lamda,
mu#956μ greek small letter mu, U+03BC ISOgrk3 -->
nu#957ν greek small letter nu, U+03BD ISOgrk3 -->
xi#958ξ greek small letter xi, U+03BE ISOgrk3 -->
omicron#959ο greek small letter omicron, U+03BF NEW -->
pi#960π greek small letter pi, U+03C0 ISOgrk3 -->
rho#961ρ greek small letter rho, U+03C1 ISOgrk3 -->
sigmaf#962ς greek small letter final sigma,
sigma#963σ greek small letter sigma,
tau#964τ greek small letter tau, U+03C4 ISOgrk3 -->
upsilon#965υ greek small letter upsilon,
phi#966φ greek small letter phi, U+03C6 ISOgrk3 -->
chi#967χ greek small letter chi, U+03C7 ISOgrk3 -->
psi#968ψ greek small letter psi, U+03C8 ISOgrk3 -->
omega#969ω greek small letter omega,
thetasym#977ϑ greek theta symbol,
upsih#978ϒ greek upsilon with hook symbol,
piv#982ϖ greek pi symbol, U+03D6 ISOgrk3 -->
bull#8226 bullet = black small circle,
hellip#8230 horizontal ellipsis = three dot leader,
prime#8242 prime = minutes = feet, U+2032 ISOtech -->
Prime#8243 double prime = seconds = inches,
oline#8254 overline = spacing overscore,
frasl#8260 fraction slash, U+2044 NEW -->
weierp#8472 script capital P = power set
image#8465 black-letter capital I = imaginary part,
real#8476 black-letter capital R = real part symbol,
trade#8482 trade mark sign, U+2122 ISOnum -->
alefsym#8501 alef symbol = first transfinite cardinal,
larr#8592 leftwards arrow, U+2190 ISOnum -->
uarr#8593 upwards arrow, U+2191 ISOnum-->
rarr#8594 rightwards arrow, U+2192 ISOnum -->
darr#8595 downwards arrow, U+2193 ISOnum -->
harr#8596 left right arrow, U+2194 ISOamsa -->
crarr#8629 downwards arrow with corner leftwards
lArr#8656 leftwards double arrow, U+21D0 ISOtech -->
uArr#8657 upwards double arrow, U+21D1 ISOamsa -->
rArr#8658 rightwards double arrow,
dArr#8659 downwards double arrow, U+21D3 ISOamsa -->
hArr#8660 left right double arrow,
forall#8704 for all, U+2200 ISOtech -->
part#8706 partial differential, U+2202 ISOtech -->
exist#8707 there exists, U+2203 ISOtech -->
empty#8709 empty set = null set, U+2205 ISOamso -->
nabla#8711 nabla = backward difference,
isin#8712 element of, U+2208 ISOtech -->
notin#8713 not an element of, U+2209 ISOtech -->
ni#8715 contains as member, U+220B ISOtech -->
prod#8719 n-ary product = product sign,
sum#8721 n-ary summation, U+2211 ISOamsb -->
minus#8722 minus sign, U+2212 ISOtech -->
lowast#8727 asterisk operator, U+2217 ISOtech -->
radic#8730 square root = radical sign,
prop#8733 proportional to, U+221D ISOtech -->
infin#8734 infinity, U+221E ISOtech -->
ang#8736 angle, U+2220 ISOamso -->
and#8743 logical and = wedge, U+2227 ISOtech -->
or#8744 logical or = vee, U+2228 ISOtech -->
cap#8745 intersection = cap, U+2229 ISOtech -->
cup#8746 union = cup, U+222A ISOtech -->
int#8747 integral, U+222B ISOtech -->
there4#8756 therefore, U+2234 ISOtech -->
sim#8764 tilde operator = varies with = similar to,
cong#8773 approximately equal to, U+2245 ISOtech -->
asymp#8776 almost equal to = asymptotic to,
ne#8800 not equal to, U+2260 ISOtech -->
equiv#8801 identical to, U+2261 ISOtech -->
le#8804 less-than or equal to, U+2264 ISOtech -->
ge#8805 greater-than or equal to,
sub#8834 subset of, U+2282 ISOtech -->
sup#8835 superset of, U+2283 ISOtech -->
nsub#8836 not a subset of, U+2284 ISOamsn -->
sube#8838 subset of or equal to, U+2286 ISOtech -->
supe#8839 superset of or equal to,
oplus#8853 circled plus = direct sum,
otimes#8855 circled times = vector product,
perp#8869 up tack = orthogonal to = perpendicular,
sdot#8901 dot operator, U+22C5 ISOamsb -->
lceil#8968 left ceiling = APL upstile,
rceil#8969 right ceiling, U+2309 ISOamsc -->
lfloor#8970 left floor = APL downstile,
rfloor#8971 right floor, U+230B ISOamsc -->
lang#9001 left-pointing angle bracket = bra,
rang#9002 right-pointing angle bracket = ket,
loz#9674 lozenge, U+25CA ISOpub -->
spades#9824 black spade suit, U+2660 ISOpub -->
clubs#9827 black club suit = shamrock,
hearts#9829 black heart suit = valentine,
diams#9830 black diamond suit, U+2666 ISOpub -->