Gentzen introduced cut-free proofs in 1934. In these, all formulas are subformulas of what is being proved (and with the same polarity). This is an important feature for many reasons, proof search among them. In 1957 Ohnishi and Matsumoto extended Gentzen’s ideas to several modal logics. Beth introduced tableaus in the 1950’s, with their modern version coming from Smullyan in the 1960’s. Roughly, tableaus are sequent calculi upside-down. I (probably) introduced tableau versions of Ohnishi and Matsumoto’s calculi in the 1970’s. All this treated a small number of modal logics.

Based on an idea of Fitch, I introduced prefixed tableaus in 1972. These add new machinery, but are able to handle many more modal logics. Today they are rather common in automated theorem proving.

In a recent (yet unpublished) paper I introduced set prefixed tableaus. We now have machinery that can handle an infinite family of modal logics, including all the most common ones. And they do this in a uniform way, separating logical rules from so-called structural rules.

The idea that tableaus and sequent calculi are dual to each other continues. Nested sequents have been much studied. In a paper from 2012 I showed that nested sequents and prefixed tableaus were dual, in this sense. And I have a new construct, indexed nested sequents, which is dual to set prefixed tableaus. The pattern continues.

I will cover as much of this as time permits. (My talk is intended to be a trial run for a talk to be given at UNILOG, In Istanbul, this summer.)