Hi list members,
We are now mechanically verifying the fault tolerant properties of safety critical distributed systems.
We want to prove a formula of a theory in batch mode, because the proof strategy for this formula has already
been generated. However, I haven’t found any suitable command in the PVS system guide for this. After viewing the help site of PVS, I found that Mr. Sam Owre has defined a function for this, which is shown below:
(defun my-prove-formula (theoryname formname)
(let ((*suppress-printing* t)
(if (eq (status-flag (prove-formula theoryname formname t)) '!)
(format t "~%Formula proved")
(format t "~%Formula unproved"))))
My problem is that how I can use this function as a PVS system command in batch mode? For example, I can write
(my-prove-formula (theoryname forname) “apply then* (flatten) ……(assert)”) in the .el file?
Thank you very much!
School of Computing, NUS