A Non-Binary Method for Finding Interpolants: Theory and Practice

Titolo

Un metodo non binario per trovare interpolanti: teoria e pratica.

1. Il Problema

L'articolo affronta il problema della ricerca di interpolanti nella logica proposizionale classica.

• Definizione: Dato che $A \to B$ è valido e che $A$ e $B$ condividono almeno una variabile proposizionale, un interpolante è una formula $C$ costruita esclusivamente con le variabili condivise da $A$ e $B$, tale che $A \to C$ e $C \to B$ siano entrambi validi (Teorema di Interpolazione di Craig).
• Contesto: Sebbene esistano diversi metodi teorici (es. Maehara, Kleene, Smullyan) e sistemi pratici utilizzati nell'automated theorem proving (come il sistema HKP basato sulla risoluzione binaria), gli autori mirano a sviluppare un approccio alternativo che sia concettualmente semplice e facilmente implementabile, superando le limitazioni dei metodi basati sulla risoluzione binaria classica.

2. Metodologia

L'approccio proposto si discosta dai metodi tradizionali basati sulla dimostrazione diretta o sulla risoluzione binaria, fondandosi invece sui sistemi di refutazione.

• Sistemi di Refutazione: Invece di cercare di provare che una formula è valida, il sistema si concentra su quali formule sono non valide (da rifiutare). Un sistema di refutazione è composto da assiomi di refutazione (formule non valide) e regole di refutazione che preservano la non validità.
• Il Sistema Proposto: Gli autori utilizzano un sistema di refutazione per la logica proposizionale classica (basato sui lavori di Skura). Le regole di refutazione agiscono eliminando coppie di letterali complementari ($l$ e $l^*$) da una formula in forma normale.
• Il "Trucco" Non Binario: La proprietà fondamentale su cui si basa l'algoritmo è che una formula $G$ è valida se e solo se entrambe le formule risultanti dall'eliminazione di una coppia di letterali ($G_1$ e $G_2$) sono valide.
  • A differenza della risoluzione binaria (che combina due clausole per eliminarne una variabile), questo metodo utilizza una forma di risoluzione non binaria. Le regole permettono di dividere il problema in due sottoproblemi ($G_1$ e $G_2$) mantenendo la struttura logica necessaria per costruire l'interpolante.
• Procedura Costruttiva:
  1. Si parte da $X \to Y$ (dove $X$ è in CNF e $Y$ in DNF).
  2. Si trasforma il problema in una forma normale clausale.
  3. Si applica ricorsivamente le regole di refutazione per eliminare coppie di letterali ($l, l^*$) finché non si raggiungono casi base (rank 0).
  4. Nei casi base, l'interpolante è $\top$ (Verum) o $\bot$ (Falsum) a seconda che la negazione di $X$ o $Y$ sia una tautologia.
  5. Si ricostruisce l'interpolante risalendo l'albero di ricorsione combinando gli interpolanti parziali ($I(G_1)$ e $I(G_2)$) tramite congiunzioni o disgiunzioni, a seconda della presenza dei letterali eliminati in $X$ o $Y$.

3. Contributi Chiave

1. Nuova Dimostrazione Teorica: Forniscono una nuova dimostrazione del teorema di interpolazione basata sui sistemi di refutazione, che è concettualmente semplice e costruttiva.
2. Approccio Non Binario: Introducono un metodo che non dipende dalla risoluzione binaria. Questo permette potenzialmente di ridurre il numero di passaggi necessari per trovare un interpolante rispetto ai sistemi tradizionali (come HKP).
3. Implementazione Pratica: Sviluppano uno script in Python che implementa l'algoritmo descritto. L'implementazione è un "proof-of-concept" che non applica ottimizzazioni umane (come saltare passaggi quando si notano tautologie immediate), per dimostrare la correttezza pura della procedura.
4. Analisi delle Prestazioni: Evidenziano che, sebbene gli interpolanti prodotti grezzi possano essere complessi e richiedere semplificazione, il metodo è efficiente in termini di passi computazionali.

4. Risultati Sperimentali

Gli autori hanno condotto esperimenti su un generatore di formule pseudo-casuali con diverse configurazioni:

• Configurazione A: 100.000 formule con fino a 4 variabili, 10 congiunzioni e 10 disgiunzioni.
  • Tempo medio di esecuzione: 0,0032 secondi.
  • Dimensione media dell'interpolante: 165 (operatori).
• Configurazione B: 50.000 formule con 20 congiunzioni e 20 disgiunzioni (sempre max 4 variabili).
  • Tempo medio di esecuzione: 0,011 secondi.
  • Dimensione media dell'interpolante: 346.
• Configurazione C (Estesa): 1.000 formule con fino a 10 variabili.
• Analisi dei Dati: I grafici mostrano una relazione lineare tra il tempo di esecuzione e la dimensione della formula di input/interpolante. Questo suggerisce che l'algoritmo scala bene, almeno nell'ambito della logica proposizionale testata.
• Confronto con HKP: Viene citato un esempio in cui il sistema HKP richiede 5 passaggi, mentre il metodo proposto ne richiede solo 2, confermando il vantaggio potenziale della risoluzione non binaria.

5. Significato e Conclusioni

• Validità Teorica: Il lavoro dimostra che i sistemi di refutazione, spesso visti come strumenti puramente teorici per la non validità, possono essere efficacemente ribaltati per costruire procedure pratiche di interpolazione.
• Efficienza: Il metodo non binario offre un potenziale vantaggio in termini di riduzione del numero di passi rispetto alla risoluzione binaria standard, rendendolo promettente per applicazioni nell'automated theorem proving.
• Sviluppi Futuri:
  • Semplificazione: Gli interpolanti prodotti sono spesso complessi e necessitano di ottimizzazione/semplificazione post-processo.
  • Estensione: La sfida principale futura è estendere questo sistema dalla logica proposizionale alla logica del primo ordine (FOL), un'area dove i metodi attuali sono più complessi.
  • Ottimizzazione: Sviluppare versioni più sofisticate del software che integrino euristiche per ridurre la dimensione degli interpolanti finali.

In sintesi, il paper presenta un approccio innovativo che unisce teoria della dimostrazione (refutazione) e pratica computazionale, offrendo un metodo alternativo ed efficiente per l'interpolazione logica.