Unicode Mapping for ProofPower
[ProofPower Logo]

Unicode Mapping for ProofPower

The mapping is defined in terms of a basic translation table, which, subject to some additional rules, defines a translation from ProofPower to Unicode or from Unicode to ProofPower. There are some notes giving the rationale for the mapping.

Basic Translation Table

The following table gives a one-to-one mapping from a subset of the ProofPower extended character set to the Unicode character set. The range of the mapping includes all the ProofPower extended characters with the exception of the byte 0x8B.

The LaTeX column contains GIFs showing the typeset form of each character (produced using dvipng). The GIFs should display properly in any browser without any Unicode support. The Unicode column shows the corresponding Unicode glyph as rendered by your web browser.
Byte LaTeX Unicode Code Point Unicode Name
0x80⊆0x002286SUBSET OF OR EQUAL TO
0x81⩥0x002A65Z NOTATION RANGE ANTIRESTRICTION
0x82⊎0x00228EMULTISET UNION
0x83𝕌0x01D54CMATHEMATICAL DOUBLE-STRUCK CAPITAL U
0x84𝛥0x01D6E5MATHEMATICAL ITALIC CAPITAL DELTA
0x85∘0x002218RING OPERATOR
0x86𝛷0x01D6F7MATHEMATICAL ITALIC CAPITAL PHI
0x87𝛤0x01D6E4MATHEMATICAL ITALIC CAPITAL GAMMA
0x88└0x002514BOX DRAWINGS LIGHT UP AND RIGHT
0x89⋎0x0022CECURLY LOGICAL OR
0x8A𝛩0x01D6E9MATHEMATICAL ITALIC CAPITAL THETA
0x8B Translated into a sequence of two code points. See below
0x8C𝛬0x01D6ECMATHEMATICAL ITALIC CAPITAL LAMDA
0x8D∈0x002208ELEMENT OF
0x8E∉0x002209NOT AN ELEMENT OF
0x8F⤖0x002916RIGHTWARDS TWO-HEADED ARROW WITH TAIL
0x90𝛱0x01D6F1MATHEMATICAL ITALIC CAPITAL PI
0x91ⓜ0x0024DCCIRCLED LATIN SMALL LETTER M
0x92▷0x0025B7WHITE RIGHT-POINTING TRIANGLE
0x93𝛴0x01D6F4MATHEMATICAL ITALIC CAPITAL SIGMA
0x94ⓣ0x0024E3CIRCLED LATIN SMALL LETTER T
0x95𝛶0x01D6F6MATHEMATICAL ITALIC CAPITAL UPSILON
0x96𝔹0x01D539MATHEMATICAL DOUBLE-STRUCK CAPITAL B
0x97𝛺0x01D6FAMATHEMATICAL ITALIC CAPITAL OMEGA
0x98𝛯0x01D6EFMATHEMATICAL ITALIC CAPITAL XI
0x99𝛹0x01D6F9MATHEMATICAL ITALIC CAPITAL PSI
0x9A∅0x002205EMPTY SET
0x9B⋏0x0022CFCURLY LOGICAL AND
0x9C═0x002550BOX DRAWINGS DOUBLE HORIZONTAL
0x9D╒0x002552BOX DRAWINGS DOWN SINGLE AND RIGHT DOUBLE
0x9E⤕0x002915RIGHTWARDS ARROW WITH TAIL WITH DOUBLE VERTICAL STROKE
0x9F⇻0x0021FBRIGHTWARDS ARROW WITH DOUBLE VERTICAL STROKE
0xA0⊂0x002282SUBSET OF
0xA1∩0x002229INTERSECTION
0xA2⟩0x0027E9MATHEMATICAL RIGHT ANGLE BRACKET
0xA3⊖0x002296CIRCLED MINUS
0xA4⇔0x0021D4LEFT RIGHT DOUBLE ARROW
0xA5⋂0x0022C2N-ARY INTERSECTION
0xA6≜0x00225CDELTA EQUAL TO
0xA7⟨0x0027E8MATHEMATICAL LEFT ANGLE BRACKET
0xA8⦇0x002987Z NOTATION LEFT IMAGE BRACKET
0xA9⦈0x002988Z NOTATION RIGHT IMAGE BRACKET
0xAA↔0x002194LEFT RIGHT ARROW
0xAB⊕0x002295CIRCLED PLUS
0xAC⌜0x00231CTOP LEFT CORNER
0xAD→0x002192RIGHTWARDS ARROW
0xAE⌝0x00231DTOP RIGHT CORNER
0xAFℝ0x00211DDOUBLE-STRUCK CAPITAL R
0xB0■0x0025A0BLACK SQUARE
0xB1∧0x002227LOGICAL AND
0xB2∨0x002228LOGICAL OR
0xB3¬0x0000ACNOT SIGN
0xB4⇒0x0021D2RIGHTWARDS DOUBLE ARROW
0xB5∀0x002200FOR ALL
0xB6∃0x002203THERE EXISTS
0xB7⦁0x002981Z NOTATION SPOT
0xB8×0x0000D7MULTIPLICATION SIGN
0xB9Ⓢ0x0024C8CIRCLED LATIN CAPITAL LETTER S
0xBA⦂0x002982Z NOTATION TYPE COLON
0xBB⨾0x002A3EZ NOTATION RELATIONAL COMPOSITION
0xBC≤0x002264LESS-THAN OR EQUAL TO
0xBD≠0x002260NOT EQUAL TO
0xBE≥0x002265GREATER-THAN OR EQUAL TO
0xBF𝕊0x01D54AMATHEMATICAL DOUBLE-STRUCK CAPITAL S
0xC0∪0x00222AUNION
0xC1𝛼0x01D6FCMATHEMATICAL ITALIC SMALL ALPHA
0xC2𝛽0x01D6FDMATHEMATICAL ITALIC SMALL BETA
0xC3⊑0x002291SQUARE IMAGE OF OR EQUAL TO
0xC4𝛿0x01D6FFMATHEMATICAL ITALIC SMALL DELTA
0xC5𝜀0x01D700MATHEMATICAL ITALIC SMALL EPSILON
0xC6𝜑0x01D711MATHEMATICAL ITALIC SMALL PHI
0xC7𝛾0x01D6FEMATHEMATICAL ITALIC SMALL GAMMA
0xC8𝜂0x01D702MATHEMATICAL ITALIC SMALL ETA
0xC9𝜄0x01D704MATHEMATICAL ITALIC SMALL IOTA
0xCA𝜃0x01D703MATHEMATICAL ITALIC SMALL THETA
0xCB𝜅0x01D705MATHEMATICAL ITALIC SMALL KAPPA
0xCC𝜆0x01D706MATHEMATICAL ITALIC SMALL LAMDA
0xCD𝜇0x01D707MATHEMATICAL ITALIC SMALL MU
0xCE𝜈0x01D708MATHEMATICAL ITALIC SMALL NU
0xCF⤀0x002900RIGHTWARDS TWO-HEADED ARROW WITH VERTICAL STROKE
0xD0𝜋0x01D70BMATHEMATICAL ITALIC SMALL PI
0xD1𝜒0x01D712MATHEMATICAL ITALIC SMALL CHI
0xD2𝜌0x01D70CMATHEMATICAL ITALIC SMALL RHO
0xD3𝜎0x01D70EMATHEMATICAL ITALIC SMALL SIGMA
0xD4𝜏0x01D70FMATHEMATICAL ITALIC SMALL TAU
0xD5𝜐0x01D710MATHEMATICAL ITALIC SMALL UPSILON
0xD6ℂ0x002102DOUBLE-STRUCK CAPITAL C
0xD7𝜔0x01D714MATHEMATICAL ITALIC SMALL OMEGA
0xD8𝜉0x01D709MATHEMATICAL ITALIC SMALL XI
0xD9𝜓0x01D713MATHEMATICAL ITALIC SMALL PSI
0xDA𝜁0x01D701MATHEMATICAL ITALIC SMALL ZETA
0xDB⦏0x00298FLEFT SQUARE BRACKET WITH TICK IN BOTTOM CORNER
0xDC│0x002502BOX DRAWINGS LIGHT VERTICAL
0xDD⦎0x00298ERIGHT SQUARE BRACKET WITH TICK IN BOTTOM CORNER
0xDE⋃0x0022C3N-ARY UNION
0xDF⇸0x0021F8RIGHTWARDS ARROW WITH VERTICAL STROKE
0xE0↣0x0021A3RIGHTWARDS ARROW WITH TAIL
0xE1⩤0x002A64Z NOTATION DOMAIN ANTIRESTRICTION
0xE2⊥0x0022A5UP TACK
0xE3⇐0x0021D0LEFTWARDS DOUBLE ARROW
0xE4⊃0x002283SUPERSET OF
0xE5⊇0x002287SUPERSET OF OR EQUAL TO
0xE6𝔽0x01D53DMATHEMATICAL DOUBLE-STRUCK CAPITAL F
0xE7↗0x002197NORTH EAST ARROW
0xE8↘0x002198SOUTH EAST ARROW
0xE9≡0x002261IDENTICAL TO
0xEA↕0x002195UP DOWN ARROW
0xEB⁀0x002040CHARACTER TIE
0xEC↿0x0021BFUPWARDS HARPOON WITH BARB LEFTWARDS
0xED↦0x0021A6RIGHTWARDS ARROW FROM BAR
0xEEℕ0x002115DOUBLE-STRUCK CAPITAL N
0xEF↠0x0021A0RIGHTWARDS TWO HEADED ARROW
0xF0ℙ0x002119DOUBLE-STRUCK CAPITAL P
0xF1ⓩ0x0024e9CIRCLED LATIN SMALL LETTER Z
0xF2◁0x0025C1WHITE LEFT-POINTING TRIANGLE
0xF3ℚ0x00211ADOUBLE-STRUCK CAPITAL Q
0xF4⊢0x0022A2RIGHT TACK
0xF5⨽0x002A3DRIGHTHAND INTERIOR PRODUCT
0xF6⨼0x002A3CINTERIOR PRODUCT
0xF7├0x00251CBOX DRAWINGS LIGHT VERTICAL AND RIGHT
0xF8﹣0x00FE63SMALL HYPHEN-MINUS
0xF9↾0x0021BEUPWARDS HARPOON WITH BARB RIGHTWARDS
0xFAℤ0x002124DOUBLE-STRUCK CAPITAL Z
0xFB⟦0x0027E6MATHEMATICAL LEFT WHITE SQUARE BRACKET
0xFC─0x002500BOX DRAWINGS LIGHT HORIZONTAL
0xFD⟧0x0027E7MATHEMATICAL RIGHT WHITE SQUARE BRACKET
0xFE⤔0x002914RIGHTWARDS ARROW WITH TAIL WITH VERTICAL STROKE
0xFF┌0x00250CBOX DRAWINGS LIGHT DOWN AND RIGHT

ProofPower to Unicode

 Translating ProofPower into Unicode converts a stream of bytes into a stream of Unicode code points. An ASCII string of the form "%xHHHHHH%", where HHHHHH is a string of 6 upper-case hexadecimal digits representing a value in the range 0x000100 to 0x10FFFF, is translated into the Unicode code point with that value. Strings of this form are identified reading from left to right. Any byte in the range 0x00 to 0x7F not appearing in such a string is translated into the Unicode code point with the same numeric value. A byte in the range 0x80 to 0xFF other than 0x8B is translated into the Unicode code point identified in the basic translation table above. The byte 0x8B (representing distributed concatenation in Z) is translated into the sequence of 2 Unicode code points shown below:
Byte LaTeX Code Point Sequence Unicode
0x8B0x002040 0x00002F⁀/

Unicode to ProofPower

Translating Unicode converts a stream of code points into a stream of bytes. A Unicode code point in the range 0x000000 to 0x00007F is translated into the byte with the same numeric value. A Unicode code point listed in the Code Point column in the basic translation table is translated into the byte with the numeric value given in the Byte column. A Unicode code point in the range 0x000080 to 0x10FFFF that is not listed in the basic translation table is translated into the ASCII string "%xHHHHHH%", where HHHHHH represents the value of the code point as 6 upper-case hexadecimal digits.

Rationale

The mapping for Z symbols (other than paragraph mark-up) follows the ISO Z Standard Unicode mark-up. An exception is that the ASCII minus sign is translated unchanged while the unary minus sign 0xF8 is translated into SMALL HYPHEN-MINUS. Unfortunately, SMALL HYPHEN-MINUS often seems to be rendered bigger than HYPHEN-MINUS.

Unicode does not provide any single glyphs that resemble the decorated Quine corners provided in the ProofPower character set for quoting HOL types, ML and Z. Squared letters T, M and Z have been used as a convenient single character translation for these.

The %xHHHHHH% format allows any code point to be used in a ProofPower identifier. Strings of this form are highly unlikely to occur in existing scripts and so there is no requirement for a string of this form to be translated into Unicode as 9 ASCII characters.

Thanks to Phil Clayton for valuable comments.
Copyright © Lemma 1 Ltd.
Created by  Rob Arthan [rda at lemma-one dot com]
Last updated: 28th March 2015