Computing Witnesses Using the SCAN Algorithm

1. Enunciato del Problema

Il documento affronta l'Eliminazione dei Quantificatori del Secondo Ordine (SOQE), il problema di trovare una formula del primo ordine $\psi$ logicamente equivalente per una data formula del secondo ordine $\exists X \phi$ (dove $\phi$ è del primo ordine). Sebbene la SOQE sia indecidibile in generale, esistono algoritmi pratici per specifiche sottoclassi.

Gli autori introducono un problema più generale chiamato Eliminazione dei Quantificatori del Secondo Ordine con Testimone (WSOQE). Invece di trovare semplicemente una formula del primo ordine equivalente, l'obiettivo è trovare un testimone: una tupla di predicati del primo ordine $\alpha$ tale che:
$$\exists X \phi \equiv \phi[X \leftarrow \alpha]$$
Ciò significa che la formula del secondo ordine è equivalente alla formula del primo ordine ottenuta sostituendo le variabili predicative $X$ con definizioni specifiche del primo ordine $\alpha$.

Significato della WSOQE:

• Colma il divario tra la SOQE e le Equazioni di Formula (FEQ) (trovare $\alpha$ tale che $\models \phi[X \leftarrow \alpha]$).
• È cruciale per applicazioni nella rappresentazione della conoscenza (oblio/proiezione), nella teoria della corrispondenza modale e nella verifica dei programmi (trovare invarianti di ciclo).
• A differenza della SOQE standard, che produce solo il risultato, la WSOQE fornisce la definizione dei predicati eliminati, preservando la struttura della base di conoscenza.

2. Metodologia: L'Algoritmo WSCAN

Gli autori propongono WSCAN, un'estensione dell'esistente algoritmo SCAN (un dimostratore di teoremi basato sulla saturazione per la SOQE). La metodologia di base coinvolge due fasi principali:

A. La Derivazione SCAN

L'algoritmo opera su insiemi di clausole. Trasforma la formula di input in forma normale clausale ed esegue un processo di saturazione utilizzando un calcolo di inferenza specifico $\mathcal{I}$:

1. Risoluzione e Fattorizzazione con Vincoli: Invece della unificazione standard, queste regole introducono vincoli di disuguaglianza (ad es. $t \not\simeq t'$) tra termini.
2. Eliminazione dei Vincoli: Unifica i termini per rimuovere i vincoli.
3. Regole di Cancellazione:
   • Cancellazione di Purezza Estesa: Rimuove le clausole contenenti $X$ se $X$ appare con una sola polarità (tutte positive o tutte negative).
   • Cancellazione di Clausola Purificata: Rimuove una clausola $P$ contenente $X$ se sono state eseguite "sufficienti" inferenze tali che il restante insieme di clausole implichi logicamente la chiusura per risoluzione di $P$. Questo è formalizzato tramite un criterio di ridondanza in avanti che coinvolge l'eliminazione delle variabili e la subsumption.

Il processo continua fino a quando tutti i letterali $X$ non sono eliminati, risultando in un insieme di clausole del primo ordine $N^*$ equivalente a $\exists X N$.

B. Costruzione del Testimone (Dal Basso verso l'Alto)

Il contributo innovativo è l'estrazione di un testimone $\sigma$ dalla storia della derivazione. L'algoritmo costruisce il testimone all'indietro (dallo stato finale allo stato iniziale):

1. Caso Base: Se l'insieme di clausole finale $N_m$ non contiene $X$, la sostituzione identità è un testimone.
2. Passo Induttivo: Per ogni passo di derivazione $S_i$ che trasforma $N_{i-1}$ in $N_i$, l'algoritmo calcola una sostituzione $\tau_{S_i}$ tale che se $\sigma_i$ è un testimone per $N_i$, allora $\tau_{S_i}\sigma_i$ è un testimone per $N_{i-1}$.
   • Per i passi di inferenza standard (Risoluzione, Fattorizzazione, ecc.), $\tau$ è l'identità.
   • Per la Cancellazione di Purezza Estesa, $\tau$ imposta $X$ a $\top$ o $\bot$ a seconda della polarità.
   • Per la Cancellazione di Clausola Purificata (il caso complesso), l'algoritmo costruisce un testimone basato sulla chiusura per risoluzione locale della clausola cancellata.

C. Gestione dei Testimoni Infiniti

La chiusura per risoluzione utilizzata per le clausole purificate può essere infinita, portando a testimoni infiniti (espressi come congiunzioni infinite). Il documento introduce due soluzioni:

1. Testimoni a Punto Fisso: Il testimone infinito è espresso come un massimo punto fisso ($gfp$) nella logica dei punti fissi. Ciò fornisce una rappresentazione finita della definizione potenzialmente infinita.
2. Testimoni del Primo Ordine (Condizione Aciclica): Gli autori definiscono una condizione chiamata purificazione $k$-aciclica. Se il "grafo di subsumption della purificazione" associato a un passo di cancellazione è aciclico, il testimone può essere calcolato come un predicato finito, del primo ordine, utilizzando un'iterazione limitata della chiusura per risoluzione.

3. Contributi Chiave

1. Algoritmo WSCAN: Un metodo completo per calcolare testimoni per la SOQE su insiemi di clausole, estendendo l'algoritmo SCAN.
2. Dimostrazioni di Correttezza:
   • Dimostrazione che la sostituzione costruita $\sigma$ è un testimone valido ($\exists X N \equiv N\sigma$).
   • Una nuova dimostrazione di correttezza per l'algoritmo SCAN originale derivata dalla logica di costruzione del testimone.
3. Garanzia di Testimone del Primo Ordine: Identificazione della condizione di purificazione aciclica, che garantisce che il testimone risultante sia una formula del primo ordine (evitando espressioni infinite o a punto fisso).
4. Estensione del Lemma di Ackermann: Gli autori dimostrano che il loro metodo include il Lemma di Ackermann (un metodo classico per la SOQE) e lo estende a casi in cui il predicato appare con polarità mista.
5. Gestione di Teorie di Sfondo: Il metodo è esteso per gestire il ragionamento sull'uguaglianza (tramite paramodulazione) e teorie di sfondo del primo ordine, permettendo di risolvere problemi di raggiungibilità nei grafi e altri problemi di clausole Horn vincolate.
6. Implementazione Prototipale: Un'implementazione prototipale nel pacchetto software GAPT (General Architecture for Proof Theory) (versione 2.19.0).

4. Risultati e Valutazione

• Implementazione: Il prototipo è stato testato su 44 esempi (dalla letteratura e personalizzati).
• Prestazioni:
  • Sono state trovate derivazioni SCAN per il 90,9% degli esempi (40/44) entro un timeout di 10 secondi.
  • Il calcolo del testimone è stato estremamente veloce (media 0,619 ms) rispetto alla ricerca della derivazione (media 375 ms).
  • Le dimensioni dei testimoni sono state generalmente piccole (media 6,9 simboli).
• Capacità: Il sistema ha calcolato con successo testimoni del primo ordine per derivazioni che in precedenza producevano testimoni infiniti o richiedevano logica a punto fisso, specificamente in casi che coinvolgono grafi di purificazione aciclici.
• Limitazioni:
  • Il metodo richiede che l'input sia un insieme di clausole (variabili di dominio quantificate universalmente).
  • Non può gestire casi in cui è necessaria la skolemizzazione e non può essere invertita (ad es. $\exists X \exists u \exists v (X(u) \land \neg X(v))$), poiché il testimone risultante conterrebbe costanti di Skolem non presenti nel linguaggio originale.
  • Lo spazio di ricerca per le derivazioni può essere grande; l'implementazione corrente utilizza il backtracking ma non è ottimizzata per insiemi di clausole massicci.

5. Significato

Questo lavoro è significativo perché trasforma l'algoritmo SCAN da uno strumento che meramente elimina i quantificatori in uno che sintetizza le definizioni dei predicati eliminati.

• Ponte Teorico: Unifica i campi dell'Eliminazione dei Quantificatori del Secondo Ordine (SOQE) e delle Equazioni di Formula (FEQ), mostrando che sono due facce della stessa medaglia.
• Applicazione Pratica: Fornendo definizioni esplicite del primo ordine (testimoni), il metodo è direttamente applicabile a:
  • Rappresentazione della Conoscenza: Creazione di interpolanti uniformi e oblio di predicati mantenendo la struttura logica.
  • Verifica: Generazione automatica di invarianti di ciclo per la verifica dei programmi (risoluzione di clausole Horn vincolate).
  • Logica Modale: Calcolo di assiomi di corrispondenza per logiche modali.

Il documento stabilisce che per una vasta classe di derivazioni (quelle con grafi di purificazione aciclici), il complesso problema del secondo ordine può essere ridotto alla ricerca di un testimone finito del primo ordine, offrendo un potente nuovo strumento per il ragionamento automatico.