next up previous Sommario
Next: 4. La terminazione di Up: 3.3 Negazione costruttiva Previous: 3.3.7 Correttezza e completezza   Sommario

3.3.8 Sottogoal negativi quantificati esplicitamente

Per trattare i sottogoal del tipo $\forall X \neg Q$ (e quelli equivalenti del tipo $\neg \exists X \; Q$), si procede nel modo seguente:

se il letterale selezionato contiene n variabili $X_{1}, \ldots, X_{n}$ e il sottogoal è $\forall (X_{1}, \ldots, X_{m}) \neg Q$, si normalizza e si nega la risposta a Q rispetto soltanto a $X_{m+1}, \ldots, X_{n} $ e si procede come al solito.



Roberto Giungato 2001-03-14