PVS and library functions

[Eyal Amir <eyal@Steam.Stanford.EDU>]

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

---

• Prev by Date: Summary of generic verified refinement steps
• Next by Date: client access to PVS system.
• Prev by thread: Summary of generic verified refinement steps
• Next by thread: client access to PVS system.
• Index(es):
  • Date
  • Thread