Unificazione: rimuovere le equazioni e aggiornare la soluzione

Question

Questa domanda riguarda l'unificazione del primo ordine. Supponiamo di avere un set $ d $ di equazioni e una soluzione a queste equazioni. Lascia che questa soluzione sia un set $ s $ di sostituzioni. Ora, supponiamo di rimuovere alcune equazioni da $ d $. Esiste un algoritmo che utilizza solo queste equazioni rimosse e aggiorna rapidamente $ D $, o l'unificazione deve essere fatta da zero?

(Nella mia applicazione, tendo ad avere molte equazioni, quindi è per questo che sono interessato a una soluzione che non ricompensa tutto.)