#2 selection in scope of negation possible

[Robert Hein]

Is is possible to select inside negation in negated
atoms and apply rules to the unnegated atom. This is
fatal for some deep inference systems, for instance
where weakening is present. The following unsound
inference is possible:

[tt, a]
w_---------
[-b, a]

with weakening. This is present in 0.9.4 and svn.

--Robert

[Robert Hein]

Logged In: YES
user_id=956614

As of svn revision 35 this bug is fixed at least on the
maude side. One can still select an atom behind a negation
and have rules applied to it. However, grape doesn't
anymore apply any rules on its own inside the scope of
negation. To fix the reminding issue we probably need to
extend the frontend by some knowledge of where rules can be
applied. An alternative approach might be to change the
syntax of atoms to something like:

sort aname
sort atom < structure .
op a b c d e : aname .
op - : aname -> atom .
op + : aname -> atom .

Since a,b,c etc are no structures anymore rules can only be
applied to +a or -a but not a.

--Robert