next up previous Sommario
Next: 3.3.4 Derivazione Up: 3.3 Negazione costruttiva Previous: 3.3.2 Diseguaglianze   Sommario

3.3.3 Regola di computazione

Come conseguenza delle considerazioni precedenti, escluse le diseguaglianze primitive, ogni sottogoal è candidato alla selezione, includendo anche quelli negativi non ground.

Le diseguaglianze valide o soddisfacibili, che sono selezionabili, possono essere identificate attraverso l'uso dell'unificazione. Una diseguaglianza $r \neq s$ è considerata insoddisfacibile se $r$ ed $s$ sono identici, cioè sono unificabili senza legami di variabili; una diseguaglianza è valida se $r$ ed $s$ non sono unificabili. Una diseguaglianza preceduta dal quantificatore universale $\forall$ ( $ \forall r \neq s$) è insoddisfacibile se $r$ ed $s$ possono essere unificati con legami delle sole variabili quantificate universalmente; tale diseguaglianza è valida se $r$ ed $s$ non sono unificabili.

Una regola di computazione efficiente è quella che seleziona una disuguaglianza insoddisfacibile il più presto possibile; infatti la selezione di tale diseguaglianza porterà al fallimento immediato del goal a cui appartiene il predicato selezionato.

In un sistema Prolog si può pensare di prendere come base la regola "left to right", cioè scegliere il predicato più a sinistra se è selezionabile, altrimenti tralasciarlo per il momento e passare a quello successivo.


next up previous Sommario
Next: 3.3.4 Derivazione Up: 3.3 Negazione costruttiva Previous: 3.3.2 Diseguaglianze   Sommario
Roberto Giungato 2001-03-14