Dear All,

I am currently working on support for input and output using Unicode into 
ProofPower. I would appreciate any feedback on the translation scheme I am 
proposing to use, which is described here:

I am particularly interested to know how good the coverage for the Unicode 
characters needed is on different systems and on different applications. You 
can see how good your web browser is just by looking at the above Web page, 
which includes GIFs that show how LaTeX renders the ProofPower symbols 
alongside the Unicode translation as rendered by your browser. To see how good 
your mail client is, the following should look something like the HOL 
definition of distributed union:

        ⌜∀ x a⦁ x ∈ ⋃ a ⇔ (∃ s⦁ x ∈ s ∧ s ∈ a)⌝

(There is a complete list of the symbols used at the end of this e-mail.)

Current indications are that Mac OS can do everything that is required, but 
that recent Linux systems and MS Windows tend to miss one or two glyphs: the 
squared upper case letters I am using for some of the quotation symbols seem to 
be poorly supported, for example. Most text editors and word processors on the 
systems I have tried do support UTF-8. If anyone can advise on how to extend 
the range of Unicode glyphs available on Linux or on how to get font 
substitution working nicely with OpenMotif, I would be very grateful.

There is a prototype implementation of the translation as two free-standing 
programs pputf8 and utf8pp here:

(These have been around for a while, but I have just changed them to implement 
the somewhat simplified and extended scheme described in the Web page cited 

My immediate plan is to integrate the translation into ProofPower itself, so 
that Unicode input and output are options you can select with set_flag (similar 
to the way that you can currently select ASCII output, by calling 
set_flag(“use_extended_chars”, false)). I will provide separate flags for input 
and output.

Below, as a further test of your e-mail client, you will find the ASCII 
encoding and UTF-8 encoding of the corresponding Unicode for all the characters 
in the ProofPower extended character set.



%rsub%: ⩥
%bagunion%: ⨄
%bbU%: 𝕌
%Delta%: Δ
%fcomp%: ∘
%Phi%: Φ
%Gamma%: Γ
%down%: ⋎
%Theta%: Θ
%dcat%: ⁀/
%Lambda%: Λ
%mem%: ∈
%notmem%: ∉
%bij%: ⤖
%Pi%: Π
%SML%: 🄼
%rres%: ▷
%Sigma%: Σ
%<:%: 🅃
%Upsilon%: Υ
%boolean%: 𝔹
%Omega%: Ω
%Xi%: Ξ
%Psi%: Ψ
%emptyset%: ∅
%up%: ⋏
%BHH%: ═
%finj%: ⤕
%ffun%: ⇻
%psubset%: ⊂
%intersect%: ∩
%rseq%: 〉
%symdiff%: ⊖
%equiv%: ⇔
%dintersect%: ⋂
%def%: ≜
%lseq%: 〈
%lrelimg%: ⦇
%rrelimg%: ⦈
%rel%: ↔
%overwrite%: ⊕
%<%: ⌜
%fun%: →
%>%: ⌝
%real%: ℝ
%EFT%: █
%and%: ∧
%or%: ∨
%not%: ¬
%implies%: ⇒
%forall%: ∀
%exists%: ∃
%spot%: ⦁
%x%: ×
%SFT%: Ⓢ
%bigcolon%: ⦂
%rcomp%: ⨾
%leq%: ≤
%neq%: ≠
%geq%: ≥
%symbol%: 𝕊
%union%: ∪
%alpha%: α
%beta%: β
%delta%: δ
%select%: ϵ
%phi%: ϕ
%gamma%: γ
%eta%: η
%iota%: ι
%theta%: θ
%kappa%: κ
%fn%: λ
%mu%: μ
%nu%: ν
%psurj%: ⤀
%pi%: π
%chi%: χ
%rho%: ρ
%sigma%: σ
%tau%: τ
%upsilon%: υ
%complex%: ℂ
%omega%: ω
%xi%: ξ
%psi%: φ
%zeta%: ζ
%SX%: ⦏
%BV%: │
%EX%: ⦎
%dunion%: ⋃
%pfun%: ⇸
%inj%: ↣
%dsub%: ⩤
%bottom%: ⊥
%Leftarrow%: ⇐
%psupset%: ⊃
%supset%: ⊇
%fset%: 𝔽
%uptext%: ↗
%dntext%: ↘
%cantext%: ↕
%cat%: ⁀
%extract%: ↿
%map%: ↦
%nat%: ℕ
%surj%: ↠
%pset%: ℙ
%dres%: ◁
%rat%: ℚ
%thm%: ⊢
%ulbegin%: ₍
%ulend%: ₎
%BT%: ├
%uminus%: ﹣
%filter%: ↾
%int%: ℤ
%lbag%: ⟦
%BH%: ─
%rbag%: ⟧
%pinj%: ⤔

Proofpower mailing list

Reply via email to