Re: [PVS-Help] Getting the prover to use axioms

[Cesar Munoz <munoz@xxxxxxxxxx>]

You have to use the axiom as a lemma, e.g.,

(lemma "AxMaxId)

and then

(assert).

Cesar

Nikhil Dinesh wrote:
> Hi,
> 
> I've been unable get the prover to use axioms in the theory. For example:
> 
> state : THEORY
> 
>   BEGIN
> 
>   State : TYPE =
>    [#
>      fDomain : [nat -> bool],
>      fGetAtt : [nat, string -> string],
>      fMaxId : nat
>    #]
> 
> 
>   s : VAR State
>   i : VAR nat
> 
>   AxMaxId : AXIOM
>     FORALL s:
>      LET maxId = fMaxId(s) IN
>      LET d = fDomain(s) IN
>       FORALL i: d(i) => i < maxId
> 
>    ThCheck2 : CONJECTURE
>     FORALL s:
>      LET d = fDomain(s) in
>      LET maxId = fMaxId(s) IN
>       FORALL i: d(i) => i < maxId
> 
> 
>   END state
> 
> The conjecture is identical to the axiom...so it should be provable,
> right? Here is the output of M-x  pr:
> 
> ThCheck2 : 
> 
>   |-------
> {1}   FORALL s:
>         LET d = fDomain(s) IN
>           LET maxId = fMaxId(s) IN FORALL i: d(i) => i < maxId
> 
> Rule? (grind)
> Trying repeated skolemization, instantiation, and if-lifting,
> this simplifies to:
> ThCheck2 : 
> 
> {-1}  i!1 >= 0
> {-2}  fDomain(s!1)(i!1)
>   |-------
> {1}   i!1 < fMaxId(s!1)
> 
> How do I get the prover to use AxMaxId?
> 
> Thanks,
> -Nikhil
> 
> 
> 


-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace         mailto:Cesar.A.Munoz@nasa.gov
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4