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:

• using small images (gifs in fact)
• using HTML4 entities
• using the UNICODE character code (in the form �)

ProofPower Special Character Renderings

code	gif		entity		unicode
200	sube		sube	⊆	2286	⊆	subset of or equal to
201	!		!		2A65	⩥	range antirestriction
202	!		!		228E	⊎	multiset union
203	dsu		!		1D54C	𝕌	double struck U
204	udelta		Delta	Δ	0394	Δ	Greek capital delta
205	!		!		!		[not in use?]
206	upsi		Phi	Φ	03A6	Φ	Greek capital phi
207	utau		Gamma	Γ	0393	Γ	Greek capital gamma
210	!		!		!		bottom left corner
211	!		!		22CE	⋎	curly logical or
212	!		Theta	Θ	0398	Θ	greek capital theta
213	!		!		!		distributed concatenation
214	ulambda		Lambda	Λ	039B	Λ	greek capital lambda
215	isin		isin	∈	2208	∈	element of
216	notin		notin	∉	2209	∉	not an element of
217	urarrtl		Rarrtl	⤖	2916	⤖	bijection space constructor
220	upi		Pi	Π	03A0	Π	greek capital letter pi
221	qqml		!		!		ML quote (left ceiling?)
222	!		!		25B7	▷	range restriction (or x22B3 ⊳?)
223	usigma		Sigma	Σ	03A3	Σ	greek capital letter sigma
224	qqco		!		!		type quote (top left crop?)
225	!		upsih	ϒ	03D2	ϒ	greek upsilon (with hook?)
226	dsb		!		1d539	𝔹	double struck B
227	uomega		Omega	Ω	03A9	Ω	greek capital letter omega
230	uchi		Xi	Ξ	039E	Ξ	greek capital letter Xi
231	!		Psi	Ψ	03A8	Ψ	greek capital letter Psi
232	empty		empty	∅	2205	∅	empty set
233	!		!		22CF	⋏	curly logical and
234	!		!		2550	═	bold horizontal double line
235	!		!		!		top left corner with double horizontal
236	nnrarrtl		!		2915	⤕	finite injection space constructor
237	nnrarr		!		21FB	⇻	finite function space constructor
240	sub		sub	⊂	2282	⊂	subset of
241	cap		cap	∩	2229	∩	intersecion
242	!		rang	⟩	232A	〉	right angled bracket (or x3009 〉?)
243	!		!		2296	⊖	circled minus
244	equiv		hArr	⇔	21D4	⇔	equivalent to
245	lcap		!		22C2	⋂	n-ary intersection (large cap)
246	!		!		!		defined as (equal + hat)
247	!		lang	⟨	2329	〈	left angled bracket (or x3008 〈?)
250	!		!		2987	⦇	left half moon bracket
251	!		!		2988	⦈	right half moon bracket
252	leftrightarrow		harr	↔	2194	↔	relation space constructor
253	!		!		2295	⊕	relational override (o + +)
254	qqtel		!		231C	⌜	top left quine corner
255	rarr		rarr	→	2192	→	rightwards arrow
256	qqter		!		231D	⌝	top right quine corner
257	dsr		!		211D	ℝ	the set of real numbers
260	!		!		220E	∎	end of proof (black box)
261	and		and	∧	2227	∧	logical and
262	or		or	∨	2228	∨	logical or
263	not		not	¬	00AC	¬	not
264	ruarr		rArr	⇒	21D2	⇒	implies
265	forall		forall	∀	2200	∀	universal quantification
266	exist		exist	∃	2203	∃	existential quantification
267	bull		bull	•	2022	•	bullet (or x2981 ⦁?)
270	cross		cross	✗	00D7	×	runic cross punctuation
271	!		!		24C8	Ⓢ	circled latin capital letter s
272	!		!		!		type constraint
273	!		fwsemico	&fwsemico;	2A1F	⨟	Z schema composition (or x2A3E ⨾?)
274	le		le	≤	2264	≤	less than or equal to
275	ne		ne	≠	2260	≠	not equal to
276	ge		ge	≥	2265	≥	greater-than or equal to
277	dss		!		1D54A	𝕊	double struck S
300	cup		cup	∪	222A	∪	union
301	alpha		alpha	α	03B1	α	small greek alpha
302	beta		beta	β	03B2	β	small greek beta
303	!		!		!		square less than or equal
304	delta		delta	δ	03B4	δ	small greek delta
305	epsilon		epsilon	ε	03B5	ε	small greek epsilon
306	phi		phi	φ	03C6	φ	small greek phi
307	!		gamma	γ	03B3	γ	small greek gamma
310	!		eta	η	03B7	η	small greek eta
311	iota		iota	ι	03B9	ι	small greek iota
312	theta		theta	θ	03B8	θ	small greek theta
313	!		kappa	κ	03BA	κ	small greek kappa
314	lambda		lambda	λ	03BB	λ	small greek lambda
315	mu		mu	μ	03BC	μ	small greek mu
316	!		nu	ν	03BD	ν	small greek nu
317	nurarr		!		2900	⤀	partial surjection space constructor
320	pi		pi	π	03C0	π	small greek pi
321	!		chi	χ	03C7	χ	small greek chi
322	!		rho	ρ	03C1	ρ	small greek rho
323	!		sigma	σ	03C3	σ	small greek sigma
324	tau		tau	τ	03C4	τ	small greek tau
325	!		!		03C5	υ	small greek upsilon?
326	dsc		!		2102	ℂ	double struck C
327	omega		omega	ω	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	!		!		2577	╷	vertical bar
335	!		!		!		right indexing bracket
336	lcup		!		22C3	⋃	distributed ("n-ary") union
337	nrightarrow		!		21F8	⇸	partial function space constructor (or x219B ↛?)
340	rarrtl		!		21A3	↣	injection space constructor
341	!		!		2A64	⩤	domain co-restriction
342	bottom		perp	⊥	22A5	⊥	bottom or up tack
343	!		lArr	⇐	21D0	⇐	left double arrow
344	!		sup	⊃	2283	⊃	superset
345	!		supe	⊇	2287	⊇	superset or equal
346	fset		!		1D53D	𝔽	finite_subsets *fset
347	!		!		2197	↗	superscript, north east arrow
350	!		!		2198	↘	subscript, south east arrow
351	equiv2		equivalent	&equivalent;	2261	≡	*ppequiv
352	!		sboth	&sboth;	!		endsubsupscript *ppesss
353	!		!		2040	⁀	concatenate, slur, character tie
354	!		!		21BF	↿	sequence extraction, up harpoon with barb left
355	mapsto		!		21A6	↦	maplet, rightward arrow from bar
356	nat		nat	&nat;	2115	ℕ	natural_number *ppnat
357	urarr		Rarr	↠	21A0	↠	surjection
360	pset		!		2119	ℙ	powerset (entity should be dsP?)
361	!		!		!		leftquinecornerz *qqtelz
362	dr		!		25C1	◁	domain restriction (or x22B2 ⊲?)
363	dsq		!		211A	ℚ	double struck Q
364	turnstil		!		22A2	⊢	turnstile (right tack)
365	!		!		!		[not in use?]
366	!		!		!		[not in use?]
366	!		!		!		[not in use?]
371	!		!		21BE	↾	schema projection (or x2A21 ⨡?)
372	dsz		!		2124	ℤ	set of integers
373	!		!		!		double left square bracket
374	!		!		!		horizontal for box
375	!		!		!		double right square bracket
376	nrarrtl		!		2914	⤔	partial injection space constructor
377	qqtel		!		250F	┏	box 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").