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

[PVS-Help] PVS logical engine

To: pvs-help@xxxxxxxxxxx
Subject: [PVS-Help] PVS logical engine
From: Gergely Buday <gbuday@xxxxxxxxx>
Date: Mon, 11 Oct 2010 17:14:23 +0200
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma;h=domainkey-signature:mime-version:received:received:date:message-id:subject:from:to:content-type;bh=CD4Bjxc6UZ7PVmcgBny8zQv6scVTdUD5kbD7fn3yWKw=;b=qOEoQOvyhSmVhj2vN+Pdz2QCSeddn7GXtfE8NJAKTDboqvl3fmnCQJOtyndewnOVtQApABDs3Mq0ECQc4b6znOQW2wbsqOXcrXCfSany06i4A+lX8i0CoZSkieYL/EF/UVMZc2eom3iv00ojahAw8mh0Twzft78+4wv/sr9psbE=
DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma;h=mime-version:date:message-id:subject:from:to:content-type;b=Pj379G5PSLIShHyLIAAeggLAVGakzF3svXtDqdVliBlpNBT8P5J1gvE81gr22uzimSkTztXdUsp0aAa+tkQLuLJv21Dlh+m+zHerM7P9iK4rpRMPh2VWvXLihba1IxovnZF4xqK5tSKfgKBB4f43vZ1+Xmqc9NlUEKfwmKPwL6w=
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

Dear PVS users,

I'm interested in the logical inference engine of PVS. I have found

The Formal Semantics of PVS

http://pvs.csl.sri.com/papers/csl-97-2/csl-97-2.ps

for the logical metatheory of PVS. I would be interested also in the
algorithms used. What papers need I read?

Best Wishes

- Gergely

Prev by Date: [PVS-Help] inductive predicates
Next by Date: [PVS-Help] not a valid pvs file
Prev by thread: Re: [PVS-Help] not a valid pvs file
Next by thread: [PVS-Help] inductive predicates
Index(es):
- Date
- Thread