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

*To*: Cesar Munoz <munoz@xxxxxxxxxx>, jane huffam <janehuffam@xxxxxxxxx>*Subject*: Re: [PVS-Help] begginer's question*From*: "Miner, Paul S." <p.s.miner@xxxxxxxx>*Date*: Fri, 03 Oct 2008 08:26:50 -0400*Cc*: pvs-help@xxxxxxxxxxx*In-reply-to*: <48E4DAD8.3080107@nianet.org>*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>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*Thread-index*: AcklU09RjfPtcJFGEd2OoAAfW/LHgg==*Thread-topic*: [PVS-Help] begginer's question*User-agent*: Microsoft-Entourage/11.4.0.080122

Jane, I suspect that the problem you are having is that the tutorial you are using is based on a much older version of PVS. The theory "decisions" as presented in the tutorial declares x, y, and v to be of type number. At that time, the built in PVS type 'number' had all the properties that we expect of real numbers, including the order axioms. However, in the current version of PVS, the order axioms are introduced for type 'real'. They do not apply for objects of type number. If you change the declaration to: x, y, v: VAR real Then the proof given in the tutorial should work. Paul Miner On 10/2/08 10:29 AM, "Cesar Munoz" <munoz@xxxxxxxxxx> wrote: > You should try (grind) instead of (ground): > > {-1} x!1 < 2 * y!1 > {-2} y!1 < 3 * v!1 > |------- > {1} 3 * x!1 < 18 * v!1 > > Rule? (grind) > Trying repeated skolemization, instantiation, and if-lifting, > Q.E.D. > > Cesar > > jane huffam wrote: >> Hi, >> I'm studying pvs through "A Tutorial Introduction to PVS" by Crow, Owre, >> Rushby, Shankar and Srivas. They gave an example I can't prove. It is >> "decisions", section 4.3. I'm stuck in arith. What do I do after "(then >> (skolem!)(ground))" ? >> Thanks for any tip! >>

- Prev by Date:
**Re: [PVS-Help] begginer's question** - Next by Date:
**Re: [PVS-Help] begginer's question** - Prev by thread:
**Re: [PVS-Help] begginer's question** - Next by thread:
**Re: [PVS-Help] begginer's question** - Index(es):