Sara

Ho risolto, utilizzando comunque il pacchetto bussproofs: anzichè utilizzare l’ambiente prooftree ho messo i comandi per generare i sequenti “sciolti” dentro la tabella e ho aggiunto alla fine di ognuno il comando \DisplayProof.
`
\begin{center}
\begin{tabular}{cccccc}
\hline
\multicolumn{2}{|c|}{
\AxiomC{}
\UnaryInfC{$\Gamma, \phi, \Gamma' \vdash \Delta, \phi, \Delta'$}
\DisplayProof
} & \multicolumn{2}{|c|}{
\AxiomC{}
\UnaryInfC{$\Gamma, \bot, \Gamma' \vdash \Delta$}
\DisplayProof
} & \multicolumn{2}{|c|}{
\AxiomC{}
\UnaryInfC{$\Gamma \vdash \Delta, \top, \Delta'$}
\DisplayProof
}\\
\hline
\multicolumn{3}{|c|}{
\AxiomC{$\Gamma, \phi, \psi \vdash \Delta$}
\UnaryInfC{$\Gamma, \phi \wedge \psi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{|c|}{
\AxiomC{$\Gamma \vdash \phi, \Delta$}
\AxiomC{$\Gamma \vdash \psi, \Delta$}
\BinaryInfC{$\Gamma \vdash \phi \wedge \psi, \Delta$}
\DisplayProof
}\\
\hline
\multicolumn{3}{|c|}{
\AxiomC{$\Gamma, \phi \vdash \Delta$}
\AxiomC{$\Gamma, \psi \vdash \Delta$}
\BinaryInfC{$\Gamma, \phi \vee \psi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{|c|}{
\AxiomC{$\Gamma \vdash \phi, \psi, \Delta$}
\UnaryInfC{$\Gamma \vdash \phi \vee \psi, \Delta$}
\DisplayProof
}\\
\hline
\multicolumn{3}{|c|}{
\AxiomC{$\Gamma \vdash \phi, \Delta$}
\AxiomC{$\Gamma, \psi \vdash \Delta$}
\BinaryInfC{$\Gamma, \phi \rightarrow \psi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{|c|}{
\AxiomC{$\Gamma, \phi \vdash \psi, \Delta$}
\UnaryInfC{$\Gamma \vdash \phi \rightarrow \psi, \Delta$}
\DisplayProof
}\\
\hline
\multicolumn{3}{|c|}{
\AxiomC{$\Gamma \vdash \phi, \Delta$}
\UnaryInfC{$\Gamma, \neg \phi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{|c|}{
\AxiomC{$\Gamma, \phi \vdash \Delta$}
\UnaryInfC{$\Gamma\vdash \neg \phi, \Delta$}
\DisplayProof
}\\
\hline
\multicolumn{3}{|c|}{
\AxiomC{$\Sigma, \Gamma, \Theta, \Gamma', \Sigma' \vdash \Delta$}
\UnaryInfC{$\Sigma, \Gamma', \Theta, \Gamma, \Sigma' \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{|c|}{
\AxiomC{$\Gamma \vdash \Sigma, \Delta, \Theta, \Delta', \Sigma'$}
\UnaryInfC{$\Gamma \vdash \Sigma, \Delta', \Theta, \Delta, \Sigma'$}
\DisplayProof
}\\
\hline
\end{tabular}
\end{center}
`
L’unica cosa che ora non mi torna è come mai ora la prima riga della tabella (che è composta da tre celle) ha la prima cella più larga delle altre due, nonostante nel codice siano tutte e tre multicolumn{2}…

[attachment=2740]tabella.pdf[/attachment]

Penso di aver risolto il problema pur mantenendo il pacchetto bussproofs, anzichè utilizzare l’ambiente prooftree ho inserito i sequenti in linea e dopo ogni sequente ho aggiunto il comando \DisplayProof nel modo seguente:
`
\AxiomC{}
\UnaryInfC{$\Gamma, \phi, \Gamma' \vdash \phi$}
\DisplayProof
`

Ora ho scritto il seguente codice:
`
\section{Logica proposizionale intuizionista}

AAAAAAAAAAAAAAAAAAAAAAAAA

\begin{table}[]
\centering
\begin{tabular}{cccccccccccc}
\multicolumn{4}{c}{
\AxiomC{}
\UnaryInfC{$\Gamma, \phi, \Gamma' \vdash \phi$}
\DisplayProof
} & \multicolumn{4}{c}{
\AxiomC{}
\UnaryInfC{$\Gamma, \bot, \Gamma' \vdash \phi$}
\DisplayProof
} & \multicolumn{4}{c}{
\AxiomC{}
\UnaryInfC{$\Gamma \vdash \top$}
\DisplayProof
}\\
\multicolumn{6}{c}{
\AxiomC{$\Gamma, \phi, \psi \vdash \gamma$}
\UnaryInfC{$\Gamma, \phi \wedge \psi \vdash \gamma$}
\DisplayProof
} & \multicolumn{6}{c}{
\AxiomC{$\Gamma \vdash \phi$}
\AxiomC{$\Gamma \vdash \psi$}
\BinaryInfC{$\Gamma \vdash \phi \wedge \psi$}
\DisplayProof
}\\
\multicolumn{6}{c}{
\AxiomC{$\Gamma, \phi \vdash \gamma$}
\AxiomC{$\Gamma, \psi \vdash \gamma$}
\BinaryInfC{$\Gamma, \phi \vee \psi \vdash \gamma$}
\DisplayProof
} & \multicolumn{3}{c}{
\AxiomC{$\Gamma \vdash \phi$}
\UnaryInfC{$\Gamma \vdash \phi \vee \psi$}
\DisplayProof
} & \multicolumn{3}{c}{
\AxiomC{$\Gamma \vdash \psi$}
\UnaryInfC{$\Gamma \vdash \phi \vee \psi$}
\DisplayProof
}\\
\multicolumn{6}{c}{
\AxiomC{$\Gamma, \phi \rightarrow \psi \vdash \phi$}
\AxiomC{$\Gamma, \psi \vdash \gamma$}
\BinaryInfC{$\Gamma, \phi \rightarrow \psi \vdash \gamma$}
\DisplayProof
} & \multicolumn{6}{c}{
\AxiomC{$\Gamma, \phi \vdash \psi$}
\UnaryInfC{$\Gamma \vdash \phi \rightarrow \psi$}
\DisplayProof
}\\
\multicolumn{6}{c}{
\AxiomC{$\Gamma, \neg \phi \vdash \phi$}
\UnaryInfC{$\Gamma, \neg \phi \vdash \psi$}
\DisplayProof
} & \multicolumn{6}{c}{
\AxiomC{$\Gamma, \phi \vdash$}
\UnaryInfC{$\Gamma \vdash \neg \phi$}
\DisplayProof
}\\
\multicolumn{12}{c}{
\AxiomC{$\Sigma, \Gamma, \Theta, \Gamma', \Sigma' \vdash \phi$}
\UnaryInfC{$\Sigma, \Gamma', \Theta, \Gamma, \Sigma' \vdash \phi$}
\DisplayProof
}
\end{tabular}
\end{table}

BBBBBBBBBBBBBBBBBBBBBBBBBBB

\section{Logica proposizionale classica}

CCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCC

\begin{table}[]
\centering
\begin{tabular}{cccccc}
\multicolumn{2}{c}{
\AxiomC{}
\UnaryInfC{$\Gamma, \phi, \Gamma' \vdash \Delta, \phi, \Delta'$}
\DisplayProof
} & \multicolumn{2}{c}{
\AxiomC{}
\UnaryInfC{$\Gamma, \bot, \Gamma' \vdash \Delta$}
\DisplayProof
} & \multicolumn{2}{c}{
\AxiomC{}
\UnaryInfC{$\Gamma \vdash \Delta, \top, \Delta'$}
\DisplayProof
}\\
\multicolumn{3}{c}{
\AxiomC{$\Gamma, \phi, \psi \vdash \Delta$}
\UnaryInfC{$\Gamma, \phi \wedge \psi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{c}{
\AxiomC{$\Gamma \vdash \phi, \Delta$}
\AxiomC{$\Gamma \vdash \psi, \Delta$}
\BinaryInfC{$\Gamma \vdash \phi \wedge \psi, \Delta$}
\DisplayProof
}\\
\multicolumn{3}{c}{
\AxiomC{$\Gamma, \phi \vdash \Delta$}
\AxiomC{$\Gamma, \psi \vdash \Delta$}
\BinaryInfC{$\Gamma, \phi \vee \psi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{c}{
\AxiomC{$\Gamma \vdash \phi, \psi, \Delta$}
\UnaryInfC{$\Gamma \vdash \phi \vee \psi, \Delta$}
\DisplayProof
}\\
\multicolumn{3}{c}{
\AxiomC{$\Gamma \vdash \phi, \Delta$}
\AxiomC{$\Gamma, \psi \vdash \Delta$}
\BinaryInfC{$\Gamma, \phi \rightarrow \psi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{c}{
\AxiomC{$\Gamma, \phi \vdash \psi, \Delta$}
\UnaryInfC{$\Gamma \vdash \phi \rightarrow \psi, \Delta$}
\DisplayProof
}\\
\multicolumn{3}{c}{
\AxiomC{$\Gamma \vdash \phi, \Delta$}
\UnaryInfC{$\Gamma, \neg \phi \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{c}{
\AxiomC{$\Gamma, \phi \vdash \Delta$}
\UnaryInfC{$\Gamma\vdash \neg \phi, \Delta$}
\DisplayProof
}\\
\multicolumn{3}{c}{
\AxiomC{$\Sigma, \Gamma, \Theta, \Gamma', \Sigma' \vdash \Delta$}
\UnaryInfC{$\Sigma, \Gamma', \Theta, \Gamma, \Sigma' \vdash \Delta$}
\DisplayProof
} & \multicolumn{3}{c}{
\AxiomC{$\Gamma \vdash \Sigma, \Delta, \Theta, \Delta', \Sigma'$}
\UnaryInfC{$\Gamma \vdash \Sigma, \Delta', \Theta, \Delta, \Sigma'$}
\DisplayProof
}
\end{tabular}
\end{table}

DDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDDD
`
La prima tabella dovrebbe comparire tra la riga di A e la riga di B, la seconda tabella dovrebbe comparire tra la riga di C e la riga di D e invece…allego il risultato che ottengo.

[attachment]C:\fakepath\anteprima.png[/attachment]

Ho creato una table con multicolumn come mi hai suggerito:
`
\begin{table}[]
\centering
\begin{tabular}{clllclclclll}
\multicolumn{4}{c}{ax1} & \multicolumn{4}{c}{ax2} & \multicolumn{4}{c}{ax3}\\
\multicolumn{6}{c}{e s} & \multicolumn{6}{c}{e d}\\
\multicolumn{6}{c}{o s} & \multicolumn{3}{c}{o d 1} & \multicolumn{3}{l}{o d 2}\\
\multicolumn{6}{c}{implica s} & \multicolumn{6}{c}{implica d}\\
\multicolumn{6}{c}{neg s} & \multicolumn{6}{c}{neg d}\\
\multicolumn{12}{c}{scambio}
\end{tabular}
\end{table}
`
Fin qui tutto bene.
Ho anche scritto una dimostrazione tramite calcolo dei sequenti con il package bussproofs:
`
\begin{prooftree}
\AxiomC{$\Gamma, \phi, \psi \vdash \gamma$}
\UnaryInfC{$\Gamma, \phi \wedge \psi \vdash \gamma$}
\end{prooftree}
`
Anche qui tutto bene.
Il problema nasce quando vado ad inserire la dimostrazione all’interno della multicolumn:
`
\begin{table}[]
\centering
\begin{tabular}{clllclclclll}
\multicolumn{4}{c}{ax1} & \multicolumn{4}{c}{ax2} & \multicolumn{4}{c}{ax3}\\
\multicolumn{6}{c}{
\begin{prooftree}
\AxiomC{$\Gamma, \phi, \psi \vdash \gamma$}
\UnaryInfC{$\Gamma, \phi \wedge \psi \vdash \gamma$}
\end{prooftree}
} & \multicolumn{6}{c}{e d}\\
\multicolumn{6}{c}{o s} & \multicolumn{3}{c}{o d 1} & \multicolumn{3}{l}{o d 2}\\
\multicolumn{6}{c}{implica s} & \multicolumn{6}{c}{implica d}\\
\multicolumn{6}{c}{neg s} & \multicolumn{6}{c}{neg d}\\
\multicolumn{12}{c}{scambio}
\end{tabular}
\end{table}
`
In fase di compilazione ottengo l’errore:

! LaTeX Error: Something’s wrong–perhaps a missing \item.

See the LaTeX manual or LaTeX Companion for explanation.
Type H for immediate help.
…

l.74 }
& \multicolumn{6}{c}{e d}\\
?

Quale può essere il problema?

Il mio problema non è come inserire i simboli, ma come inserire quelle strutture “a più piani” tipiche del calcolo dei sequenti. Chiedevo se c’era un pacchetto apposito.

Grazie mille!

Ho fatto come mi hai suggerito ed ho ottenuto proprio il risultato cercato. Grazie mille ad entrambi!

Grazie mille, ho adottato la soluzione con il comando \onehalfspace.

OldClaudio” post=120377
Il coefficiente 1.5 per lo scartamento è accettabile in tipografia solo quando le righe contengono formule o caratteri che sporgono fuori dallo spazio previsto per ciascuna riga in relazione al corpo, e consentono di comporre le righe con interlinee uguali fra tutte le righe; mancando queste condizioni, si tratta di cattiva tipografia o cattive abitudini contratte usando i soliti word processor.

Effettivamente le indicazioni che ho ricevuto per la stesura del documento in questione sono pensate per un word processor, sto quindi adeguando il preambolo perchè il mio documento le rispetti anche se scritto in LaTeX.

A questo proposito ne approfitto per chiedere un altro dubbio analogo: nelle indicazioni che ho ricevuto è richiesto di utilizzare un carattere di 12 (si fa sempre riferimento ad un word processor), ma di cosa si tratta? Punti o altro? Si tratta quindi di 12pt?

Il motivo per cui vorrei rimuovere l’indentazione quando si va a capo è che ho visto che nella quasi totalità delle tesi di informatica e matematica non si adotta questa convenzione.

Il motivo per cui non mi piaceva l’idea di settare a 0 il valore di \parindent è che se in qualche punto del mio documento decidessi di inserire un’indentazione questa sarebbe per così dire invisibile, quindi speravo che ci fosse un modo di disabilitare l’indentazione automatica ma allo stesso tempo di consentire l’indentazione manuale della larghezza standard.