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

Re: [PVS-Help] pvs raw mode



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
>       (+974) 33 52 24 90
>
>
>
>
>




--
Best Regards

Boulifa Bilel
Computer Engineer




--
Best Regards

Boulifa Bilel
Computer Engineer

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