Re: [ProofPower] "Unicode" vs. UTF8

On 07/11/2023 10:09, Makarius wrote: I first heard of "Unicode" approx. 1990. Everybody was talking about "wide charaters" (16bit) and made moves to support them (e.g. major Unix vendors and MicroSoft). That was the time of now obsolete UCS16: "16bit should be sufficient for everyone, i.e. ever

Re: [ProofPower] Existential Elimination

David, Something odd about your message which confuses my mail tool and doesn't quote it properly, so this is hand cranked (your text in italics) / //What is confusing is the 3 parameters.  e.g. In this partial proof, there is only one premise, but you mention 2? /I'm afraid I'm confused by

Re: [ProofPower] ∃_elim

David, The existential rule most closely analogous to universal instantiation is existential introduction. The ∃_elim rule is more complex, and the name perhaps misleading. The conclusion is always exactly the conclusion of the second premise. The existential "eliminated" is the conclusion of t

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

On 04/11/2019 02:01, David Topham wrote: Those two don't seem to get along!  Probably my error and sorry to be burdening you with debugging due to partial understanding on my part. you need ⌜sum (pow r)⌝ and now you are in the reals, / instead of Div, so: ⌜λ n⦁ ∀ r⦁ sum (pow r) n = 1.0 - po

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

David, I should perhaps have mentioned that though your formulation of 9.1 is correct, what you have for 9.2 does not capture that theorem correctly, because your "sum n" adds the first n natural numbers, not the first n elements of a sequence. To get 9.2 you need to use the function "sigma" p

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

David, Good to see you are making some progress. For the examples in 9.2 you best course is probably to have a power function with type:     ℝ→ℕ→ℝ ⓈHOLCONST │ pow:ℝ→ℕ→ℝ ├── │ ∀b e⦁ (pow b 0) = 1. ∧ │       (pow b (e + 1)) = b * (pow b e) ■ This will fit with Rob's suggestion for modelling s

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

On 02/11/2019 19:10, Rob Arthan wrote: If I need to work with the rationals I just treat them as a subset of the reals. Though I think for these examples even that is an unnecessary complication, since the proof over the reals as a whole will be closest (apart from the actual types) to what a p

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

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! Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/m

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

David, Thanks for the reference to the text you are working from, it makes it much clearer what you are trying to do. In example 9.2 I think he should stipulate 0 < r < 1 not just r not= 1. I think strictly speaking if you work with real numbers you are not doing discrete maths, but I don't

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

David, Looking further at what you are trying to prove, its clear that, though you can have geometric sequences over the naturals, this kind of result will not be obtainable in that context. As soon as you thing of them as series, things go awry, since non but the absolutely trivial ones con

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

David The ascii may not be readable, but it can be converted back to ext, or to utf8: ⓈHOLCONST │ sum:ℕ→ℕ ├── │ ∀n⦁ sum 0 = 0 ∧ sum (n) = n + (sum n-1) ■ ⓈHOLCONST │ pow:ℕ→ℕ→ℕ ├── │ ∀b e⦁ (pow b 0) = 1 ∧ (pow b e) = b * (pow b (e - 1)) ■ =SML val ex92 = ⌜λ n r⦁ sum (pow r n) = (1 - (pow r (n -

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

On 01/11/2019 18:38, David Topham wrote: Adapting to the idea of using only whole numbers for a geometric progression that sums over powers I am trying this approach: It works up until trying to instantiate into induction_thm where it breaks down since conjecture needs 2 variables:  r and

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

David, On 01/11/2019 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.  I see the "induction_thm" won't work with R anyway since it has

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

David, On 31/10/2019 19:14, David Topham wrote: Thank you Roger, that is very helpful.  I found I had to add this line to make it work: (open_theory "cs113" handle _ => (open_theory "hol"; new_theory "cs113")); But then my next problem is to work on geometric progressions which require real

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

David, I missed a pair of brackets in my last. Should be: ⓈHOLCONST │    tri : ℕ → ℕ ├── │    ∀n⦁    tri 0 = 0 │    ∧    tri (n+1) = (tri n)+n+1 ■ ⌜∀n⦁ tri n = (n*(n+1)) Div 2⌝; val tri_p = ⌜λn⦁ tri n = (n*(n+1)) Div 2⌝; ∀_elim tri_p induction_thm; val lemma1 = rewrite_r

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

David, On 29/10/2019 22:55, David Topham wrote: Thanks Roger, I do have some pure SML code that checks the summation to the explicit formula but not so sure how to express summation in ProofPower. I did find this interesting reference http://www.rbjones.com/rbjpub/pp/rda001.html Which has th

Re: [ProofPower] ProofPower and Discrete Math

David, On 28/10/2019 02:39, David Topham wrote: Hello Rob,Roger, et al. Hope you are doing well. I am still trying to apply ProofPower to forward proofs. Glad to hear that. I am working on proof by induction and came across this: induction_thm In the notes, there is an intriguing statement t

Re: [ProofPower] ProofPower and Discrete Math

> David, Good to hear you are still moving forward. If the transformation you seek is a propositional tautology, the following general prescription should work. 1. Formulate the transformation as an equivalence using propositional (Boolean) variables, with the starting point on the left of the

Re: [ProofPower] ProofPower and Discrete Math

val L5 = %exists%_intro L4 L3; val L6 = asm_rule %<%%exists%y:'b%spot%p%>%; val L7 = %exists%_elim L4 L5 L6; The error I get is "does not match the bound varstruct" Does anyone have a suggestion to get me past this roadblock?

Re: [ProofPower] Font for SML

David, Looks like one problem for you is the way you are processing the latex files. There is a ProofPower manual, USR001, called:ProofPower - Document Preparation which tells you how to process ProofPower files for printing (or to .dvi fi

Re: [ProofPower] Font for SML

David, Doctex doesn't chose a font, it just generates LaTeX commands for the formal text and any font changing is up to the rest of the document (that you provide in the =TEX sections of the .doc file). It does generate tex for the HOL and ZED paragraphs which is intended to force the layout

Re: [ProofPower] file conversion

s On 18/08/2016 21:15, Rob Arthan wrote: Roger, On 17 Aug 2016, at 11:41, Roger Bishop Jones wrote: Rob, It would be helpful for intelligible email discussions about ProofPower if you could tell us all the slickest way to get a proofpower script into a form in which it can be pasted into an

[ProofPower] file conversion

Rob, It would be helpful for intelligible email discussions about ProofPower if you could tell us all the slickest way to get a proofpower script into a form in which it can be pasted into an email (UTF8 presumably), and vice-versa. Roger ___ Proo

Re: [ProofPower] ProofPower and Discrete Math

David, There is a reason why the ProofPower tutorials don't say much about the forward proof tools you are trying to use. I have given courses on ProofPower HOL and on ProofPower Z and wrote the tutorials. What I did in the courses was to teach just enough about forward proof for the students

Re: [ProofPower] ProofPower and Discrete Math

On 14/08/2016 08:44, David Topham wrote: Thanks Roger, I am using slides he distributes. He has false introduction rules starting on page 24 (attached). Sorry about my poor example, please ignore that since is a confused use of this technique anyway! -Dave Looks like he changed the name.

Re: [ProofPower] ProofPower and Discrete Math

David, I don't quite understand what you are trying to do here. On the face of it you want a rule: p -- false-intro false But this is not possible, because it is not sound. As far as I can see Woodcock does not have a false-intro rule, he has only a false-elim rule, is that what you

Re: [ProofPower] ProofPower on Ubuntu 16.04

ched a patch. If you build poly yourself, rather than install the package you might not need to do (2), but the patch does not harm. Regards, Rob. On 21 Jul 2016, at 11:15, Rob Arthan wrote: Roger, On 18 Jul 2016, at 22:15, Roger Bishop Jones wrote: I have been trying to install ProofP

[ProofPower] ProofPower on Ubuntu 16.04

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 usual repositories. If anyone figures out how to get ProofPower installed on Ubuntu 16.04 I s

[ProofPower] Installing ProofPower on OS X El Capitain

Here is my reconstruction of the method I used to get ProofPower running on OS X 10.11.4, which is an adaptation of a recipe posted by Rob for an earlier version of OS X. From the App Store install Xcode. The rest of the process is done on the command line, so you either need to use terminal

Re: [ProofPower] ProofPower build on OS X

Magic. Build complete. I just had to change the path. xpp seems to come up ok. Thanks, I’ll post a resume. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Re: [ProofPower] ProofPower build on OS X

Rob, Now failing to find mkfontdir. PATH=/opt/local/bin:/opt/local/sbin:/usr/bin:/bin:/usr/sbin:/sbin:/Applications/Emacs.app/Contents/MacOS/bin-x86_64-10_9:/Applications/Emacs.app/Contents/MacOS/libexec-x86_64-10_9 Am I missing something from the PATH or do I need to install something else? Ro

Re: [ProofPower] ProofPower build on OS X

Rob, Thanks for you continuing support. > On 30 Apr 2016, at 10:16, Rob Arthan wrote: > > ... > Try it in in src/dev. I think it will fail. If so, try it without the > obsolete options: > > polyc -o pp-ml pp-ml.o > Here are the results: bash-3.2$ polyc -segprot POLY rwx rwx -o pp-

Re: [ProofPower] ProofPower build on OS X

Rob, > On 29 Apr 2016, at 20:31, Rob Arthan wrote: > > > The linker can’t find the gmp library. What version of Poly/ML are you using? > Did you build > it yourself or download it ready-made from somewhere? > I did: port install polymer poly -v gives Poly/ML 5.5.2 ReleaseRTS ve

[ProofPower] ProofPower build on OS X

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 { { echo "val system_version : string = \"3.1w7\"; val build_date : Date.date = Date.fromTimeLocal(

Re: [ProofPower] ProofPower on OS X

> On 29 Apr 2016, at 10:24, Roger Bishop Jones wrote: > > > That seems to be necessary, but the port of openmotif nevertheless fails. > port complains that: > > xorg-libXt must be installed with +flat_namespace > I found the fix to that, so I am progressing, Will po

Re: [ProofPower] ProofPower on OS X

Thanks for your help so far Rob. > On 28 Apr 2016, at 22:01, Rob Arthan wrote: > >> I have managed to get Xcode installed now, > > Good. > >> but fail on step 2 of your prescription because the preferences in Xcode >> doesn’t seem to have a download option. > > I am not sure an analogue of t

Re: [ProofPower] ProofPower on OS X

> On 28 Apr 2016, at 11:57, Rob Arthan wrote: > > > Can you point me at the recipe, so I can see what is likely to be > out of date. http://lemma-one.com/pipermail/proofpower_lemma-one.com/2012-December/000955.html

[ProofPower] ProofPower on OS X

I would appreciate advice on how to run ProofPower on OS X El Capitain (10.11.4). I tried a rather dated recipe posted by Rob a while back but find that there is problem installing Xcode (it hangs up in the installation). If I have to resort to running Linux is VirtualBox the best way to do that

Re: [ProofPower] V_cancel_rule alpha-conversion error

David, This is not an alph-conversion error. The reference to apha conversion is a normal qualifier when any rule doesn't get what it needs, since in general a statement of of what is needed need only be complied with "up to alpha conversion". The real problem here (I guess since I can't actually

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

On 28/09/15 11:05, Lin, Yuhui wrote: > Thank you very much. Your solution works perfectly for me. Just be a little > curious, what dose the following promoted message means when applying the > tactic > > 'Tactics proof introduced the subgoal 2 but did not request it as a > subgoal" > > Tha

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

Further to my last on this topic, I now see that simple_eq_match_conv already does what is needed for the solution of the first approximation to the requirement. If you take a theorem of the form: forall x, y. P(x,y) ==> A(x,y) = B(x,y) and infer: P(x,y) |- A(x,y) = B(x,y) the

Re: [ProofPower] tactic in backward reasoning for rewrite rules with conditions

On 23/09/15 13:03, Lin, Yuhui wrote: > Hi, > > I want to write a tactic to performance the following action, > > assume that the goal is > h_1, … h_n |- g > and thm is > forall x, y. P(x,y) ==> A(x,y) = B(x,y) > where A(x,y) can be matched with a subterm of the current goal. After >

[ProofPower] Hard copy manuals

>From version 3.1w6 most of the ProofPower manuals are available as paperback books from amazon websites. A search on a US or European amazon website for "ProofPower Manuals" brings them up, or you can use the links provided at the top of the ProofPower documentation page which is created when ver

Re: [ProofPower] apply conditional rewriting

On 04/06/15 10:30, YuHui Lin wrote: > Hi, > > How can I apply a conditional rewrite rule in proof power. For example, > applying the following thm: > > forall x,y, z | x > y dot x - y + z = x + z -y > > where x > y is the condition, to generate the following two subgoals: > 1) x > y > 2) goal

Re: [ProofPower] ProofPower and Discrete Math

On 03/02/15 13:55, David Topham wrote: > > > I am interested in using ProofPower to aid in the teaching of Discrete > Math. I would like to assist the students in developing proofs using > specific rules of inference. e.g. in the attached proof from our > textbook the proof uses Hypothetical Syllog

Re: [ProofPower] use and use_file

On 19/09/13 16:25, YuHui Lin wrote: > Hi, > > I notice that some function names need to be changed when using the key word > 'use_file' to include ML files, e.g. EQUAL becomes E%Q%UAL. I wonder why ? > Is there anything else I need to keep in mind when using use_fie ? Many > thanks. > use_file

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

Further to my last, this is what I did before building on Ubuntu 12.04 sudo apt-get install texlive-latex-extra texlive-fonts-extra sudo apt-get install libXp-dev libXext-dev \ libXmu-dev libXt-dev \ libxft-dev libjpeg-dev libpng12-dev sudo apt-get install libmotif4 libm

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

On 09/05/13 23:03, Piotr Trojanek wrote: Thank you for your reply. I have groff installed, so this is not the reason. As far as I understand, the build workflow is .doc->.sml->.err. With my experience in SML I can only attach the files with indication of the problem and kindly ask for your assis

Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)

On 09/05/13 15:16, Piotr Trojanek wrote: Dear ProofPower experts, I triy to install the latest OpenProofPower under Ubuntu 12.04, but it fails with the (somewhat cryptic) tail of build.log: docsml -f hol.svf imp001 Compiling (code) imp001.sml make[1]: *** [imp001.ldd] Error 1 My setup details:

Re: [ProofPower] directory path

Sarah, The reason why you had problems after setting the PATH variable to point to the ProofPower binary directory is because you set it to include only that one directory, so xpp was found, but lots of other necessary binaries were no longer in the search path. As recommended by Phil, the c

Re: [ProofPower] any recommended ml editor

On 19/02/13 10:29, Yuhui Lin wrote: Hi, We plan to start a project based on proofpower. So we want to have a look at the source code, in particular those ml files. I wonder that if there is a recommended editor which can access/organise the source code for a developer. Currently I'm switching

Re: [ProofPower] (no subject)

On 19/02/13 00:55, Phil Clayton wrote: Easy - by doing exactly that before you run xpp, e.g. PATH=/home/sarah/pp/bin:$PATH Put this in /home/sarah/.bash_profile to have this done automatically when you log in. (That's for Fedora, at leats. For other Linux distributions, it may go

Re: [ProofPower] latest release

On Tuesday 15 Jan 2013 17:02:01 Jon Lockhart wrote: Roger, Thanks, so the issue is then with an older release of the tool. I doubt that there is a problem with either release, just a misunderstanding of how to configure. Sarah raised a problem, and when I went to check it I had just upgrade

[ProofPower] latest release

On Tuesday 15 Jan 2013 16:42:21 Jon Lockhart wrote: Is 2.9.1w2 the latest release of ProofPower on the git hub? 2.9.1w5 is available at lemma-one.com. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinf

Re: [ProofPower] templates activation problem

On Tuesday 15 Jan 2013 09:27:06 Roger Bishop Jones wrote: > On Tuesday 15 Jan 2013 07:43:30 Phil Clayton wrote: > > When you select Tools->Templates, do you see the templates dialog box > > (with very small buttons) or does nothing happen? (The first is a known > > iss

Re: [ProofPower] templates activation problem

On Tuesday 15 Jan 2013 07:43:30 Phil Clayton wrote: > When you select Tools->Templates, do you see the templates dialog box > (with very small buttons) or does nothing happen? (The first is a known > issue that is easily worked around.) I havn't used the templates for a long time, but I see now

Re: [ProofPower] Trying to Prove my Zed Specifications

On Tuesday 06 Nov 2012 01:04, Jon Lockhart wrote: > Unfortunately I realized I > needed to show that the starting and calling floors were > greater than zero not greater than or equal to zero. However, this makes the goal false, so far as I can see. You need to change the specification if you wan

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, I should have mentioned that the problem goal you are looking at can be solved by linear arithmetic so you don't need any lemma at all. Linear arithmetic is not covered by the tutorlal but this is one way to prove the goal: a (PC_T1 "z_lin_arith" asm_prove_tac[]); Roger

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, Your file does not show what you were trying to do with LEMMA_T, or what you actually did, so its hard to offer much help. "lemma_tac" is easier to understand that "LEMMA_T", so you could try doing it with "lemma_tac" first. (you can always collapse it down to an application of LEMMA_T o

[ProofPower] Recursion theorems without constructors

I make quite a lot of use of recursion theorems to enable various kinds of recursive definitions to be proven consistent automatically. The facilities provided in ProofPower are designed to support recursive definitions over recursive datatypes, in which every element of the type is obtained u

Re: [ProofPower] Trying to Prove my Zed Specifications

On Thursday 18 Oct 2012 21:14, Jon Lockhart wrote: > After fixing the correction you pointed out, I was able > to get the existance proofs completed and I removed the > precondition proofs for those init operations. You can > see this in the attached specification file. You are now using after st

Re: [ProofPower] Trying to Prove my Zed Specifications

On Wednesday 17 Oct 2012 04:18, Jon Lockhart wrote: > Attached is my latest attempt. With both the delta > operator and priming Button_State, with the existance > and precondition proof, I run into a wall. I get close, > but can't seem to give it the right witness to solve > this simple init opera

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 16 Oct 2012 01:12, Jon Lockhart wrote: > I guess I didn't quite understand or comprehend properly > the second point you were trying to make. I inserted an > existance proof like I had done for the state schemas > and I unfortunately get a very interesting goal after > the rewrite

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Sunday 14 Oct 2012 04:52, you wrote: > Any direction on how to finish these up so I may move on > to the actual operations would be greatly appreciated. Two points to keep in mind. First, ProofPower does not automatically rewrite with any of the specifications which you have put in, yo

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Friday 12 Oct 2012 20:35, Jon Lockhart wrote: > I got back to the specification today, and moved on to > proving the elevator state schema, Elevator_State, and I > moved the static component elevator to an axiom, similar > to the static components of button. Unfortunately I get > a weird

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 09 Oct 2012 20:22, Jon Lockhart wrote: > I am having a little trouble getting the axioms created, > moving the static portions of the Button_State to an > axiom from the schema. I can't seem to get the proof to > operate properly. Any suggestions? The problem is that the existent

Re: [ProofPower] Trying to Prove my Zed Specifications

On Friday 28 Sep 2012 22:26, Jon Lockhart wrote: > I have two questions on that then. First, from a since > and style standpoint, if I wanted to make everything > neat in the spec I would place the no changing sets in > the axiom after the state schema, but for functionality > standpoint, if I wa

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 25 Sep 2012 22:05, Jon Lockhart wrote: > I started doing the "There Exist" proofs, and as you said > they seem quite trivial indeed, but I seem to be stuck > after the first two lines. So I have the goal, and it > has been rewritten, now I am not sure what is the right > question

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Sunday 23 Sep 2012 22:32, Jon Lockhart wrote: > I tried adding the exclamation point to the end of the > pushed' line, but if gave me a paser error saying free > types here not allowed. I have provided exactly the what > the paragraph looked like I tried to parse and the error > that was

Re: [ProofPower] Initialisation convention

Phil, On Sunday 23 Sep 2012 21:11, Phil Clayton wrote: > By making initialization an operation without a before > state, the initialization can be used with schema > operators such as composition and pre, e.g. > >Init ⨟ Op > >pre Init > > the latter being another way to write the follo

[ProofPower] Initialisation convention

I see that Potter Sinclair and Till "An Introduction to Formal Specification Using Z" 1991 use the primed version of the convention, and offer the following rationale (p43): "Here we use Vocab' as the variable to suggest that initialisation is like an operation which produces after objects whi

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Saturday 22 Sep 2012 00:11, Jon Lockhart wrote: > I tried what you mentioned after Phil brought it up and > if you try to do State' and then push' = {} the system > throws an error saying "No free types allowed in > predicates" which to me means that push is not > accessible in the predic

Re: [ProofPower] Trying to Prove my Zed Specifications

On Friday 21 Sep 2012 11:52, Roger Bishop Jones wrote: > I checked Spivey (Understanding Z) In fact it was "The Z Notation" I checked. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/pro

Re: [ProofPower] Trying to Prove my Zed Specifications

I checked Spivey (Understanding Z) and Woodcock (Using Z) on the conventions they use for initial state. Neither of them uses an operation for initial state. In Spivey initial state is simply a constraint on state. In Woodcock initial state is a constraint on state'. I have no idea why Woodcock

Re: [ProofPower] Trying to Prove my Zed Specifications

On Wednesday 19 Sep 2012 21:10, Jon Lockhart wrote: > I moved on to the next area of my specification, which is > the initializations of the states declared earlier, and > I am stuck on the first one. No errors or anything, just > not sure how to proceed to reduce the goal any further. > As of now

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Tuesday 18 Sep 2012 20:37, Jon Lockhart wrote: > So I have run into an error again while working on my > specification. This time it is with the second axiomatic > definition, the one right after Roger helped me with > last time. Using what he had done, and from the integer > example in th

Re: [ProofPower] Question - Step After Proof Verification?

On Tuesday 18 Sep 2012 00:00, Jon Lockhart wrote: > In any case, we came up with the question of what do you > do when you are taking the specification and developing > the code from it? So, I thought since many of you have > written specifications in Zed like I am doing now, what > have you all d

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, On Friday 14 Sep 2012 21:14, Jon Lockhart wrote: > Now I have moved on to trying to do the same thing for > masterReset, using the exact same code that Roger has > implemented in my spec, but now I am getting an error > when I try to push the consistency goal. That's because its a single sp

Re: [ProofPower] Trying to Prove my Zed Specifications

On Friday 14 Sep 2012 17:39, Jon Lockhart wrote: > First, I find it odd that the zipping is not working when > before it was for Phil, and still is for me. I just > generated a zip, emailed it to myself, and then unzipped > it and got something that looks just fine, exactly what > I zipped up. I h

Re: [ProofPower] Trying to Prove my Zed Specifications

On Friday 14 Sep 2012 10:36, Phil Clayton wrote: > On 14/09/12 10:05, Roger Bishop Jones wrote: > > I had a brief look at the last spec that you posted. > > I also had a problem unzipping it, ... > > This doesn't surprise me because the attachment was byte > for

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, I had a brief look at the last spec that you posted. I also had a problem unzipping it, but despite a failure message got a decompression by opening the file in emacs. The file decompressed in this way had two issues in it. The first was that it terminated mid paragraph. The second was that

Re: [ProofPower] Best platform for ProofPower?

On Thursday 13 Sep 2012 19:37, Phil Clayton wrote: > On 12/09/12 21:05, Roger Bishop Jones wrote: > > So far I'm not having much success on Ubuntu 12.04 (the > > PolyML build doesn't seem to work for me). > > What error message do you get? I ask because David >

[ProofPower] Best platform for ProofPower?

I'm having bad luck lately getting suitable environments for running ProofPower. My laptop is on Ubuntu 10.4, and that is fine for ProofPower, but is now so out of date that I can't upgrade it, I would have to install a more recent version of Ubuntu from scratch. So I revived an old server to

Re: [ProofPower] ProofPower Update

Rob, Sorry for the slow response. I have thought quite a bit about this, but these days such cogitations don't always go anywhere useful. On Thursday 30 Aug 2012 21:58, Rob Arthan wrote: > On 11 Aug 2012, at 15:07, Roger Bishop Jones wrote: > > and a number of cases where ident

Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 03 Sep 2012 21:03, Jon Lockhart wrote: > Most of the tactics return the > exact same goal and the comment printed with the goal is > that it is alpha-convertible to its goal. The significance of this is simply that the proof step you have just done has not moved you forward. i.e. it sa

Re: [ProofPower] Trying to Prove my Zed Specifications

On Saturday 25 Aug 2012 20:47, Jon Lockhart wrote: > I did have a question on some of the outputs from the > tutorial document. Currently I am on user013C and when I > have placed some of the commands into the terminal, via > the execute line command, the ProofPower output is not > the same as is

Re: [ProofPower] Trying to Prove my Zed Specifications

Jon, You are right that Rob is the man to answer your technical problem, but in the meantime I might be able to help you round it. "save_and_quit();" is something that I never use. If your system otherwise seems OK then you should go right ahead and work through the tutorial. Why don't I use

Re: [ProofPower] Trying to Prove my Zed Specifications

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 the Z in a format suitable for > processing by other

Re: [ProofPower] Trying to Prove my Zed Specifications

On Monday 13 Aug 2012 03:24, Jon Lockhart wrote: > I have already written the specifications in Word using Z > Word Tools, and they are already saved in a variety of > formats. I have them transferred over to my linux image. > What format do they need to be in for me to get to > import them into X

Re: [ProofPower] ProofPower Update

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 names. These include the changes to theorems "plus" => "additive"

Re: [ProofPower] ProofPower Update

The new version of ProofPower breaks a differential geometry proof (probably one of yours!) in my t003. Were you expecting this to happen at this stage, I thought I had already sucessfully built all my stuff on the version with the higher order rewriting? The changes history does not seem to b

Re: [ProofPower] ProofPower Update

Rob, My theories fail to build on the latest version of maths_egs because I have been using "R_plus_ops_thm" and "R_plus_group_thm" which were in wrk068 but are no longer. Looks like you have just changed some names, is that right? Roger Jones ___ P

Re: [ProofPower] ProofPower Update

Rob, On Thursday 09 Aug 2012 10:26, Rob Arthan wrote: > 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/getti

Re: [ProofPower] ProofPower RCS Repository

On Monday 06 Aug 2012 19:40, Rob Arthan wrote: > Could you try again with > PPMOTIFLINKING=dynamic ? That worked fine. I'm afraid I can't help with mercurial or git, but I am due for a new development regime so I will be following you closely. Roger __

Re: [ProofPower] ProofPower RCS Repository

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 or Git and RCS. Any feedback on this > would be gratefully

[ProofPower] ProofPower on AWS EC2

Thanks to Phil, Rob and Wolfram for help so far. I was completely distracted yesterday by the delivery of a new keyboard (7-octave variety), but seem to have made some progress. Phil's Yum prescription was helpful. The amazon repositories don't have SML, but do contain a satisfactory openmotif.

Re: [ProofPower] Trouble Installing in cloud

On Thursday 02 Aug 2012 00:33, you wrote: > On 01/08/12 14:35, Roger Bishop Jones wrote: > > The real challenge (for me at least) is to get xpp > > and/or emacs to run in the cloud with a display here > > on earth, I don't have much clue how to do that. > > I

Re: [ProofPower] Trouble Installing in cloud

Phil, On Wednesday 01 Aug 2012 14:06, Phil Clayton wrote: > Can you > provide the output of > >rpm -ql openmotif-devel It had to be something really stupid, I don't do enough of this kind of thing. I didn't install openmotif-devel. Now I have, and the configure script does find it. I have

[ProofPower] Trouble Installing in cloud

I seem to have the same problem as John in a different place. i.e. in a linux image in the amazon cloud. I followed Phil's Yum list to get me started, which worked apart from failing to find polyml. I successfully built polyml from the sources. Then I checked with yum and found that the openmotif

Re: [ProofPower] ProofPower in the cloud?

I have a Linux instance running up there in the Amazon "elastic cloud" and will see if I can install ProofPower. There doesn't seem to be much software installed, not even "make", but "yum" seems to be working fine. I'll report back if I get anywhere. Roger Jones

  1   2   >