tableau

Tableau

Il programma tableau può essere utilizzato per generare e stampare un tableau completo per una lista di formule proposizionali. Il programma si utilizza con la sintassi: 

   tableau [ -o <outputfile> ] <inputfile>
Se si omette l'argomento opzionale, il risultato viene stampato su video. Se si omettono entrambi gli argomenti, essi vengono richiesti in input.

Nel file <inputfile> deve essere contenuta una lista di formule proposizionali, separate da virgole e terminata da un punto. Un esempio e' nel file formule. I simboli usati per i simboli logici sono: 

   -   (negazione)
   &   (congiunzione)
   |   (disgiunzione)
   ->  (implicazione)
  <->  (doppia implicazione: viene espansa in una congiunzione
                             di implicazioni)
   T  (True)
   F  (False)
I nomi delle lettere proposizionali devono iniziare con una lettera alfabetica (minuscola o maiuscola), seguita da lettere alfabetiche, cifre e il carattere _.

L'output del programma produce una lista di nodi, etichettati da sequenze di $0$ e $1$, in modo tale che il figlio destro (o l'unico figlio) di un nodo etichettato dalla sequenza $b_0...b_n$ è etichettato da $b_0...b_n0$, il figlio sinistro, se esiste, dalla sequenza $b_0...b_n1$.

Ad esempio, se f3 è un file contenente solo la formula f3, cioè: 

    ((-p|q)&-(p->q)).
Il comando tableau f3 genererà l'output: 
Tableaux iniziale:
0: ((-pvq)&-(p->q))
Espansione di: 0: ((-pvq)&-(p->q))
Generato il nodo 00: (-pvq)
Generato il nodo 000: -(p->q)
Espansione di: 00: (-pvq)
Generato il nodo 0000: -p
Generato il nodo 0001: q
Espansione di: 000: -(p->q)
Generato il nodo 00000: p
Generato il nodo 000000: -q
Espansione del ramo terminata.
Ramo chiuso: -p, p, -q
Espansione di: 000: -(p->q)
Generato il nodo 00010: p
Generato il nodo 000100: -q
Espansione del ramo terminata.
Ramo chiuso: p, q, -q

L'albero rappresentato è il seguente:

Qui potete trovare il programma tableau precompilato per Linux e il programma tableau.exe per Windows.

Nella sottodirectory sources sono contenuti i sorgenti OCaml. Per ricompilare il programma sotto Linux, nella directory in cui sono posizionati i files, dare i comandi 

 
   touch .depend
   make parser
   make depend
   make native
Per ripulire la directory dai files creati dalla compilazioni, eccetto il programma: 
 
   make clean

Per compilare il programma sotto Windows, eseguire la batch win-make.bat, che crea il file tableau.exe. Per eseguire il programma utilizzando la sintassi 

 
   tableau
si puo' utilizzare una shell XEmacs, avviata con il comando 
 
  ESC X shell
(da una finestra XEmacs, premere il tasto ESC, poi il tasto X, poi digitare "shell" nella linea in basso in cui si e' spostato il cursore).