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

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

Dear all,

Thanks for your input. 

 > 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. 

My domains are finite (mostly, subsets of natural numbers) but ground
evaluator is not evaluating the quantifiers over them. Is there a way
to see the trace of what ground evaluator is doing? This should help
identify the problem. May be my declarations are not sufficient for the
evaluator to infer that the domains are finite. If I locate the
problem, I can possibly restructure the declarations to solve the problem.
 > It may be that you want to define a "new" existential quantifier for
 > your temporal logic. This is tricky as you cannot define binder

As of now, I'm trying the following:

exists?(s:set[t],f:pred[(s)):bool = exists (elt:(s)): f(s)

I think this should let me attach semantics to exists? as well as to
straight-a-way use quantifiers (here, exists) as defined in PVS while
working out proofs. I'll use exists? instead of exists everywhere.

 > 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.   

Can I not use both my semantic attachments and PVSio together? For the
things that are not evaluable in PVS and not defined in PVSio, I'll
have to give semantic attachments.

Another question related to PVSio and attachments. Can I use PVSio
functions in semantic attachments? I see it's not possible. For
example, I want to get a "new" string which is not already there in
the given set of strings. And I've axiomatized the function new but
for animating, I would like to get input from user and I "don't" want
to modify the original theory (as I want the animation to be
transparent to the user). So the only (?) option is to give a sematic

(push '|new| ...)
(defun |pvs_new| (strings)
(query_word "Please give a new string: ")
;; Validate that the string is not in "strings" )

As this won't work, I copy the code of query_word instead:

(defun |pvs_new| (string)
(prompt "Please give a new string: ")
  (format nil "~a" (read-token *standard-input* ""))
;; Validate that the string is not in "string")

Is this the way to go? I believe there should be a better way.

Best wishes,