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

Re: [PVS-Help] Semantic attachments for evaluating quantifiers



Aditya,

I don't believe that you can define a semantic attachment to "exists" as
the quantifiers are not regular PVS functions. By default, the ground
evaluator evaluates quantifiers provided that they quantify over a
finite domain. 

It may be that you want to define a "new" existential quantifier for
your temporal logic. This is tricky as you cannot define binder
operators directly in PVS. There are, however, some ways to do that. One
way is via Higher Order Abstract Syntax (HOAS), where essentially you
encode your quantifier using lambda-expressions. Another technique is De
Bruijn indices, where you encode higher order expressions in a
first-order system.

As for the second question, it is not a good idea to mix PVSio semantic
attachments (the ones that you write in pvs-attachments) with bare bone
semantics attachments (the ones that you write in .pvs.lisp). PVSio
semantic attachments are *safe* vis-a-vis the theorem prover, bare bone
semantic attachments are not. Unless you have a very powerful reason to
write semantic attachments directly in PVS, I highly recommend to use
PVSio for that (using the macro defattach in the file pvs-attachments).


However, if you really want to write your semantic attachments directly
in .pvs.lisp, and you are confortable with that, unload PVSio from the
context. Just remove the file .pvs_context and re-typecheck your
theories.  

Cesar

On Fri, 2005-06-10 at 12:44, Aditya Kanade wrote:
> Hi,
> 
> I need to evaluate temporal formulae in PVS. For that firstly I've to
> give semantic attachments for quantifiers. I tried the following:
> 
> (push (mk-name '|exists| nil '|prelude|) *pvs2cl-primitives*)
> 
> ;; 2 underscores in pvs__exists as it takes more than one argument
> ;; Ref. [Evaluating, Testing, ... PVS specifications]
> 
> (defun |pvs__exists| (p type)
>   (let ((result nil))
>   (dolist (elt type result)
> 	(setq result (or (p elt) result))
> 	(when result (return t)))))
> 
> This is not working. Can anyone point out the problem (I think I don't
> know how "exists" takes its arguments) and suggest a solution?
> 
> Secondly, in the above said reference, the name of attached function
> starts with "PVS_" and the lisp code is supposed to written in
> .pvs.lisp file in current context (or home). But that too didn't work
> for me. I'd to start the name of attached function with "pvs_" and had
> to put the code in pvs-attachments file in the current context. Is
> there any change in recent implementations or is it a side effect of
> loading PVSio package?
> 
> Thanks.
> 
> Best wishes,
> Aditya.
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way                 http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988