MGU e standardizzazione variabile - CNF

Question

Ho letto sulla conversione prime frasi logiche per forma normale congiuntiva, e quindi l'esecuzione di risoluzione.

Una delle fasi di conversione in CNF, è quello di variabili Standardizzare: rinominare tutte le variabili in modo che ogni quantificatore ha un proprio nome variabile univoco

.

La maggior parte generale Unificatore è l'unificazione almeno specializzato di due clausole.

Domanda 1: ho cercato di trovare un esempio che mostra quali sono i potenziali problemi se non lo faccio standardizzare le variabili, ma tutte le risorse online ho trovato solo spiegare il "come" e non il "perché". Mi può fornire un esempio di un potenziale problema?

Domanda 2: lo stesso problema come la prima domanda. Che cosa succede se non usiamo MGU, ed usiamo un unificatore più specializzata? Quali sono i potenziali problemi? Mi può fornire con un esempio?

I miei sinceri ringraziamenti. Felipe

Answer 1

1. questa risposta - è un esempio di un insieme contraddittorio di clausole in cui non possiamo derivare una contraddizione senza rinominare variabili. Nota che non è sufficiente rinominare variabili solo dopo la conversione al CNF, dobbiamo rinominare le variabili per essere distinti prima di tutti applicazione della norma risoluzione. È possibile visualizzare nel modo seguente: Una variabile che appare in due distinte clausole ha un significato diverso in ognuno di essi come sono implicitamente universalmente quantificati. Se non si rinomina la variabile in una delle clausole, facciamo un falso presupposto che la variabile significa la stessa in entrambe le clausole.

2. Utilizzando MGU, deriviamo la clausola più generale in una fase di risoluzione. Se usiamo ogni unificatore che è più specializzata rispetto ai loro MGU, la clausola che ne risulta è più debole. Questo significa che non abbiamo inferire tutte le conoscenze che potevamo, e possiamo perdere una derivazione di una clausola vuota, anche se esiste. Per esempio: \ Begin {array} {c} P (x, y) \ lor Q (y) \\ \ Lnot Q (d) \\ \ Lnot P (c, d) \ End {array} Se facciamo una risolvente dalle prime due clausole che utilizzano MGU che invia $ y \ a D $, otteniamo $ P (x, d) $ e si può procedere con la terza clausola. Se prendiamo un unificatore più debole, come quella che invia anche $ x \ a D $, otteniamo $ P (d, d) $ e non siamo in grado di fare una risolvente con la terza clausola. Questo significa che il metodo non è completa.