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

[PVS-Help] begginer's question

To: pvs-help@xxxxxxxxxxx
Subject: [PVS-Help] begginer's question
From: "jane huffam" <janehuffam@xxxxxxxxx>
Date: Wed, 1 Oct 2008 17:27:10 -0300
Dkim-signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:received:received:message-id:date:from:to :subject:mime-version:content-type; bh=BiKq40SSkQxfTOxxGVF7DRJ7peG8fBCeWx4oQCPw7K4=; b=a+ZI36DJaO0MFnJkiNKiTdJknzVCUbMKSUyH1132EDxV0igB8EaoBwqALsq6LpUOhB yoKwGFYn+znDe7xP/tozGOxRH+QfrE62k6LvN6iByNTORM/1gIT6dqm9/KVehjV8j7LD YI+U2C6ntHiICUkNN1O6tWe8E+G1ZF9q5KEG4=
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:mime-version:content-type; b=Q9/U4ljCx7RQaLzYBIqR7XzHqcVrGKoK4r509IAR4CctV/1mZ9CZQT8pnUlxTuNDZ9 W/FFDv9IinhdgOe6VZvukHHDSKo3cDKFr6yXRSxes/PxEbpSIxZx5ZWi/+ozo2M29R5w zVRASydwapNPFbyqxpTBHR9s9E+IBaUwCBLpw=
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

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!

Follow-Ups:
- Re: [PVS-Help] begginer's question
  - From: Cesar Munoz

Prev by Date: [PVS-Help] success running build from PVS source w/ CMUCL, Suse 11.0, gcclibs 4.3.1
Next by Date: Re: [PVS-Help] begginer's question
Previous by thread: [PVS-Help] success running build from PVS source w/ CMUCL, Suse 11.0, gcclibs 4.3.1
Next by thread: Re: [PVS-Help] begginer's question
Index(es):
- Date
- Thread