Demodulatie (afleidingsregel)

In eerste-orde logica is demodulatie een afleidingsregel voor het afleiden van een nieuwe clausule bij resolutie met gelijkheid. Deze regel vervangt een term, bijvoorbeeld x, door een andere term die gelijk is aan x (bijvoorbeeld x = y). De gelijkheid wordt de demodulator genoemd. Demodulatie wordt ook het herschrijven van termen genoemd aangezien men het linkerdeel van de gelijkheid vervangt door het rechterdeel. Bij demodulatie werkt alleen van links naar rechts; bij paramodulatie wordt de gelijkheid beide kanten op gebruikt.

Definitie

Formeel verloopt demodulatie als volgt:

${\frac {x=y,\quad k_{1}\lor \ldots \lor k_{n}[z]}{k_{1}\lor \ldots \lor k_{n}'}}$

waarbij:

• z een term is die geünificeerd kan worden met x,
• k_n[z] een literaal waar z in voorkomt, en
• k_n' een literal waarin z is geünificeerd met x en vervangen door y.

Met behulp van verzamelingen kan deze regel als volgt genoteerd worden:

${\frac {\{x=y\},\quad \{k_{1},\ldots ,k_{n}[z]\}}{\{k_{1},\ldots ,k_{n}'\}}}$

Voorbeelden

Het predicaat p(f(a)) wordt met de demodulator f(x) = x gedemoduleerd tot p(a). Eerst wordt f(a) geünificeerd met f(x) door a in te vullen voor x (de demodulator wordt hierdoor f(a) = a) en vervolgens wordt f(a) vervangen door a.

Het is ook mogelijk demodulatie herhaaldelijk toe te passen: zo kan p(f(f(a))) met de demodulator f(x) = x gedemoduleerd worden tot p(a) door tweemaal demodulatie toe te passen (zoals bij het voorbeeld hierboven): eerst op f(a) waardoor men p(f(a)) krijgt en daarna opnieuw op f(a) om p(a) te krijgen.

Demodulatie is niet mogelijk op p(f(a)) met b = a (om eventueel p(f(b)) te verkrijgen) aangezien de gelijkheid alleen van links naar rechts gebruikt wordt.

Referenties

• Artificial Intelligence - A Modern Approach, Inference in First-Order Logic (Chapter 9), Resolution (Section 9.5), pagina 304 - Russell, A., Norvig, P., Second Edition, ISBN 0137903952