Re: [ProofPower] "Unicode" vs. UTF8

Makarius, Good to hear from you. > On 7 Nov 2023, at 10:09, Makarius wrote: > > On 06/11/2023 02:19, Rob Arthan wrote: >> One bit of burrowing inside instigated by the developers rather than the >> users began a few years ago: an experimental port of ProofPower to use

Re: [ProofPower] Test

with this strand of work again in the not too distant future. Best regards, Rob. > On 6 Nov 2023, at 00:54, Rob Arthan wrote: > > This is an attempt to investigate what happened to the ProofPower mailing > list and to see if I can bring it back to life. > > If you get this me

[ProofPower] Test

This is an attempt to investigate what happened to the ProofPower mailing list and to see if I can bring it back to life. If you get this message please reply. Best regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com

Re: [ProofPower] Law of Cases

David, I think you got some help with this from Roger off the list. I am replying on the list in case you still haven't solved your problem. It looks like you want your law of cases to be a rule that given 훤 ⊢ p ⇒ r and 훥 ⊢ q ⇒ r infers 훤, 훥 ⊢ p ∨ q ⇒ r. Your proposed implementation doesn't

Re: [ProofPower] HOLCONST

David, Phil, Phil's post gives a nice little introduction to programming with conversions (things like plus_1_conv) and conversionals (functions that create new conversions from old like THEN_C). Phil's conversion is focussed and efficient. Going for comfort rather than speed, an alternative

Re: [ProofPower] Proofpower Digest, Vol 120, Issue 1

gest..." > > > Today's Topics: > >1. Testing, testing (Rob Arthan) > > > ---------- > > Message: 1 > Date: Wed, 25 Mar 2020 15:10:15 + > From: Rob Arthan > To: ProofPower Lis

[ProofPower] Testing, testing

This is a test. If you receive it, please ignore it. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] (EXTERNAL) Re: ProofPower and Discrete Math

Roger, David, > On 2 Nov 2019, at 18:45, Roger Bishop Jones wrote: > > Oops. > > On 02/11/2019 17:25, Roger Bishop Jones wrote: >> How about working in theory "ℚ"? > Great idea, apart from the fact that it doesn't exist! That's right: we don't provide a type ℚ of rationals. The approach I

Re: [ProofPower] Proofpower Digest, Vol 119, Issue 1

David, > On 1 Nov 2019, at 16:13, David Topham wrote: > > Ok, I can work within integers for awhile! I was trying to use the general > form of the geometric progression that may involve fractions, but I can > explore whole numbers more first. As an aside from what Roger has been trying to

Re: [ProofPower] Distributed concatenation symbol

Phil, > On 26 Mar 2019, at 17:49, Phil Clayton wrote: > > Rob, > > [A somewhat belated response now. I only noticed the delivery failure from > December 2016 today! Trying again...] Better late than never! > > On 27/11/16 14:21, Rob Arthan wrote: >>

Re: [ProofPower] ProofPower output

by docsml. I would typically copy text out of the journal window and paste it into the script window while writing the document and processing the SML that produces the output interactively. Regards, Rob. > On 15 Feb 2019, at 18:17, David Topham wrote: > > I was reading an article by

Re: [ProofPower] Setting up on macosx Sierra fails...

Hugh, > On 14 May 2017, at 03:21, Hugh Anderson wrote: > > > Hi Phil, > > That does the trick! With polyml it now compiles and installs correctly on my > up-to-date sierra, and the version of Poly/ML that brew installs (5.7). The folk who maintain brew must be very

Re: [ProofPower] Is this a MacOs 10.12 problem?

Steve,Not your ignorance at all. It was a change in clang that came in with Mac OS 10.11.I’d been meaning to issue a fix. I’ve attached a patch. To apply it do: patch -p1 -b -B orig/ < patch-3.1.rda.20170301in the OpenProofPower-3.1w7 directory. Let me know if you have any more

[ProofPower] Distributed concatenation symbol

Dear All, Roger Jones and I are doing some more work on Unicode and UTF-8 support in ProofPower. We are currently considering two changes to the Unicode mapping as currently defined at: http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html

Re: [ProofPower] Font for SML

David, The ProofPower environments use \obeyspaces to persuade LaTeX to honour the spaces in ML code etc. The ffslides package is doing something that is stopping \obeyspaces working properly. A quick fix would be to edit the .tex file (lab.tex in your example) to replace spaces between

Re: [ProofPower] ProofPower and Discrete Math

David, I endorse what Roger said about forward v. backwards proof. There is definitely a tension between teaching proof theory and teaching practical mechanised proof. For the record, the problem was that you had the two theorem arguments of ∃_elim the wrong way round and you seemed to have

Re: [ProofPower] ProofPower on Ubuntu 16.04

Roger, > On 18 Jul 2016, at 22:15, Roger Bishop Jones wrote: > > I have been trying to install ProofPower on Ubuntu 16.04, without success. > > The stumbling block comes early, in the prerequisites for installing > OpenMotif, since some of these are not available in the

Re: [ProofPower] ProofPower build on OS X

ironment. I will look into improving the way I test it. > >> On 30 Apr 2016, at 10:16, Rob Arthan <r...@lemma-one.com >> <mailto:r...@lemma-one.com>> wrote: >> >> > > ... > >> Try it in in src/dev. I think it will fail. If so,

Re: [ProofPower] ProofPower build on OS X

Roger, > On 29 Apr 2016, at 23:16, Roger Bishop Jones <r...@rbjones.com> wrote: > > Rob, > >> On 29 Apr 2016, at 20:31, Rob Arthan <r...@lemma-one.com> wrote: >> >> >> The linker can’t find the gmp library. What version of Poly/ML are you &g

Re: [ProofPower] ProofPower build on OS X

Roger, > On 29 Apr 2016, at 17:17, Roger Bishop Jones wrote: > > Rob, > > OK, so now I am through to the ProofPower build, which fails pretty fast, > just after compiling dtd108. > > Here’s the tail of the log: > > rm -f hol.polydb > Compiling dtd108.sml and imp108.sml > {

Re: [ProofPower] ProofPower on OS X

Roger, > On 28 Apr 2016, at 21:32, Roger Bishop Jones <r...@rbjones.com> wrote: > > >> On 28 Apr 2016, at 11:57, Rob Arthan <r...@lemma-one.com> wrote: >> >> >> Can you point me at the recipe, so I can see what is likely to be >&g

[ProofPower] Attachments

Dear all, I have had a few moderator requests recently for posts to the ProofPower list that were bigger than 40Kb. This was because the posts had attachments of a few hundred Kb. My usual practice is not to accept such posts, not because of the size of the attachments but because such

Re: [ProofPower] Issue in compiling OpenProofPower-3.1w5 on Xubuntu (Ubuntu) 14.04 LTS

Daniel, I am taking the liberty of copying this to the ProofPower mailing list as it may be of interest to other users. Perhaps you might like to join the list and continue the discussion there. Most interactive users of ProofPower need the online documentation and they also want to create

Re: [ProofPower] Question about installation.

On 1 Jun 2015, at 21:31, Robert White ai.robert.wangsh...@gmail.com wrote: This is what I have now. Is this a correct version? Poly/ML 5.2 ReleaseRTS version: X86_64-5.2.1 You need 5.5 or later. So you will need to build it from source. Don’t hesitate to ask if you need any help with

Re: [ProofPower] building error and solution regarding the x11 path for Mac

Yuhui, On 1 Apr 2015, at 23:14, YuHui Lin y@hw.ac.uk wrote: Hi, I’ve got two errors when I install pp, on the latest version of Mac OS 10.10.2. The causes of these two errors are the path of X11 which seems to be different. I am thinking my experience might be helpful, so I share the

Re: [ProofPower] ProofPower (and xpp) is a great program!

David, On 30 Mar 2015, at 06:05, David Topham dtop...@ohlone.edu 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

Re: [ProofPower] Updated Unicode translation scheme

, 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

[ProofPower] Unicode and ProofPower

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: http://www.lemma-one.com/ProofPower/unicode/pp-unicode.html I am particularly

Re: [ProofPower] ProofPower PrettyPrinter

David, On 22 Feb 2015, at 16:47, David Topham dtop...@ohlone.edu wrote: I am trying to get a proof listing (of hypothetical syllogism) for teaching purposes. Thanks to help from Roger, I have the proof working, but would like to use PrettyPrinter to put each step of proof on different

Re: [ProofPower] load proof power with PolyML

Yuhui, On 22 Feb 2013, at 14:24, Yuhui Lin wrote: Hi, I wonder if is possible to load proof power from polyML directly, perhaps by PolyML.make with the proof power source code. I have never tried PolyML.make. There is no reason why you shouldn't compile the ProofPower source code by

Re: [ProofPower] proofpower

Sarah, Why do you keep repeating your questions? If you do not understand the replies that Phil Clayton or Roger Jones provided then respond to their posts and make sure you copy your replies to the mailing list. Also, you have been trying to make a post with a screenshot attached. Please do

Re: [ProofPower] activating templates

Sarah, On Feb 11, 2013, at 9:12 AM, khan khan azurc...@yahoo.com wrote: Hi i have a problem in activating templates in the tools menu PPXpp-2.9.1w2 that i have installed it...the templates in the tools menu is not active...could you please tell me that how to activate it...how to

Re: [ProofPower] activating templates

like you are picking up another program called xpp that is used to configure printers on some Linux distributions. Regards, Rob. thank you sarah --- On Mon, 11/2/13, Rob Arthan r...@lemma-one.com wrote: From: Rob Arthan r...@lemma-one.com Subject: Re: [ProofPower] activating templates

Re: [ProofPower] templates activation problem

On 15 Jan 2013, at 22:12, Phil Clayton wrote: In an X/Motif resource file, I believe '!' starts a comment and include is a macro so must have a '#' before it, as in the Xpp file distributed with ProofPower. That is correct. It may also be worth knowing that the file name in a #include

[ProofPower] Fwd: Motif Released Under LGPL; Updated Version Available Now

See below for some good news. The dependency of xpp on OpenMotif should be much less problematic in the future. Regards, Rob. Begin forwarded message: From: Natalie Adams nata...@ics.com Date: 24 October 2012 18:00:11 GMT+01:00 To: r...@lemma-one.com Subject: Motif Released Under LGPL;

Re: [ProofPower] Trying to Prove my Zed Specifications

On 14 Sep 2012, at 03:01, Jon Lockhart wrote: Phil, Moving them all to there own paragraph worked great. Now I am up to proving the consistency of the axioms, which is where I am run into my next stumbling block. Got the spec load and the consistency goal using the commands no problem.

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, Can you post the actual input that is failing, please. (To protect it in transit, either gzip your .doc file and attach it to your post, or use conv_ascii to convert it into ASCII). Regards, Rob. Regards, Rob. On 3 Sep 2012, at 01:47, Jon Lockhart wrote: Phil, Thanks for the

[ProofPower] Test from lemma-one.com

This is a test please ignore, unless you don't receive it, in which case it would be helpful if you could let me know :-) Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com

Re: [ProofPower] ProofPower Update

On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote: I have now managed to build my theories on the new ProofPower and MathsEgs. I had to modify 13 source files to get them through. It seems probable that the changes all resulted from the new MathsEgs, and primarily were changes to

Re: [ProofPower] Trying to Prove my Zed Specifications

On 18 Aug 2012, at 22:14, Jon Lockhart wrote: Rob, I got a trouble shooting question for you. Been going through the learning documentation this weekend, currently still on the first tutorial wanting to make sure I soak it all in before moving to HOL and Z, but I seem to be running

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On 19 Aug 2012, at 20:51, Jon Lockhart wrote: Roger, Yes, the xpp interface locks. The command executes and then I can't access any of the taps in the journal window, the ML command line will not close, nor can I use the palette I have open either. My first guess is that a

Re: [ProofPower] Trying to Prove my Zed Specifications

at the process id list to see if there was anything besides the one xpp, and there is not, so there is just the one running. I will try and get this gdb installed on my Debian imaged and get back to you. Thanks, Jon On Mon, Aug 20, 2012 at 1:01 PM, Rob Arthan r...@lemma-one.com wrote: Jon

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On 18 Aug 2012, at 22:14, Jon Lockhart wrote: Rob, I got a trouble shooting question for you. Been going through the learning documentation this weekend, currently still on the first tutorial wanting to make sure I soak it all in before moving to HOL and Z, but I seem to be

Re: [ProofPower] Trying to Prove my Zed Specifications

On 13 Aug 2012, at 12:05, Jon Lockhart wrote: Gentlemen, I apologize I should of been more specific at the tasks that I was trying to accomplish and in describing where I am at so far. It seems the first point of business though from what Rob is saying is actually getting the

Re: [ProofPower] Trying to Prove my Zed Specifications

On 13 Aug 2012, at 10:59, Roger Bishop Jones wrote: On Monday 13 Aug 2012 13:12, Rob Arthan wrote: Jon is using Anthony Hall's Z Word Tools, which actually go quite a long way to bridging this gap. Z Word Tools allows you to prepare a Z specification inside a Word document and project out

Re: [ProofPower] Trying to Prove my Zed Specifications

On 13 Aug 2012, at 13:31, Jon Lockhart wrote: Rob, Ok so looks like I am looking to rewrite all my specifications again in ProofPower. A minor inconvenience but should not be a problem. That is likely the quickest way to get started. I will just pop up my specs on one screen and bring

[ProofPower] ProofPower Update

Dear All, I plan to make a new ProofPower release shortly. In the meantime, if you want the state of the art, I uploaded an experimental version built from the latest source. You can find this here: http://www.lemma-one.com/ProofPower/getting/experimental/ The main reason for the experimental

Re: [ProofPower] ProofPower RCS Repository

roger, On 6 Aug 2012, at 14:08, Roger Bishop Jones wrote: On Sunday 05 Aug 2012 15:36, Rob Arthan wrote: If anyone feels minded to look at this and advise how it could be adapted to work with Mercurial or Git, I would be very grateful. My ideal would be to be able to map between Mercurial

[ProofPower] ProofPower RCS Repository

There were some discussions last year about making the ProofPower source repository available online, but this didn't come to anything. The main problem I have is that the popular version control systems (CVS, SVN, Git, Mercurial) don't seem to fit very well with what I have always done

Re: [ProofPower] Trouble Installing on Windows

On 1 Aug 2012, at 04:35, Jon Lockhart wrote: Phil, I ran the original yum setup you gave me. Unfortunately the polyml from the yum install was not placed in the user/lib path, and I could not find it, so I just built a copy of 5.4 myself and was able to get that installed no problem in

Re: [ProofPower] ProofPower in the cloud?

Roger, On 22 Jul 2012, at 10:23, Roger Bishop Jones wrote: Has anyone tried, or even considered, running ProoPower in the Amazon cloud (AWS they call it Amazon Web Services)? They offer a number of Linux images which might be used as starting points. Presumably one could run ProofPower

Re: [ProofPower] Trouble Installing on Windows

John, On 21 Jul 2012, at 17:56, Jon Lockhart wrote: Dear Rob, Thank you for returning my email and the advice you have given. After getting more into the installation I realized that Motiff was not available for Cygwin and I was going to have no interface to work with. I thought maybe

Re: [ProofPower] Trouble Installing on Windows

Jon, On 19 Jul 2012, at 21:57, Jon Lockhart wrote: Dear PP Community, I was wondering if anyone had any help or suggestions for trying to install ProofPower on a Windows machine? I am currently running Windows XP Professional, Service Pack 3, 32-bit. I have downloaded all the

Re: [ProofPower] Scope of variables in Z declaration

On 15 Apr 2012, at 15:21, Roger Bishop Jones wrote: Thanks for your comments on the ProofPower-Z scope rules Phil. I personally believe that the ProofPower position on the scope of variables is preferable to the alternative, for reasons I will come to shortly, but I think it possible

[ProofPower] Fwd: ABZ2012

Begin forwarded message: From: ABZ2012 abz2...@easychair.org Date: 9 January 2012 08:53:58 GMT To: Rob Arthan r...@lemma-one.com Subject: ABZ2012 Dear Rob, after several requests, the ABZ deadline has been extended to Jan. 22. The conference web page will be updated soon. Please

[ProofPower] Fwd: ABZ2012 remind deadline

Begin forwarded message: From: ABZ2012 abz2...@easychair.org Date: 22 December 2011 09:25:34 GMT To: Rob Arthan r...@lemma-one.com Subject: ABZ2012 remind deadline Dear Rob, I would like to recall you the ABZ submission deadline of Jan. 14th. I also kindly ask you, especially

[ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110814

Dear All, I have just completed a new experimental release of OpenProofPower. You can find it here: http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110814.tgz The idea is that an experimental release is a step toward the next stable version (2.9.2 in this

Re: [ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110814

Oops1 On 14 Aug 2011, at 16:18, Rob Arthan wrote: ... b) In xpp, you can now switch dynamically between the horizontal and vertical layout using a new item in the window geometry. I meant new item in the Window Menu. Regards, Rob.___ Proofpower

Re: [ProofPower] How do you arrange Xpp?

a 1280x800 screen, and so horizontal mode means that the journal window is very squashed up if the script window stays at 80. So I prefer vertical. I bet Phil is now going to show off about his new, super-hidef screen laptop and suggest horizontal mode... :) Mark. on 22/7/11 3:10 PM, Rob

[ProofPower] Experimental OpenProofPower release 2.9.1w2.rda.110727

Dear All, It has taken a little bit longer than I would have hoped but I have just completed a new experimental release of OpenProofPower. You can find it here: http://www.lemma-one.com/ProofPower/getting/experimental/OpenProofPower-2.9.1w2.rda.110727.tgz The idea is that an experimental

Re: [ProofPower] Z parser/pretty printer issue with precedence of lambda and mu

Phil, On 15 Jul 2011, at 15:29, Phil Clayton wrote: I was going to leave this issue for now but I bumped into it again today, so I've had a look into it. (It's not something that is holding me up, just forcing me to put in parentheses where I don't want to!) This issue was originally

Re: [ProofPower] Schema in a predicate stub

Phil, On 6 Jul 2011, at 16:15, Phil Clayton wrote: On 21/06/11 16:58, Phil Clayton wrote: Is there any reason why a schema argument in a predicate stub (_?) isn't implicitly converted to a predicate? A Z specification taking a Standard-compatible approach to booleans may have: BOOL ==

Re: [ProofPower] Printing of \not\in

to something different from what LaTeX gives you out of the box. Note that \notin is not in the standard list of mathematical symbols in the LaTeX User's Guide. Regards, Rob. On 31 Mar 2011, at 14:26, Roger Bishop Jones wrote: On Tuesday 29 Mar 2011 16:48, Rob Arthan wrote: It works fine

Re: [ProofPower] Xpp on Fedora 14 and later

Phil, The OpenMotif bug report suggests that if you use jpeg versions of the template images, then things will work. You can find a tarball containing the jpegs you need here: http://dl.dropbox.com/u/34693999/ProofPower/template-jpegs.tgz If you copy these into the bitmaps directory in the

Re: [ProofPower] Characteristic function construction?

Phil, On 5 Jun 2011, at 22:53, Phil Clayton wrote: I've noticed that the ProofPower-Z grammar accepts lambda expressions without a spot, e.g. (%lambda% x : X) because it uses the same grammar rules as for mu expressions. Such expressions always produce the error message Exception

Re: [ProofPower] Broken theory indexes

On 10 Aug 2010, at 17:08, Roger Bishop Jones wrote: ... \typeout{$Id: rbj.sty,v 1.2 2010-08-08 15:50:44 rbj Exp $} \NeedsTeXFormat{LaTeX2e} \ProvidesPackage{rbj} \RequirePackage{ProofPower} \RequirePackage{mathabx} \def\Zdef{\MMM{\corresponds}} \def\holindexon{\def\holin...@aux##1{%

Re: [ProofPower] Using sqsubset symbol

On 6 Jul 2010, at 10:29, Roger Bishop Jones wrote: I find myself in puzzlement when trying to use the square subset symbol. When I use it I get an Unknown extended character error. If I try to add it (as if it were one of the unallocated codes) using add_new_symbols it complains that

Re: [ProofPower] Generating PDF files with texdvi and docdvi

On 14/04/2010 17:03, Roger Bishop Jones wrote: On Wednesday 14 Apr 2010 16:07, Rob Arthan wrote: Can you test texpdf on wrk066 from maths_egs? makeindex produces some garbled entries resulting in LaTeX erros when I try running it by hand. No, doesn't work. ! Extra

Re: [ProofPower] help

(tryed find -name '*ML_dbase*') ig...@igorj-laptop:~/Desktop/OpenProofPower-2.7.8$ ./configure Using /opt/pp as the installation target directory Using Poly/ML ERROR: The file /usr/lib/poly/ML_dbase does not exist 2009/11/16 Rob Arthan r...@lemma-one.com Igor, PS: the mailing list

Re: [ProofPower] ProofPower on Ubuntu 9.04

On Tuesday 13 Oct 2009 1:15 pm, Roger Bishop Jones wrote: I have tried to build ProofPower on Ubuntu 9.04, but it failed so I was wondering whether anyone else has succeeded and if they have any helpful hints. I used the lastest p2 sources, which build OK for me on openSUSE 10.3. On

[ProofPower] Forthcoming Poly/ML 5.3

Dear All, Poly/ML 5.3 is likely to be released very soon. I have just posted a patch on the ProofPower website that fixes a performance problem you will experience if you compile using the latest development version of Poly/ML or with 5.3 when it is released. As most people have fairly fast

[ProofPower] OpenProofPower 2.8.1

Dear All, I am happy to announce that OpenProofPower version 2.8.1 is now available from the ProofPower web site: http://www.lemma-one.com/ProofPower/getting/getting.html Many thanks to all who helped with the new version and particularly Phil Clayton of QinetiQ. Regards, Rob.

Re: [ProofPower] Clashing definitions

Roger, On 9 Jun 2009, at 07:23, Roger Bishop Jones wrote: On Monday 08 June 2009 22:59:01 Rob Arthan wrote: The name clash should definitely cause an error. Perhaps you are catching the error somehow? I don't think so. Re-instating the error, I end up in a context in which rbjmisc

Re: [ProofPower] Extended character support

On 5 Jun 2009, at 08:35, Roger Bishop Jones wrote: I quite often find that I want to use a new character in ProofPower HOL. However, ProofPower seems to be quite fussy about what characters you use. For example, there are three spares at the moment, which would be useful for me. They

Re: [ProofPower] Subgoal limits

On 18 May 2009, at 23:27, Artur Oliveira Gomes wrote: Rob, Can you tell me how can I increase the default subgoal limit when stripping a goal? In that proof I sent you an example, or me, the complete version of the proof creates over 34 subgoals, then, ProofPower give me a warning telling

Re: [ProofPower] Instantiation of free variables according to some matching.

Frank, On 7 Apr 2009, at 14:39, Frank Zeyda wrote: Dear Roger, Many thanks for the reply. The additional feature of better error handling is easily supported with another line of code handling possible exceptions. The idea behind the caller parameter in many of these internal

Re: [ProofPower] Real Numbers - Proofs

Artur, You may like to know that there is a so-called component proof context called 'z_reals which will make evaluation of real arithmetic expressions happen automatically when you rewrite. Try: set_merge_pcs['z_reals, z_library]; set_goal([], %SZT% real 30 %mem% real 20 ..%down%R real 40

Re: [ProofPower] Error when installing Proofpower 2.8

On 27 Jan 2009, at 21:54, Artur Oliveira Gomes wrote: Rob, I'll try to install this release on Ubuntu. You mentioned Mac OS X. Do you have a tutorial, anything to help me in order to install ProofPower on a Mac? It is just like installing on Linux. You need to have installed the