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

Re: Automating proofs




Tamarah -

A starting point would be Rushby & Stringer-Calvert's `less elementary
tutorial', which describes some of the powerful built in strategies
such as (grind). This is available from:

     http://www.csl.sri.com/elementary-tutorial.html

The entire PVS documentation set is in the process of a rewrite, and will
include documentation of the strategy mechanism and how to get the most
out of the automation. Watch the pvs mailing list for future
announcements.

Hope that helps,

Dave

---
Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com