Maude-help mailing list

[Francisco Duran <duran AT lcc.uma.es>]

Hi Hubert,

Unconditional rules with variables in their righthand sides not 
appearing in their lefthand sides cannot be executed. The admissibility 
of conditional rules (equations and memberships) is trickier (look to 
the Maude manual for a concrete definition). One need strategies for 
executing non-admissible rules. In Maude 1 the system just not consider 
them when rewriting. Since Maude 2 the system checks whether the rules 
are admissible, and  gives error messages when they are not, giving 
error messages like the ones you have got. Maude assumes that those 
rules that cannot be executed (without strategies) are marked with the 
nonexec attribute.

Best regards,

Paco Duran


Hubert Wagner wrote:

> Hello.
>
> we have tried to run one of the older examples (sequents.maude) with 
> Maude 2.
> Here we get the following error message:
>
> mod SEQUENT-RULES-PROP-LOG
> Advisory: redefining module SEQUENT-RULES-PROP-LOG.
> Warning: "sequents.maude", line 11 (mod SEQUENT-RULES-PROP-LOG): 
> variable P is
>    used before it is bound in rule:
> rl empty => |- (P,~ P) [label Identity] .
> Warning: "sequents.maude", line 19 (mod SEQUENT-RULES-PROP-LOG): 
> variable P is
>    used before it is bound in rule:
> rl |- R => |- (P,R) [label Weakening] .
>
> I assume that this example has worked with Maude 1. What are the 
> essential changes in Maude 2 that this
> example no longer works with Maude 2? What have I to change in the 
> source code of sequents.maude
> so that I can use it with Maude 2?
>
> Thanks in advance.
>
> Best regards,
>
> Hubert Wagner
>
> -------------------------------------------
>
> Dr. Hubert Wagner
> FB Informatik
> University of Dortmund
> D 44221 Dortmund
> Germany
>
> Email:  
> Hubert.Wagner AT udo.edu
>
> _______________________________________________
> Maude-help mailing list
> Maude-help AT maude.cs.uiuc.edu
> http://maude.cs.uiuc.edu/cgi-bin/mailman/listinfo/maude-help