[Prev][Next][Index][Thread]
semi-unification
Date: Mon, 17 Jul 89 20:08:47 CET
I've become interested in semi-unification (see the LICS 89 paper
of Kfouri et al., for instance). Before I waste more time on it,
I would like to ask a few things:
1. Is the general problem still open (Kapur et al. solved it for
one inequation, Kfouri et al. for inequations with linear LHSs)?
2. Is it clear why Kapur et al's techniques don't extend to the general
case, or may they?
3. Are there people expecting the problem to be undecidable?
(It seems we have a proof that the problem is undecidable
for rational trees ("cyclic terms"), but this proof really
exploits the availibility of infinite trees).
Gert Smolka, IBM Deutschland, smolka@ds0lilog.bitnet