Analisi delle prestazioni di un theorem prover per le logiche condizionali: sviluppo di un benchmark per test automatici

In questo documento viene presentata ProLogicGen, un’applicazione che permette di generare formule casuali al fine di testare alcuni ragionatori automatici esistenti. L’obiettivo è quello di creare un benchmark per l’esecuzione di test automatici, al fine di testare le prestazioni di un theorem prover per le logiche condizionali. A tale scopo, sono state utilizzate le regole per le logiche con cui è stato allenato CondLean4.0. L’applicazione nasce per la generazione di formule che appartengono alla logica proposizionale condizionale, ma può essere usata per la quasi totalità delle formule per la logica proposizionale. Oltre alla generazione casuale, l’applicazione permette di specificare uno schema alla quale le formule devono appartenere: se, per esempio, viene richiesto lo schema A→B, allora il programma provvede a generare formule del tipo p→q piuttosto che (p∧q) →(p∨q). In pratica, l’applicazione prende in input una formula che contiene, oltre ai connettivi, anche una serie di meta-variabili e le sostituisce con delle formule generate casualmente. Ovviamente, ad una stessa meta-variabile deve corrispondere una stessa formula (è possibile che più meta-variabili abbiano la stessa formula, ma la probabilità è estremamente bassa grazie alla casualità con cui vengono create le formule). Questa funzionalità permette, ad esempio, di generare formule valide appartenenti alle logiche condizionali ID, CM, CEM e MP, con le quali è possibile effettuare alcuni test. L’applicazione permette inoltre di utilizzare direttamente un programma Prolog che, grazie alle regole per la logica condizionale di CondLean4.0, permette di verificare se le formule appartengono alla logica specificata. Le formule con cui vengono eseguiti i test devono appartenere ad una delle logiche condizionali sopra citate. Non viene permessa l’esecuzione di test con formule che non appartengono a nessuna logica: vista la casualità con cui vengono generate, è altamente improbabile che una formula di questo tipo dia esito positivo al test. Queste funzionalità servono per garantire all’utente la possibilità di generare le formule e verificarne l’attendibilità entro un certo intervallo di tempo, dopo aver inizializzato opportunamente l’ambiente di lavoro.