8.1 Una sessione al terminale

Nelle pagine seguenti è riportata una sessione al terminale. Si inzia facendo partire l'interprete Gödel, caricando una serie di moduli di sistema e infine caricando il modulo Theory, che implementa i predicati che operano sulla rappresentazione ground delle teorie oggetto.

Successivamente vengono caricati i moduli del progetto e si può iniziare a lanciare i goal. I messaggi di warning avvisano che i moduli che rappresentano le teorie sono composti solo di una parte locale: come precisato prima, la parte export è inutile non potendo questi moduli ereditare da altri.

Nelle risposte compare spesso qualcosa del tipo: $x= <Hidden>$; in questo caso si ha che alla variabile $x$ corrisponde un oggetto in rappresentazione ground, che non viene visualizzato dall'interprete (sarebbe lungo ed incomprensibile).

La convenzione utilizzata per rappresentare i predicati di uguaglianza, diseguaglianza e diseguaglianza universalmente quantificata è la seguente: $NEQ(x,t)$ corrisponde a $x \neq t$, $EQ(x,t)$ corrisponde a $x = t$ e $FALLNEQ(y,f(x_{1}, \ldots, x_{n}),Cons(x_{i}, \ldots,Cons(x_{j},Nil)))$ corrisponde a $\forall x_{i}, \ldots, x_{j} y \neq f(x_{1}, \ldots, x_{n})$.

Per riportare in forma di stringa le teorie oggetto risultato delle trasformazioni realizzate dagli operatori viene usato il predicato PutTheory che scrive in un file di nome nome_della_teoria.loc che viene posto nella directory corrente.