[FOM] A textbook on logic with natural deduction

[Vaughan Pratt]

Did anyone mention Smullyan, First-Order Logic, SV 1968?  This is where 
I first learned about Beth's semantic tableaux, along with Smullyan's 
adaption of them as analytic tableaux, in 1977.  I applied these ideas 
in "A Practical Decision Method for Propositional Dynamic Logic," ACM 
STOC'78, pp 326-337.  I hadn't seen tableaux used in program 
verification before, though that's not to claim they hadn't been. 
Certainly in CS as a whole the sequent approach can be traced back to 
Prawitz et al and Wang around 1958, who may I guess have been influenced 
more by Gentzen than Beth since the latter's book The Foundations of 
Mathematics, NH 1959, had not yet appeared.  The historians would be a 
better judge of this.

Vaughan Pratt