| has gloss | nld: In eerste-orde logica is demodulatie is 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. |