Secondo una tradizione che risale alla "Deduzione Naturale" di G. Gentzen, il significato di una parola logica (congiunzione, disgiunzione, negazione, condizionale) è completamente determinato dalle regole di introduzione e di eliminazione che ne governano l'uso. Le regole di introduzione specificano le condizioni sufficienti per la verità (o la falsità) di proposizioni che contengono la parola logica come "operatore principale". Per esempio se sono vere sia P sia Q allora è vera la loro congiunzione P & Q. Le regole di eliminazione specificano invece le conseguenze della verità (o della falsità) di tali proposizioni: se è vera la congiunzione P & Q allora sono vere sia P sia Q.
Negli anni '50 del ventesimo secolo E. Beth e J. Hintikka scoprirono indipendentemente che è possibile costruire un calcolo logico completo per la logica classica del primo ordine basato esclusivamente su regole di eliminazione (il metodo dei tableaux analitici reso celebre da un fortunato libro di Raymund Smullyan). In questo articolo del 1995, pubblicato sul Journal of the IGPL, Mondadori affronta il problema inverso: è possibile costruire un calcolo completo per la logica classica del primo ordine che sia basato solo su regole di introduzione? Esistono dei "tableaux sintentici" le cui regole siano, in un senso ben definito, "inverse" di quelle dei Tableaux Analitici? Si tratta di un problema ricco di implicazioni sia per la filosofia della logica sia per la teoria del ragionamento automatico. In questo lavoro Mondadori prospetta un'elegante soluzione di questo problema e la confronta con il metodo dei tableaux sottolineandone i vantaggi anche sul piano computazionale. (marcello.d'agostino)