WinKE: Known Bugs
=================
If you find a bug in WinKE please send a short description to:
Ulle Endriss
-------------------------------------------------------------------
(1) In automated deduction mode, when applying a quantifier rule,
WinKE may unnecessarily rename bound variables. This happens
whenever the variable x to be substituted also has a bound
occurrence within the scope of x.
Example: Apply gamma-rule to (Ax)(P(x) v (Ax)Q(x)) with
substitution [x <- c]. The result should be P(c) v (Ax)Q(x),
but WinKE generates P(c) v (Ac)Q(c).
In particular when you are substituting with a term that is not
just a constant, this can cause serious problems further down a
proof and should be fixed eventually. In the meantime, please use
distinct variable names for every quantifier (this may be a good
idea to do anyway, for reasons of readability).
-------------------------------------------------------------------
(2) If you select two formulas on *different* branches as premises
for a beta or eta rule or for the closure rule, WinKE allows you
to apply that rule, thereby leading to the construction of
incorrect proof trees!
This is a serious problem, but fortunately students seem unlikely
to make that sort of mistake by accident.
Thanks to Sonia Gatti (Ferrara) who found this bug.
-------------------------------------------------------------------
(3) When using the Renumber option from the Problem menu the
bookkeeping information on whether a formula has been analysed on
all open branches can get distorted.
-------------------------------------------------------------------
(4) The strategy of restricting the gamma rule to so-called "useful
instantiations" is somewhat critical in view of the generation of
countermodels, because the gamma rule may not get applied to all
named elements of the domain. (While on the one hand, deduction
should stop once there are no more useful instantiations, the
generation of countermodels, on the other hand, should not be
possible in certain cases.)
-------------------------------------------------------------------
(5) A bug in the module used to compute the set of "useful
instantiations" before the application of the gamma rule can cause
problems in Assistant mode as well as during automated deduction.
A sample problem where this occurs would be the following:
(Ax) P(x,x)
(Ax) P(x,f(x))
Thanks to Jan Denef (Leuven) who found this bug. Thanks are also
due to Johan Wittocx (also Leuven) for spotting another problem
with the implementation of the algorithm for finding useful
instantiations.
-------------------------------------------------------------------
(6) When applying the gamma rule, the variable in question should
be substituted with a ground term. However, WinKE also allows
substitution with terms including symbols that are already being
used to represent variables. This can lead to unsound proof steps.
For example, this would allow us to infer (Ey)R(y,y) from the
formula (Ax)(Ex)R(x,y), which is clearly not correct.
Thanks to Ivano Ciardelli (Amsterdam) who reported this bug.
-------------------------------------------------------------------