Re: [PVS-Help] Error: ill-formed rule/strategy:

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Tommy,

The prover expects commands in lisp syntax, i.e., surrounded by
parentheses.  Use (flatten) instead and it should work.

Regards,
Sam


xiufeng liu <toxiufeng@gmail.com> wrote:

> Hi,
> 
> I have installed PVS 4.0 on Fedora 6.  When i type the any command at the
> end of rule?, I will receive the error:"ll-formed rule/strategy". But it
> works find on Fedora 4.  Would you like to tell me what the matter is?
> thanks
> 
> -tommy
> 
> ====================================
> 
> pvs(1):
> pvs(2):
> 
> prop :
> 
>   |-------
> {1}   (A IMPLIES (B IMPLIES C)) AND (A IMPLIES B) AND A IMPLIES C
> 
> Rerunning step: (postpone)
> Postponing prop.
> 
> prop :
> 
>   |-------
> {1}   (A IMPLIES (B IMPLIES C)) AND (A IMPLIES B) AND A IMPLIES C
> 
> Rule? flatten
> Ill-formed rule/strategy: flatten
> No change on: (skip)
> prop :
> 
>   |-------
> {1}   (A IMPLIES (B IMPLIES C)) AND (A IMPLIES B) AND A IMPLIES C
> 
> Rule?
> [1]+  Done                    ./pvs
> [lxf@xiliu PVS]$