Theorem Prover incentrato sull’utilizzo di hash table per Logiche Modali Non-Normali

Presentiamo l’implementazione della struttura dati delle tabelle hash per HYPNO (HYpersequent Prover for NOn-normal modal logics), un dimostratore di teoremi e generatore di contromodelli per logiche modali non-normali basato su Prolog. L’implementazione delle tabelle viene utilizzata per scoprire se sia possibile o meno migliorare le prestazioni di HYPNO sostituendo le attuali liste utilizzate all’interno del codice con la nuova struttura dati. Viene fornita una descrizione dell’implementazione delle tabelle di hash, così come le sue operazioni più importanti prima di passare alla fase di valutazione delle prestazioni. Gli esperimenti effettuati mostrano un leggero miglioramento delle performance di HYPNO, in particolare effettuando test con formule generate randomicamente. Questo suggerisce che l’applicazione delle tabelle di hash all’interno del theorem prover porti a un incremento delle prestazioni.