[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:


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

Hope that helps,


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