]> matita.cs.unibo.it Git - helm.git/commitdiff
This alternative version of disambiguate.crit2 implements the following
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Nov 2007 15:59:43 +0000 (15:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 23 Nov 2007 15:59:43 +0000 (15:59 +0000)
criterion for spurious error detection:

an error is spurious iff:
  a) it is obtained interpreting the symbol s with the interpretation \phi
  b) there exists another interpretation \phi' such that
     1) dom(\phi) = dom(\phi')
     2) \phi' is valid
     3) \phi(x)=\phi'(x) for each x != s

More (but not too many) errors are spurious according to this criterion.


No differences found