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:

## Advertising

http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html 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: https://github.com/RobArthan/pp-contrib (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 above.) 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. Regards, Rob. %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 Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com