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

*To*: Kyongho Min <min@xxxxxxxxxxxxxxx>*Subject*: Re: [PVS-Help] How to use PVSio for prove formulas?*From*: Cesar Munoz <munoz@xxxxxxxxxx>*Date*: Wed, 10 Sep 2008 09:17:35 -0400*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <48C71D64.3080200@cse.unsw.edu.au>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <48C71D64.3080200@cse.unsw.edu.au>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Processing ./pvsbatch.pvs. Writing output to file ./pvsbatch.status.

Proof summary for theory pvsbatch

c2....................................unfinished [shostak](0.02 s)

Theory totals: 2 formulas, 2 attempted, 1 succeeded (0.07 s)

Grand Totals: 2 proofs, 2 attempted, 1 succeeded (0.07 s)

*** File: ./pvsbatch.pvs

*** At: 8:50:30 9/10/2008

*** Generated by: proveit - ProofLite-4.i (09/03/08)

***

Proof summary for theory pvsbatch

c1....................................proved - complete [shostak](0.05 s)

c2....................................unfinished [shostak](0.03 s)

Theory totals: 2 formulas, 2 attempted, 1 succeeded (0.08 s)

$proveit -t c1,c2 pvsbatch

|------- {1} FORALL (x1, x2: int): (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0)

Trying repeated skolemization, instantiation, and if-lifting, This completes the proof of c1.

$ more c2.txt c2 :

|------- {1} FORALL (x1, x2: int): (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)

Trying repeated skolemization, instantiation, and if-lifting, c2 :

{-1} integer_pred(x1!1) {-2} integer_pred(x2!1) {-3} (x1!1 > x2!1) {-4} (x1!1 > 0) |------- {1} (x2!1 > 0)

c1: LEMMA (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0) c2: LEMMA (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)

Hope that this helps, Cesar

On Sep 9, 2008, at 9:05 PM, Kyongho Min wrote:

pvsbatch: THEORY

BEGIN

x1, x2: VAR int

c1: LEMMA (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0) c2: LEMMA (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)

END pvsbatch

Cesar Munoz (NIA) munoz@xxxxxxxxxx

**References**:**[PVS-Help] How to use PVSio for prove formulas?***From:*Kyongho Min

- Prev by Date:
**[PVS-Help] How to use PVSio for prove formulas?** - Next by Date:
**[PVS-Help] Graph library** - Previous by thread:
**[PVS-Help] How to use PVSio for prove formulas?** - Next by thread:
**[PVS-Help] Graph library** - Index(es):