A simple proof

[Julin S]

Hi.

I had trouble proving a simple theorem with PVS (it's my first proof in PVS).

I hope this is a right place to ask such doubts.

I was trying to prove something simple that I found from a recording for the 2021 SSFT summer school.

The task was to prove that 'I am my baby' if:
 - everyone like my baby
 - my baby likes only me

This is the source file:

```
mybaby: THEORY
BEGIN
  person: TYPE+
  me, mybaby: person
  x, y, z: VAR person
  loves(x, y): boolean

  everybodyLovesMyBaby: AXIOM
    forall x: loves(x, mybaby)

  mybabyLovesOnlyMe: AXIOM
    loves(mybaby, x) IMPLIES x = me
 
  mybabyIsMe: LEMMA
    mybaby = me
END mybaby
```

I started the proof with `M-x pr` (in emacs) and did

```
(lemma "everybodyLovesMyBaby")
(inst - "mybaby")
(lemma "mybabyLovesOnlyMe")
```

The goal had become:

```
mybabyIsMe :

{-1}  FORALL (x: person): loves(mybaby, x) IMPLIES x = me
[-2]  loves(mybaby, mybaby)
  |-------
[1]   mybaby = me
```

but when I tried

```
(forward-chain -)
```

I ran into error.

```
Rule? (forward-chain -)
debugger invoked on a UNDEFINED-FUNCTION in thread
#<THREAD "main thread" RUNNING {1008A46E73}>:
  The function PVS-JSON:UPDATE-PS-CONTROL-INFO-RESULT is undefined.

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

restarts (invokable by number or by possibly-abbreviated name):
  0: [CONTINUE      ] Retry calling PVS-JSON:UPDATE-PS-CONTROL-INFO-RESULT.
  1: [USE-VALUE     ] Call specified function.
  2: [RETURN-VALUE  ] Return specified values.
  3: [RETURN-NOTHING] Return zero values.
  4: [ABORT         ] Exit debugger, returning to top level.

("undefined function"
mybabyIsMe.1 :

{-1}  mybaby = me
[-2]  loves(mybaby, mybaby)
  |-------
[1]   mybaby = me
)
0]
```

What am I doing wrong?

Is it because I'm not using quotes somewhere?

I'm using pvs version 7.1.0

Am a total newbie to PVS.

[Julin S]

I'm running pvs on Debian 11 with SBLC.

The name of the file that I installed pvs from had 'pvs7.1.0-ix86_64-Linux-sbclisp' in it.

Just realized we can't reply by mail to the group.

[Julin S]

I just tried the same proof with allegro pvs (pvs7.1.0-ix86_64-Linux-allegro.tgz) and it worked.

So I guess the problem is shows up only with sbcl.

Unless I'm using a newer version.

[Paolo Masci]

Julin, yes this is the right place to ask these questions.

And yes, PVS Allegro is the version you should use.

Cheers,

Paolo

[Julin S]

>  yes, PVS Allegro is the version you should use

The SBCL would still be supported, right?

Or is allegro the only one that can be used for pvs?

[Paolo Masci]

Julin, yes, the SBCL version of PVS will be supported in future releases.

The problem you encountered is probably due to the erroneous inclusion in the SBCL version of PVS 7.1.0 of some functions that were meant to be included only for the Allegro version.

We are currently working with SRI on a new release of PVS that will resolve this issue and will also enhance significantly the performance of PVS.

Thanks for asking, and stay tuned for updates!

Paolo