Re: [ProofPower] Schemas and Operations
Hi Roger, This is a simple example to try to explain what I have now. My current problem is bigger than that. I have a state with many components. To load any operation over that state, ProofPower takes a long time without response. Few months ago, I sent a doc file to Rob Arthan and he suggested to use %SFT%Z %V% St %def% [St : State] %EFT% That is what I am using so far, every operation is similar to %SZS% OpNewState %BH%%BH%%BH%%BH% %BV% %Delta%NewState %BT%%BH%%BH%%BH%%BH% %BV% Old.a = real 0; %EZ%%BH%%BH%%BH%%BH%%BH% and it works fine, loading quickly. For a similar predicate to work you would need the signature of NewState to be the same as for State. Is there any other solution for my problem? Thanks, -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Z Schemas - Help with Initialization and Precondition calculus
Hi there, I'm having hard times to achieve some proofs of preciondition and initialization using ProofPower. The file attached contains 3 examples that I still can not prove. If anyone could help me out with those proofs, I will be thankful. Best, -- Artur Oliveira Gomes examples.doc Description: MS-Word document ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Z Schemas - Help with Initialization and Precondition calculus
Roger, When I execute: a (REPEAT z_strip_tac THEN POP_ASM_T ante_tac THEN asm_rewrite_tac[]); ProofPower returns the following message: :# :# Exception- Fail * the assumption list is empty [POP_ASM_T.9302] * raised Exception+ Fail * the assumption list is empty [POP_ASM_T.9302] * raised Is everything fine? Artur 2009/3/24 Roger Bishop Jones r...@rbjones.com Artur, On Tuesday 24 March 2009 10:35:51 Artur Oliveira Gomes wrote: The problem is: only for those cases, what I choose as witness does not satisfy the predicate. Well, any sequence of length 1 (or zero?) does for the first case. Proof attached. If you still can't crack the other two send me your best attempt. Roger ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Real Numbers - Proofs
Hi there Now I know how to prove it: using z_R_=_conv. Thanks anyway, Artur 2009/3/25 Artur Oliveira Gomes artur.o.go...@gmail.com Hi there, How could I prove that given two real numbers, 20 and 30, that 20 =40? Moreover, given three real numbers, 20, 30 and 40, how could I prove that 30 in 20..40. Regards, -- Artur Oliveira Gomes -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Real Numbers - Proofs
Rob, Thank you. Just one more question: and how about floating numbers? How to prove it? For example: set_merge_pcs['z_reals, z_library]; set_goal([], %SZT% 0.4 %mem% 0.1 ..%down%R 1.9 %%); a(rewrite_tac[z_%bbR%_dot_dot_def]); With those steps, ProofPower change the goal to: %SZT%0.1 %leq%%down%R 0.4 %and% 0.4 %leq%%down%R 1.9%% How can I prove it? Thanks again. Regards, -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
[ProofPower] Rewriting from assumptions - parenthesis problem
Hi there, I am having a problem in rewriting using an assumption with parenthesis. For example: (* 1 *) (\exists (SA AND SB)' · SAInit AND SBInit) = ((\exists SA' · SAInit) AND (\exists SB' · SBInit)) (* |- *) \exists (SA AND SB)' · SAInit AND SBInit The rewriting does not occur due to the parenthesis in the LHS. Does anyone know what should I do to solve this problem? Cheers, -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] How do you arrange Xpp?
Dear Rob, I use the same settings you sent. It would be useful, at least for me, to have these as default. Thank you very much indeed. Best wishes, Artur On 22 July 2011 15:10, Rob Arthan r...@lemma-one.com wrote: I nearly always use Xpp with the following settings in $HOME/app-defaults/Xpp Xpp*script.rows: 32 Xpp*script.columns: 60 Xpp*script.background: white Xpp*script.foreground: black Xpp*journal.rows: 32 Xpp*journal.columns: 60 Xpp*namestring.columns: 24 Xpp*journal.background: light blue Xpp*journal.foreground: black Xpp*journal.editable: true Xpp*mainpanes.orientation: HORIZONTAL This differs from the out of the box default in laying out the windows side-by-side and letting you bring up the command dialogue by trying to type into the journal window. I am tempted to change the default settings to the above - it looks a bit less like a standard Motif application, but it makes much better use of modern screens (or at least modern screens that have a landscape aspect ratio). It would be nice to know what other people do before I commit to this change. So please let me know your preferences. Regards, Rob. ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com -- Artur Oliveira Gomes ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
Re: [ProofPower] Compiling OpenProofPower-2.9.1w5 under Ubuntu 12.04 (64bit)
Dear Piotr, Two years ago I wrote a script in order to automate the ProofPower install process on Ubuntu. I'm sending it so you can give a try. At that time, I used Ubuntu 10.10. After the last message sent from Roger, I slightly updated a few apt files needed. I'm sending the script to you. It should be able to run with no problems. All you need is to have super user permissions (sudo) and place it in the directory you want to have ProofPower installed. Then you only have to do the following: # chmod +x install-proofpower-ubuntu.sh # ./install-proofpower-ubuntu.sh Should you have any problems with the palette, send us an email. ;) Cheers, -- Artur Oliveira Gomes Professor - Sistemas de Informação Universidade Federal do Mato Grosso do Sul On 10 May 2013 08:18, Roger Bishop Jones r...@rbjones.com wrote: 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 libmotif-dev libmotif4-dbg sudo apt-get install splint groff sudo apt-get install autoconf sudo apt-get install g++ You don't need all that for PolyML and ProofPower (probably not the texlive extra stuff, but that's probably the only large item you don't need). Sorry I can't be more definite, I found it hard to figure out what I needed for PolyML, the configure script tells you a lot about what is there and what isn't but its not so clear which items are actually necessary. Roger Jones ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com install-proofpower-ubuntu.sh Description: Bourne shell script ___ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
