We show how to integrate implicit inductive theorem proving into free variable sequent and tableau calculi and compare the appropriateness of tableau calculi for this integration with that of sequent calculi.
Wirth, C. P. (1999). Full first-order free variable sequents and tableaux in implicit induction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1617, pp. 293–307). Springer Verlag. https://doi.org/10.1007/3-540-48754-9_25