[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] pvs raw mode



but I do not have a simple _expression_, what I want to do is start the proof of a theorem which is defined in a specific line in a file.
I tried this function  " (rerun-proof-at? "file_systemTheorems" nil 6 "pvs") "   but it returns me   "no"   and that's all.

file_systemTheorems: is the file name
6:is the line where the definition of theorem begins

after that I did some research into the source code and I found in the file "pvs-lisp" the function "Prove-file-at" and I used the command " (prove-file-at" file_systemTheorems "nil 6)  "and it returns" Rule? "like "emacs" and then I was able to start the proof process.
what do you think about it ?


thank you very much for your help, it was very useful :) 







2013/1/24 MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx>
Once you have type-checked a theory and the PVS context is set, you can
use the Lisp function

(simplify-expr <pvs-expr> :strategy <strategy>)

where
* <pvs-expr> is a CLOS object representing a *closed* PVS Boolean
_expression_ and
* <strategy> is a PVS proof command.

The function simplify-expr returns the PVS CLOS object that results from
applying <strategy> to <pvs-expr>.

To get a <pvs-expr> from a string, use the function

(pc-parse "<something-in-pvs-syntax>" 'expr)

You can try these functions in PVSio, which provides an interface to the
PVS Lisp engine and to the PVS ground evaluator, e.g.,

<PVSio>  (simplify-_expression_ (pc-parse "FORALL (x:real): x-x = 0" 'expr)
:strategy '(grind))) !
TRUE


(The exclamation mark at the end of the line commands PVSio to evalute the
Lisp _expression_).

On the other hand

<PVSio> (simplify-_expression_ (pc-parse "FORALL (x:real): x-x = 1" 'expr)
:strategy '(grind))) !
real_pred(x!1) IMPLIES 0 = 1

If you download the PVS sources, go to the doc directory and look for the
pvs-api draft. It documents some of these functions.

Cesar

--
Cesar A. Munoz                             NASA Langley Research Center
Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234




On 1/24/13 3:20 AM, "Boulifa Bilel" <boulifa.bilel@xxxxxxxxx> wrote:

>thank you for your response, it was very usefull now i can start pvs in
>raw mode and put some rules but i can't start proof of a theorem, i can
>put change-context and typecheck-file but how can i start proof of a
>theorem and use rules to proove it like skosimp*, prop or grind ....?
>
>
>
>2013/1/21 Boulifa Bilel <boulifa.bilel@xxxxxxxxx>
>
>thank you very much, I'll take a look at this link and give you feedback
>
>
>
>2013/1/21 MUNOZ, CESAR  (LARC-D320) <cesar.a.munoz@xxxxxxxx>
>
>Boulifa,
>
>Look at the tool called Grizzly:
>
>http://shemesh.larc.nasa.gov/people/cam/Bernstein/Grizzly.html
>
>It is part of Bernstein in the NASA PVS Library (Try the version 5.0 of
>the library, version 6.0 doesn't include Bernstein yet, but for what you
>need it, it should be enough):
>
>
>  http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
>
>Grizzly is a script written in Perl that uses sockets to communicate with
>PVS (running in raw mode).
>
>Regards,
>
>Cesar
>
>
>On 1/21/13 3:44 AM, "Boulifa Bilel" <boulifa.bilel@xxxxxxxxx> wrote:
>
>>Does anyone have an example of using the pvs -raw mode?
>>I'd like to use PVS from a Java program but i have not been able to
>>invoke the pvs rules on command line.
>>
>>Thanks...
>>
>>--
>>Best Regards
>>
>>Boulifa Bilel
>>Computer Engineer
>>
>>
>>Boulifa.Bilel@xxxxxxxxx
>>Tel: (+216) 97 808 500 <tel:%28%2B216%29%2097%20808%20500>
>>       (+974) 33 52 24 90 <tel:%28%2B974%29%2033%2052%2024%2090>
>>
>>
>>
>>
>>
>
>
>
>
>
>
>
>
>
>
>
>--
>Best Regards
>
>Boulifa Bilel
>Computer Engineer
>
>
>Boulifa.Bilel@xxxxxxxxx
>
>Tel: (+216) 97 808 500 <tel:%28%2B216%29%2097%20808%20500>
>       (+974) 33 52 24 90 <tel:%28%2B974%29%2033%2052%2024%2090>
>
>
>
>
>
>
>
>
>
>
>
>--
>Best Regards
>
>Boulifa Bilel
>Computer Engineer
>
>
>Boulifa.Bilel@xxxxxxxxx
>Tel: (+216) 97 808 500
>       (+974) 33 52 24 90
>
>
>




--
Best Regards

Boulifa Bilel
Computer Engineer

Boulifa.Bilel@xxxxxxxxx
Tel: (+216) 97 808 500
       (+974) 33 52 24 90