The beauty and beast algorithm: quasi-linear incremental tests of entailment and disentailment over trees
Andreas Podelski, Peter Van Roy · International Conference on Logic Programming · 1994
We consider the problem of the simultaneous tests of matching and non-unifiability (logically: entailment and disentailment over trees) where the input consists of one fixed term (one fixed constraint) and an incrementally growing set of variable bindings (the constraint store). These tests are used in logic programming systems with suspensions, e.g. for proving guards as in LIFE, AKL and Oz. A weaker version of the problem tests entailment only, which is sufficient for solving inequations as in Prolog-II and CLP(Rat). The on-line complexity of previous algorithms for either version of the problem is at least quadratic. We present an on-line algorithm which is quasi-linear.