[ProofPower] Equational logic

[dtopham]

Sent from my BlackBerry® PlayBook™
www.blackberry.com

---

From: "dtop...@gmail.com" <dtop...@gmail.com>
To: "proofpower@lemma-one.com" <proofpower@lemma-one.com>
Sent: March 31, 2015 2:22 PM
Subject: Re: Proofpower Digest, Vol 91, Issue 10

http://www.cs.cornell.edu/home/gries/Logic/Equational.html

I have been studying the idea of "equational logic" as described in this link by Gries and wonder if anyone has used ProofPower in this way. If so, I would love to see a sample. 

One reason for my interest in this approach is because it seems more in line with proof by induction (which is a major topic of Discrete Math). 

For example, to prove that 2^n > n^2 for n >= 4 using induction seems like it would be clearest using equational logic.

-Dave

Sent from my BlackBerry® PlayBook™
www.blackberry.com

---

From: "proofpower-requ...@lemma-one.com" <proofpower-requ...@lemma-one.com>
To: "proofpower@lemma-one.com" <proofpower@lemma-one.com>
Sent: March 30, 2015 1:09 PM
Subject: Proofpower Digest, Vol 91, Issue 10

Send Proofpower mailing list submissions to
	proofpower@lemma-one.com

To subscribe or unsubscribe via the World Wide Web, visit
	http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
or, via email, send a message with subject or body 'help' to
	proofpower-requ...@lemma-one.com

You can reach the person managing the list at
	proofpower-ow...@lemma-one.com

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Proofpower digest..."


Today's Topics:

   1. Re: ProofPower (and xpp) is a great program! (Rob Arthan)
   2. Re: Updated Unicode translation scheme (Rob Arthan)


----------------------------------------------------------------------

Message: 1
Date: Mon, 30 Mar 2015 20:10:35 +0100
From: Rob Arthan 
To: David Topham 
Cc: ProofPower List 
Subject: Re: [ProofPower] ProofPower (and xpp) is a great program!
Message-ID: 
Content-Type: text/plain; charset="windows-1252"

David,


On 30 Mar 2015, at 06:05, David Topham  wrote:

> I know I am preaching to the choir here, but I was so impressed by the behavior of ProofPower today I thought I would go ahead and express my appreciation anyway!
> 
> I have been using xpp to prepare notes and exercises for my discrete math course this semester, and today after spending a couple of hours working on a doc with some recursive functions in SML and inductive proofs in Latex, my xpp froze up!  I don't know why, but I thought I was doomed.  Then, magically, as I gave up and killed the process I saw the wonderful message:  
>             xpp-panic-problem_3_1_10.doc-Dq6T0c
> was being saved!
> 
> Thank you, thank you, whoever added in that code to automatically save before dying!
> 
My pleasure! git tells me that that bit of the code will be celebrating its 21st birthday next month.

For future reference, xpp sometimes freezes because a dialogue box asking you for input has got hidden behind other windows. So it?s worth sliding other windows out of the way to see if you can find that dialogue box before killing the process.

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: 

------------------------------

Message: 2
Date: Mon, 30 Mar 2015 21:07:04 +0100
From: Rob Arthan 
To: Anthony Hall 
Cc: ProofPower List 
Subject: Re: [ProofPower] Updated Unicode translation scheme
Message-ID: 
Content-Type: text/plain; charset="utf-8"

Anthony,

On 30 Mar 2015, at 17:54, Anthony Hall  wrote:

> Dear Rob
>  
> I have just one small query - about the minus sign problem

Thanks for your interest.

>  
> I had a lot of trouble with this, as you might expect, when translating between Spivey latex and standard Z, but it can be done.

My problem is that I need a lexical translation scheme that is not just specific to Z, but one that makes sense for any of the open-ended set of languages that ProofPower supports. I certainly don?t want to translate ASCII characters to non-ASCII.

> I don?t know whether translating from Proofpower is more difficult, but it would be nice to get this right if possible while you are translating to Unicode.

I just don?t think ISO Z got this right. It is easy to design a grammar that allows the same symbol (a minus sign) to function both as an infix operator and a prefix operator. However, I failed to realise the importance of this before the Standards committee ran off and committed to the backwards incompatible change that gave you ?a lot of trouble".

> Or am I missing something?

As I said in a recent post to Phil Clayton, I abandoned my half-hearted hopes of providing Unicode support for ProofPower in general and some level of interoperability between ProofPower-Z and ISO Z at the same time. Inside ProofPower, interoperability with ISO Z and ProofPower-Z is best implemented using parsed syntax trees rather than lexical token streams. Of course, perhaps one day, the Z Word Tools as a common front-end will also be an option.
 
>  
> All the best

And to you!

Rob.

>  
> Anthony
>  
>  
> From: Proofpower [mailto:proofpower-boun...@lemma-one.com] On Behalf Of Rob Arthan
> Sent: 28 March 2015 16:03
> To: ProofPower List
> Subject: [ProofPower] Updated Unicode translation scheme
>  
> Dear All,
>  
> Acting on some very helpful comments from Phil Clayton, I have revised the proposed scheme for translating between Unicode and the ProofPower extended character set. The revised scheme is described here:
>  
> http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html
>  
> (You can find the earlier version at http://www.lemma-one.com/ProofPower/unicode/v0/pp-unicode.html)
>  
> The new scheme for you to look at with your e-mail client follows below.
>  
> As before, Mac OS X supports all the necessary glyphs. If you install the STIX fonts on Linux (stix-fonts on Fedora, fonts-stix on Ubuntu), there is now a good chance that you will have all you need.
>  
> Any feedback will be much appreciated.
>  
> Regards,
>  
> Rob.
>  
>  
> 0x80: %subset%: ?
> 0x81: %rsub%: ?
> 0x82: %bagunion%: ?
> 0x83: %bbU%: ?
> 0x84: %Delta%: ?
> 0x85: %fcomp%: ?
> 0x86: %Phi%: ?
> 0x87: %Gamma%: ?
> 0x88: %EZ%: ?
> 0x89: %down%: ?
> 0x8A: %Theta%: ?
> 0x8B: %dcat%: ?/
> 0x8C: %Lambda%: ?
> 0x8D: %mem%: ?
> 0x8E: %notmem%: ?
> 0x8F: %bij%: ?
> 0x90: %Pi%: ?
> 0x91: %SML%: ?
> 0x92: %rres%: ?
> 0x93: %Sigma%: ?
> 0x94: %<:%: ?
> 0x95: %Upsilon%: ?
> 0x96: %boolean%: ?
> 0x97: %Omega%: ?
> 0x98: %Xi%: ?
> 0x99: %Psi%: ?
> 0x9A: %emptyset%: ?
> 0x9B: %up%: ?
> 0x9C: %BHH%: ?
> 0x9D: %SZG%: ?
> 0x9E: %finj%: ?
> 0x9F: %ffun%: ?
> 0xA0: %psubset%: ?
> 0xA1: %intersect%: ?
> 0xA2: %rseq%: ?
> 0xA3: %symdiff%: ?
> 0xA4: %equiv%: ?
> 0xA5: %dintersect%: ?
> 0xA6: %def%: ?
> 0xA7: %lseq%: ?
> 0xA8: %lrelimg%: ?
> 0xA9: %rrelimg%: ?
> 0xAA: %rel%: ?
> 0xAB: %overwrite%: ?
> 0xAC: %<%: ?
> 0xAD: %fun%: ?
> 0xAE: %>%: ?
> 0xAF: %real%: ?
> 0xB0: %EFT%: ?
> 0xB1: %and%: ?
> 0xB2: %or%: ?
> 0xB3: %not%: ?
> 0xB4: %implies%: ?
> 0xB5: %forall%: ?
> 0xB6: %exists%: ?
> 0xB7: %spot%: ?
> 0xB8: %x%: ?
> 0xB9: %SFT%: ?
> 0xBA: %bigcolon%: ?
> 0xBB: %rcomp%: ?
> 0xBC: %leq%: ?
> 0xBD: %neq%: ?
> 0xBE: %geq%: ?
> 0xBF: %symbol%: ?
> 0xC0: %union%: ?
> 0xC1: %alpha%: ?
> 0xC2: %beta%: ?
> 0xC3: %refinedby%: ?
> 0xC4: %delta%: ?
> 0xC5: %select%: ?
> 0xC6: %phi%: ?
> 0xC7: %gamma%: ?
> 0xC8: %eta%: ?
> 0xC9: %iota%: ?
> 0xCA: %theta%: ?
> 0xCB: %kappa%: ?
> 0xCC: %fn%: ?
> 0xCD: %mu%: ?
> 0xCE: %nu%: ?
> 0xCF: %psurj%: ?
> 0xD0: %pi%: ?
> 0xD1: %chi%: ?
> 0xD2: %rho%: ?
> 0xD3: %sigma%: ?
> 0xD4: %tau%: ?
> 0xD5: %upsilon%: ?
> 0xD6: %complex%: ?
> 0xD7: %omega%: ?
> 0xD8: %xi%: ?
> 0xD9: %psi%: ?
> 0xDA: %zeta%: ?
> 0xDB: %SX%: ?
> 0xDC: %BV%: ?
> 0xDD: %EX%: ?
> 0xDE: %dunion%: ?
> 0xDF: %pfun%: ?
> 0xE0: %inj%: ?
> 0xE1: %dsub%: ?
> 0xE2: %bottom%: ?
> 0xE3: %Leftarrow%: ?
> 0xE4: %psupset%: ?
> 0xE5: %supset%: ?
> 0xE6: %fset%: ?
> 0xE7: %uptext%: ?
> 0xE8: %dntext%: ?
> 0xE9: %replacedby%: ?
> 0xEA: %cantext%: ?
> 0xEB: %cat%: ?
> 0xEC: %extract%: ?
> 0xED: %map%: ?
> 0xEE: %nat%: ?
> 0xEF: %surj%: ?
> 0xF0: %pset%: ?
> 0xF1: %SZT%: ?
> 0xF2: %dres%: ?
> 0xF3: %rat%: ?
> 0xF4: %thm%: ?
> 0xF5: %ulbegin%: ?
> 0xF6: %ulend%: ?
> 0xF7: %BT%: ?
> 0xF8: %uminus%: ?
> 0xF9: %filter%: ?
> 0xFA: %int%: ?
> 0xFB: %lbag%: ?
> 0xFC: %BH%: ?
> 0xFD: %rbag%: ?
> 0xFE: %pinj%: ?
> 0xFF: %SZS%: ?
>  
> _______________________________________________
> Proofpower mailing list
> Proofpower@lemma-one.com
> http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

-------------- next part --------------
An HTML attachment was scrubbed...
URL: 

------------------------------

Subject: Digest Footer

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com


------------------------------

End of Proofpower Digest, Vol 91, Issue 10
******************************************

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com