Implementazione OCaml di alcuni algoritmi di Logica e programmi di utilità

Corso di Logica e
Sistemi Informatici

Corso di Programmazione
Funzionale

Logica.
Linguaggio, Ragionamento,
Calcolo

Introduzione alla
Programmazione
Funzionale

prop.ml

Sorgente OCaml contente la dichiarazione di un tipo di dati per rappresentare formule proposizionali e la definizione di funzioni per operare su di esse, tra cui:

Trasformazione in forma normale negativa e congiuntiva.
Controllo della verità di una formula in un'interpretazione.
Generazione della tavola di verità di una formula.
Controllo di validità e ricerca di un modello con il metodo dei tableaux.

fol.ml

Sorgente OCaml contente la dichiarazione di un tipo di dati per rappresentare formule della logica dei predicati e la definizione di funzioni per operare su di esse, tra cui:

Sostituzione di variabili libere con termini.
Trasformazione in forma normale prenessa e forma normale di Skolem.
Rappresentazione di interpretazioni su un dominio finito e controllo della verità di formule chiuse in tali interpretazioni.
Rappresentazione di sostituzioni, applicazione e composizione di sostituzioni, unificazione.

In questa directory è contenuto il programma di utilità convert, che legge da un file una lista di formule (della logica proposizionale o dei predicati), scritte in una sintassi vicina a quella abituale, e scrive su un altro file (o su video) la rappresentazione interna di tali formule.

truthtable

In questa directory è contenuto il programma di utilità truthtable, che legge da un file una lista di formule proposizionali e stampa su un altro file (o su video) la tavola di verità, la forma normale congiuntiva a e la forma normale disgiuntiva di ciascuna formula.

tableau

In questa directory è contenuto il programma di utilità tableau, che legge da file un insieme S di formule proposizionali, scritte nella sintassi utilizzata anche da convert, e stampa su file o su video una rappresentazione linare di un tableau completo per S.

models

In questa directory è contenuto il programma di utilità models, che legge da file la specifica di un'interpretazione su un dominio finito e una formula e mostra (su file o su video) i passaggi per verificare se la formula è vera o falsa nell'interpretazione data.

prolog

In questa directory è contenuto un piccolo interprete Prolog, senza effetti collaterali e senza predicati predefiniti. Il programma viene letto da file, l'esecuzione è interattiva.