Unificazione per trasformazione

Question

Sto scrivendo un unificazione Algoritmo in F # per l'uso con AST Trasformazioni usando " termine riscrittura e tutto ciò " (Woldat ) di Franz Baader e Tobias nipkow.Per la sezione 4.6 Unificazione mediante trasformazione, è stata troppa teoria della math con gli esempi, e non chiaramente come mi sarebbe piaciuto.

Qualcuno può dare o indicare esempi più semplici che fanno uso delle trasformazioni:

Elimina, decomporre, orientare, eliminare.

Answer 1

Elimina: t = t è inutile e può essere rimosso dal set di equazioni.

1 =? 1 -> nil

.

Orient: Vogliamo tutte le equazioni sotto forma di x =? t, quindi capovolgere eventuali equazioni sotto forma di t =? x.

2 =? x1 -> x1 =? 2

.

Elimina: data x =? t, modificare tutte le altre equazioni per sostituire tutte le istanze di x con t.

x1 + x2 = 7, x2 = 5 -> x1 + 5 = 7, x2 = 5

.

decomporsi: dobbiamo prendere qualsiasi funzione ed eliminarli per ottenere equazioni sotto forma di x =? t.Si noti che questo processo tecnicamente rimuove solo una funzione alla volta.

x1 + 5 = 7 -> x1 = 2
2 * (x1 + x2) = 14 -> x1 + x2 = 7

.

Speriamo che questo aiuti.