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. -------------------------------------------------------------------