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

PVS and library functions

Dear PVS users.
I am looking for a theorem prover that supports the following features
(the following grocery list looks like a job add, but bear with me):
- First-Order Logic (or some non-too-distant variants)
- Easy-to-use strategy language
- Supports "library functions" such as the trigonometry functions
	"Sin", "Cos" and "Tan^(-1)" as well as real numbers (or an
	approximation thereof).

The following are advantageous but are not required:
- Has a complete proof procedure
- Is able to re-apply a proof guideline after the data has changed.

My experience is limited only to the PVS and Otter theorem provers, and
I think that none of them supports the above 3 first "musts". I do not
know of any use of "library functions" with PVS, unless someone here knows
of such an implementation or library/note that I managed to overlook.

Thanks much,

Eyal Amir