next up previous Sommario
Next: 3.3.3 Regola di computazione Up: 3.3 Negazione costruttiva Previous: 3.3.1 Risoluzione SLDCNF   Sommario

3.3.2 Diseguaglianze

Il predicato di disuguaglianza è fondamentale nella NC: esso permette di estendere l'uso delle variabili logiche, che sono così usate per avere informazioni su valori che non sono ancora stati calcolati. Usando la stessa variabile logica, si forzano due valori sconosciuti ad essere lo stesso valore, ma la nozione duale di forzare due valori sconosciuti ad essere diversi non è immediata e la maggior parte delle volte è omessa.

Sebbene il predicato $\neq$ (d'ora in poi chiameremo così il predicato di disuguaglianza) sia fornito come "built-in" in vari sistemi Prolog, l'implementazione è in generale inadeguata. In molti sistemi è trattato solamente un predicato $\neq$ molto semplice: di solito si tratta di diseguaglianze decidibili, per esempio diseguaglianze ground.

Diseguaglianze che non sono ground ma soddisfacibili hanno bisogno di una manipolazione più complessa (p.e. $x \neq a$).

Se ci restringiamo ad un universo di Herbrand finito, è sempre possibile sostituire una diseguaglianza con una equivalente disgiunzione di uguaglianze. Questo metodo è in generale inefficiente. Quando ci sono funzioni, l'universo di Herbrand è infinito e non è sempre possibile trovare una disgiunzione di uguaglianze equivalente che sia finita (p.e. $x \neq y$).

La soluzione scelta da Chan per trattare le diseguaglianze soddisfacibili ma non valide, dette diseguaglianze primitive, è quella di postporle finché possibile; infatti una congiunzione di diseguaglianze soddisfacibili rimane soddisfacibile.


next up previous Sommario
Next: 3.3.3 Regola di computazione Up: 3.3 Negazione costruttiva Previous: 3.3.1 Risoluzione SLDCNF   Sommario
Roberto Giungato 2001-03-14